<OAI-PMH xmlns="http://www.openarchives.org/OAI/2.0/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.openarchives.org/OAI/2.0/ http://www.openarchives.org/OAI/2.0/OAI-PMH.xsd"> <responseDate>2002-05-01T19:20:30Z</responseDate> <request verb="GetRecord" identifier="oai:arXiv.org:hep-th/9901001" metadataPrefix="oai_dc">http://an.oa.org/OAI-script</request> <GetRecord> <record> ... </record> </GetRecord> </OAI-PMH>
(∃ q : OAI-request) (∃ r : OAI-response) (∃ s : OAI-server) (∃ t : moment)(Details of the notation are given in section 4.)
(uri_server({string(./oai:request)}, s)
∧ models({./oai:request}, q)
∧ {.} = r
∧ xsd_lv(xsd:dateTime, {string(./oai:responseDate)}, t)
∧ served_response(q,s,t,r))
(∃ q : OAI-request) (∃ r : OAI-response) (∃ s : OAI-server) (∃ t : moment)
(uri_server(‘http://an.oa.org/OAI-script’, s)
∧ models(element(/1/2), q)
∧ element(/1) = r
∧ xsd_lv(xsd:dateTime, ‘2002-05-01T19:20:30Z’, t)
∧ served_response(q,s,t,r))
(∃ q : OAI-request) (∃ r : OAI-response) (∃ s : OAI-server) (∃ t : moment)Here the indented clauses have been added vis-a-vis the previous translation.
(uri_server({string(./oai:request)}, s)
∧ (∀ x)(uri_server({string(./oai:request)}, x) ⇒ x = s)
∧ (∀ x)(uri_server(x, s) ⇒ x = {string(./oai:request)})
∧ models({./oai:request}, q)
∧ (∀ x)(models({./oai:request}, x) ⇒ x = q)
∧ {.} = r
∧ xsd_lv(xsd:dateTime, {string(./oai:responseDate)}, t)
∧ (∀ x)(xsd_lv(xsd:dateTime, {string(./oai:responseDate)}, x) ⇒ x = t)
∧ served_response(q,s,t,r))
There exist an OAI request q, an OAI response r, an OAI server s, and a moment in time t, such that:
- The string value of the oai:request child is the URI of s (and there is only one such server, i.e. any server whose URI is that string value is identical to s, and also that server has only one URI, i.e. any URI which is the URI of s is that string value).
- The request q is modeled by the oai:request child (and there is only one such request).
- The response r is the same as the current (oai:OAI-PMH) element.
- The moment t is the moment identified by the string value of the oai:responseDate child, interpreted according to the usual lexical mapping of the XML Schema dateTime type (and there is only one such moment).
- Server s served response r to request q at moment t.
(∃ r : OAI-response)
{.} = r
∧ served_response(
(℩ q)(OAI-request(q) ∧ models({./oai:request}, q)),
(℩ s)(OAI-server(s) ∧ uri_server({string(./oai:request)}, s)
∧ (∀ x)(uri_server(x, s) ⇒ x = {string(./oai:request)})),
(℩ t)(moment(t) ∧ xsd_lv(xsd:dateTime, {string(./oai:responseDate)}, t)),
r))
(∃ r : OAI-response)In prose paraphrase, this works out to something like “There exists an OAI response r such that there exist (a) a unique OAI request q modeled by the oai:request child element, (b) a unique OAI server whose URI is the string value of the oai:request child element, and (c) a unique moment t which is mapped to from the string value of the oai:responseDate child using the lexical mapping for xsd:dateTime, such that server s served response r to request q at moment t. ”
(℩ q (OAI-request(q) ∧ models({./oai:request}, q)))
(℩ s (OAI-server(s) ∧ uri_server({string(./oai:request)}, s)))
(℩ t (moment(t) ∧ xsd_lv(xsd:dateTime, {string(./oai:responseDate)}, t)))
((∀ x)(uri_server(x, s) ⇒ x = {string(./oai:request)})
∧ {.} = r
∧ served_response(q,s,t,r))
(∀ s : OAI-server) (∀ u : string) (uri_server(u, s) ⇒ (∀ x)(uri_server(u, x) ⇒ x = s) ∧ (∀ x)(uri_server(x, s) ⇒ x = u))(i.e. both the relation uri_server and its inverse are functions), then the relative uniqueness of the arguments need not be asserted each time the relation is used. It is an empirical question, whose answer is not currently clear, whether all definite descriptions in our logical translation can be handled in this way.
(∃ q : OAI-request) (∃ r : OAI-response) (∃ s : OAI-server) (∃ t : moment)
( q = (℩ q : OAI-request)(models({./oai:request}, q))
∧ s = (℩ s : OAI-server)(uri_server({string(./oai:request)}, s))
∧ t = (℩ t : moment)(xsd_lv(xsd:dateTime, {string(./oai:responseDate)}, t))
∧ (∀ x)(uri_server(x, s) ⇒ x = {string(./oai:request)})
∧ {.} = r
∧ served_response(q,s,t,r))
(∃ t : moment) (∃ r : OAI-response)
(xsd_lv(xsd:dateTime, {string(.)}, t)
∧ r = {..}
∧ was_sent_at(r,t))
<responseDate>2002-05-01T19:20:30Z</responseDate>
<request verb="GetRecord" identifier="oai:arXiv.org:cs/0112017" metadataPrefix="oai_dc">http://arXiv.org/oai2</request>
(∃ q : OAI-request) (models({ . }, q)
∧ ( {string(@verb)} ≠ "" ⇒ request_verb(q, {string(@verb)}) )
∧ ( ( {string(@verb)} = "GetRecord"
∧ request_identifier(q, {string(@identifier)})
∧ request_metadataPrefix(q, {string(@metadataPrefix)}) )
∨ ( {string(@verb)} = "Identify"
∧ {count(@*)} = 0 )
∨ ( {string(@verb)} = "ListIdentifiers"
∧ request_from(q, {string(@from)})
∧ request_until(q, {string(@until)})
∧ request_metadataPrefix(q, {string(@metadataPrefix)})
∧ request_set(q, {string(@set)})
∧ request_resumptionToken(q, {string(@resumptionToken)}) )
∨ ( {string(@verb)} = "ListMetadataFormats"
∧ request_identifier(q, {string(@identifier)}) )
∨ ( {string(@verb)} = "ListRecords"
∧ request_from(q, {string(@from)})
∧ request_until(q, {string(@until)})
∧ request_metadataPrefix(q, {string(@metadataPrefix)})
∧ request_set(q, {string(@set)})
∧ request_resumptionToken(q, {string(@resumptionToken)}) )
∨ ( {string(@verb)} = "ListSets"
∧ request_resumptionToken(q, {string(@resumptionToken)}) ) )
<error code="badVerb">Illegal OAI verb</error>
(∃ q : OAI-request) (models({preceding-sibling::oai:request}, q)
∧ invalid(q)
∧ request_error(q, {string(@code)})
∧ ({string(.)} ≠ "" ⇒ error_nldesc(q, {string(.)}) ) ) )
(∃ q : OAI-request) (∃ s : oai-server) (∃ d : string) (∃ i : oai-item) (∃ p : string)In addition, we know in practice that the oai:record child of oai:GetRecord contains the requested metadata record in the requested format for the requested item. But it's more convenient to capture that in the sentence schemata for the oai:record element than here.
(q = (℩ q : OAI-request)(req_resp(q,{ancestor::oai:OAI-PMH}))
s = (℩ s : oai-server)(resp_server({ancestor::oai:OAI-PMH}, s))
d = (℩ d : string)(request_identifier(q, d))
i = (℩ i : oai-item)(item_id(i, d))
p = (℩ p : string(p)(request_metadataPrefix(q, p))
∧ request_verb(q, "GetRecord")
∧ errorfree(q)
∧ isin_repository_item(s, i)
∧ hasformat_repository_item_format(s, i, p) )
(∀ q : OAI-request)(errorfree(q) ≡ ¬invalid(q))
(∀ q : OAI-request) (∀ s : OAI-server) (∀ t : moment) (∀ r : OAI-response) (served_response(q,s,t,r) ⇒ was_sent_at(r,t))
Hughes, G. E., and M. J. Cresswell. 1996. A new introduction to modal logic. London, New York: Routledge.
Lagoze, Carl, Herbert Van de Sompel, Michael Nelson, and Simeon Warner, ed. 2002. The Open Archives Initiative Protocol for Metadata Harvesting. Protocol Version 2.0 of 2002-06-14. Document Version 2004/10/12T15:31:00Z. [n.p.]: Open Archives Initiative, 2002. <URL:http://www.openarchives.org/OAI/2.0/openarchivesprotocol.htm>
Quine, Willard Van Orman. 1951. Mathematical logic. Revised edition. Cambridge, Mass.: Harvard University Press.
Quine, W. V. 1982. Methods of logic. Cambridge, Mass.: Harvard University Press.
Sperberg-McQueen, C. M., Claus Huitfeldt, and Allen Renear. “Meaning and interpretation of markup.” Markup Languages: Theory & Practice 2.3 (2001): 215–234. <URL:http://www.w3.org/People/cmsmcq/2000/mim.html>