gruninger / common-logic Goto Github PK
View Code? Open in Web Editor NEWDocuments for the developments of ISO 24707 Editiion 2 (Common Logic)
Documents for the developments of ISO 24707 Editiion 2 (Common Logic)
In Colore there are axiomatizations for recurring strucures. E.g., there is an axiomatization of partial order.In order to reuse these axioms, e.g., in the axiomatization of "smaller than" it is important to be able to rename the names in the axiomatization. This would involve some signature mapping.
Defect Nos.: 19
Submitter: Chris Angus
References in Document: p.65 C.2 3.1.5
Nature of Defect: The abstract syntax metamodel does not support a
Binding having comment associated with it (nor does
CLIF), however XCL allows a element to
contain zero, one or more comments. This would
appear to prevent XCL being syntactically fully
conformant.
Proposed Solution: Either add support for comments being
associated with a Binding to the abstract
syntax metamodel and CLIF or remove
them from XCL.
NEED SPECIFIC TEXT CHANGES HERE
Defect Nos.: 18
Submitter: Chris Angus
References in Document: p.59-60
Nature of Defect: The content for a element is at variance
with the abstract syntax metamodel in that it allows
multiple elements.
Proposed Solution: Amend the content to be an optional
element and a element
containing the body of the module
NEED SPECIFIC TEXT CHANGES
HERE
Submitter: Pat Hayes
References in Document: p.18, 1 para last sentence
Nature of Defect: Sentence seems to contradict the formal semantics
Proposed Solution: Replace “The module
name may be used to identify a common universe of
discourse associated with the dialect, or a local universe
of discourse special to the text in the module.” with "The
module name indicates a local universe of discourse
special to the text in the module, which can be asserted
to be equivalent to a common universe of discourse
associated with the dialect by sentences outside the
module."
Submitter: Pat Hayes
References in Document: p.7 - 5.1.1, 2 sentence
Nature of Defect: First sentence uses "shall", second sentence uses
"will". It is not clear if this indicates a difference of
sense. If it does, this difference should be clarified. If
it does not, a single term should be used
consistently.
Proposed Solution:
The XCL entries of the CL Defect Report
[1] http://cl.tamu.edu/docs/cl/24707-defect-report.pdf give a very
incomplete picture of the problems with this first version of XCL (XCL1).
The additional serious XCL1 defects may be divided into two groups:
A. serious defects in the schema design
B. serious defects in the syntax design
A. The XCL1 DTD as published in the CL specification is not modular, and
so does not distinguish some subset of the syntax which could, in
principle, be exactly semantically conformant. All schema languages
allow such modularization, and we propose that the revised XCL schema be
divided into multiple parts, a core schema and one or more standard
extension modules. This is easily accomplished with Relax NG [2]
http://www.ccil.org/%7Ecowan/relaxng.pdf, and is also possible in XSD
and DTD.
There is in actuality no subset of XCL1 that is exactly semantically
conformant, so additional modifications, as described in part B, will be
necessary to create a core XCL2 syntax that is exactly semantically
conformant.
There are certain features, such as typed literals, that are easily
implemented (syntactically) in XML and that would be useful to most
applications, but are not (yet) part of the abstract CL syntax. These
features would be implemented in the standard extension modules (with
semantics of typed literals according to the outcome of the parallel
discussion on this topic.)
Note: Let us emphasize the difference between such standard extensions
of the XCL syntax versus XCL extensions external to the CL standard that
might introduce, e.g., non-monotonic logic.
B. We found a basic flaw in the design of XCL1 consisting of the
introduction of elements for higher-level syntactic categories that
should instead be non-terminals that are not shown in XML-instance
serializations (such 'invisible' non-terminals are implemented as
entities in DTD, patterns in Relax NG and groups in XSD). This flaw is
repeated multiple places (, , ) and causes multiple
problems.
<text>
- This element serves as a root element, and also for the
syntactic categories of named text and unnamed text. (We don't
distinguish commented text as a syntactic category, as just about
anything can have an attached comment.) The problems caused by this
overloading of are:
Named texts cannot be nested within any other element, while unnamed
texts can be nested within other texts and modules. For conformance, it
is therefore necessary to have two different syntactic categories for
texts, and it would be best to indicate these categories explicitly by
the name of their elements. In XCL1, nesting of texts within other texts
and within modules is not implemented at all, and so XCL1 is not exactly
conformant as a CL dialect.
<phrase>
- This element is completely unnecessary. Instead, "phrase"
should be a (serialization-)invisible non-terminal which is a choice
among the non-terminals for sentence, unnamed text, module and
importation. Problems caused by this include:
<term>
- In XCL1, this element is used to denote names of all kinds and
also functional terms. Instead, "term" should be an invisible
non-terminal which is a choice among non-terminals for the syntactic
categories name and functional term, resp. The syntactic category "name"
could be further expanded in extensions to cover both interpretable and
fixed-interpretation names. Problems caused by this overloading of
include:
<module>
<exclude>
<term>
<function><term name="a"/></function>
<term name="b"/>
</term>
</exclude>
...
</module>
This creates a syntactic disconnect between the binding and the terms in
the quantified sentence. For example, we must make "x" both a and
a when we state
<exists>
<var name="x"/>
<atomic><relation><term name="x"/></relation></atomic>
</exists>
<term name="x">
<function><term name="P"/></function>
<term name="y"/>
</term>
In comparison, the invisible "sentence" non-terminal introduces
extensibility, so extensions can increase the choices for "sentence" to
include, say, weak negation, modal sentences, fuzzy sentences, ...
To correct these and other defects, modifications including, but not
limited to, the following are proposed:
Elements to be deleted from the core XCL syntax without replacement
<phrase>
<relation>
<function>
<quantification>
<boolean>
<role>
<guard>
Attributes to be deleted from the core XCL syntax without replacement
@dialect
(may be implemented in external extensions, but processors@logicalFormOf
(may be implemented in external extensions)@syntaxType
(may be implemented in external extensions)@xml:id
( removes the ambiguity of the module name, also allowsxs:ID
with the nameNote: contrary to the statement in Annex C, it is never acceptable for a
base IRI to be "arbitrary". If relative references are used, then the
base IRI should be explicitly specified. Otherwise the text violates the
Common Logic "means the same everywhere on the network" principle.)
Elements that need to be split:
<text>
<term>
Element to be added:
Content model changes
<relation>
choice from the "atom" non-terminalAdditional errors in the DTD
p. 54 There is inconsistency in the public identifiers declared for the
DTD and the documentation.
This DTD has the following formal public identifiers:
"ISO/IEC 24707:2006//DTD XML Common Logic (XCL) 1.0//EN"
"-//purl.org/xcl//DTD XML Common Logic (XCL) 1.0//EN"
The DTD may be invoked by one of the following declarations:
<!DOCTYPE text PUBLIC
"ISO/IEC 24707:2006//DTD XCL Markup Language//EN">
"xcl1.dtd">
<!DOCTYPE text PUBLIC
"-//purl.org/xcl//DTD XML Common Logic (XCL) 1.0//EN"
We have already recommended that the syntax be specified in Relax NG and
in XSD automatically derived from the Relax NG, not in DTD, so this
defect would be irrelevant.
p.55
<!ENTITY % URI.datatype "CDATA" >
This allows any string for some attributes such as @href, but the
attribute value should be limited to the lexical space of the IRI
datatype. In Relax NG this would be corrected as follows:
URI.datatype = xsd:anyURI
Summary: It would not be feasible to make even a modest subset of the
proposed changes to the specification by piecemeal corrections of the
published DTD. We propose that the entire Annex C be rewritten.
Nevertheless, we feel that the proposed modifications to schema and
syntax design can be made without being overly burdensome to existing
users for the following reasons.
Defect Nos.: 21
Submitter: John Sowa
References in Document: p.48 B.3.4
Nature of Defect: eitherOr ="[",[comment] ?cm?,"Either",[":"],
{[comment], nestedOrs} ?ors?, [endComment] ?ecm?, "]";
Proposed Solution: Remove "{" and "}" in 2nd line to read:
[comment], nestedOrs ?ors?,
[endComment] ?ecm?, "]";
Submitter: Pat Hayes
References in Document: p.16, 2nd para, 4th sentence
Nature of Defect: The qualification "... but shall not use irregular
sentence forms to represent content that is
expressible in Common Logic text." is unnecessary
and potentially harmful to interoperability under
certain conditions. It is not mentioned in section 7
defining conformity, so it may be left over from an
earlier version by mistake.
Proposed Solution: Replace “, but shall not use irregular
sentence forms to represent content that is
expressible in Common Logic text.” With
“.”
Section 3, page 4.
The current language is:
3.12
individual
one element of the universe of discourse
NOTE The universe of discourse is the set of all individuals.
3.22 term
〈Common Logic〉 expression which denotes an individual, consisting of either a name or, recursively, a function term applied to a sequence of arguments, which are themselves terms
This is not consistent with the definition of interpretations in 6.2 where the universe of discourse may be a proper subset of the universe of reference.
Proposed:
3.22 term
〈Common Logic〉 expression which denotes an element of the universe of reference, consisting of either a name or, recursively, a function term applied to a sequence of arguments, which are themselves terms
Submitter: Pat Hayes
References in Document: p.31
Nature of Defect: The ordering of the names X1 ... Xn is not specified, and
there is no natural way to specify it. Hence this 'mapping' is
undefined, and hence the CLIF semantics is undefined, for
the guarded quantifier construction.
Solution is to remove the 'guarded quantifier' construction
from the CLIF specification in Appendix A. This solution
was arrived at by a clear consensus among the technical
committee which designed the specification. The guarded
quantifier construction is currently the subject of on-going
research, is not required by the main CL spec and has not
been implemented or used by any known CLIF project.
Proposed Solution:
(a) Delete lines 4 and 5 from table A.2 on page 31
(b) In A 2.3.8, page 29: remove the words "and may be guarded;"
(c) In A 2.3.8, page 29: remove the option “[ interpretablename ]” from the first production
(d) In A.1, page 24: remove item 11.
Provide a possibility to name sentences. This is essential for keeping the overview when using a theorem prover with large theories.
Submitter: Pat Hayes
References in Document: p.21 – 7.1.2 last sentence of para “Semantic extensions shall…”
Nature of Defect: “less complete” is ambiguous and misleading
Proposed Solution: Replace “may be less complete” with “may be incomplete”
phrase = sentence | module | (open, 'cl:imports' , interpretablename , close) | (open,
'cl:comment', quotedstring, cltext, close);
cltext = { phrase } ;
namedtext = open, 'cl:text' interpretablename, text, close ;
cltext = module | namedtext | text ;
cltext occurs twice on the left side. The last line is probably right, and refers to the root of the grammar. (But see #40 for a new proposal to have documents at the root.)
But the first occurrence of cltext should be
text = { phrase }
(Thanks to Sören Schulze for spotting this problem!)
In phrase
, the ambiguos cltext occurs on the right side. The thing that is commented upon should most likely be a list of phrases; therefore we suggest the following as a revision of the first line:
phrase = sentence | module | (open, 'cl:imports' , interpretablename , close) | (open,
'cl:comment', quotedstring, text, close);
There is one more occurrence of the ambiguous cltext
in the standard, in A.2.3.10 Module:
module = open, 'cl:module' , interpretablename , [open, 'cl:excludes' , {name} , close ] , cltext, close;
We are quite sure that this should rather be
module = open, 'cl:module' , interpretablename , [open, 'cl:excludes' , {name} , close ] , text, close;
as it does not make sense that a module, which has a name, contains texts having different, possibly unrelated names.
(also reported by Pat Hayes)
Submitter: Pat Hayes
References in Document: p.13 - 6.2 1st sentence
Nature of Defect: the phrase "mathematical structures" is potentially
misleading as it can be construed as being contrasted with
other 'kinds' of structure. The qualifier "mathematical" is
not necessary to the sense of the sentence, so should be
deleted.
Proposed Solution: Delete “mathematical”
References in Document: pp.8, 9, 11, 13, 16, Sections 6.1.1.1, 4, 5, 7, 6.1.2, 6.2, 6.3.1
Nature of defect:
Summary: The abstract syntax does not address the case where the syntax has a method for distinguishing identifiers and syntactically constraining these names from occurring bound in a quantified sentence. Further, the standard does not specifically state that all dialects must disallow identifiers being bound in a quantified sentence.
Discussion: A CL dialect that supports named texts, modules and importations, as is required for full conformance, must have rigid identifiers that are used for the names of texts, modules, vocabularies, and in importations.
Recall from the CL Standard, rigid identifiers (if there are any) are always names, but not all names are rigid identifiers. In several places, the Standard also uses "identifier", without the qualifier "rigid", to mean "rigid identifiers". Thus, in CL all identifiers are rigid identifiers, and from this point on I'll use "identifier" to mean rigid identifier.
Identifiers should not be used as freely as other names. In particular, it is not appropriate for an identifier to occur bound in a quantified sentence [1].
Aside from quantifier bindings, an identifier may be used anywhere other names are used (predicate, operator, term, exclusion set), and its denotation is a member of the domain of discourse unless excluded within a module (or used as a non-discourse name in a segregated dialect.) Identifiers as terms, operators and predicates are especially useful if vocabularies are derived from imported OWL ontologies or RDF graphs, which use IRIs for the names of classes, properties and individuals.
Further, extensions may use identifiers in other ways, e.g. to label and import or clone fragments of texts, such as sentences or terms, and to reference externally-defined datatype definitions, external annotations, "built-in" functions, and so on.
The reason for the restriction against identifiers occurring bound in a quantified sentence can be demonstrated with CLIF. CLIF does not distinguish syntactically between identifiers and other interpretable names, so the following text is syntactically legal according to the grammar.
(cl-text "http://xyz.org" (= a b))
(forall ("http://xyz.org") (P "http://xyz.org"))
The semantics (say for an interpretation I) takes an unexpected turn with this text however, because the quantification requires us to consider any interpretation J where the denotation of "http://xyz.org" "might" differ from that of I. However, all available (either CL or CLIF) interpretations give the same meaning to "http://xyz.org" because it is an identifier, so the text is true exactly when
The only way around this for CLIF is to simply declare that identifiers must not be bound in a quantified sentence, even though the grammar allows it. For this to be possible, fixing the subset of names which are identifiers must be a part of the specification of the vocabulary. However, this is not currently stated in the CL abstract semantics.
Other dialects may choose to take a different approach (from CLIF) on identifiers. Although there has not been much enthusiasm for complicating the abstract syntax by specifying details about particular identifier systems, such as IRIs, there is no reason a particular dialect could not include such details. In particular, XML has built-in capabilities for handling IRIs syntactically, and it is reasonable, if not expected, that an XML-based Common Logic dialect should incorporate both the lexical restrictions of IRIs for identifiers, and syntactic constraints that prevent identifiers occurring bound in a quantified sentence.
The abstract syntax and semantics could be modified to allow dialects that make a syntactic distinction between identifiers and other names to be considered exactly semantically conformant, without requiring this for all dialects.
Solution proposed by the submitter:
Original: (6.1.1.1) A piece of text shall optionally be identified by a name.
Proposal (6.1.1.1) A piece of text shall optionally be identified by an identifier. All identifiers are names.
Original (6.1.1.4) A module consists of a name, an optional set of names called the exclusion set, ...
Proposal (6.1.1.4) A module consists of an identifier, an optional set of names called the exclusion set, ...
Original (6.1.1.5) An importation contains a name ...
Proposal (6.1.1.5) An importation contains an identifier ...
Original (6.1.1.7) A quantified sentence has (i) a type, called a quantifier, (ii) a finite, nonrepeating sequence of names and sequence markers called the binding sequence, each element of which is called a binding of the quantified sentence, and (iii) a sentence called the body of the quantified sentence.
Proposal (6.1.1.7) A quantified sentence has (i) a type, called a quantifier, (ii) a finite, nonrepeating sequence of names and sequence markers called the binding sequence, each element of which is called a binding of the quantified sentence, and (iii) a sentence called the body of the quantified sentence. A binding must not be an identifier.
Fig. 4 p. 11 (UML diagram) p. 11. The class box labeled "Name" should be labeled instead as "Non-Identifier Name".
Section 6.2, p. 13
Original: The vocabulary of a Common Logic text is the set of names and sequence markers which occur in the text. In a segregated dialect, the names in vocabularies are partitioned into discourse names and non-discourse names.
Proposal: The vocabulary of a Common Logic text is the set of names and sequence markers which occur in the text. In all dialects, the names are partitioned into identifier and non-identifier names. In a segregated dialect, the names in vocabularies are also partitioned into discourse names and non-discourse names; identifiers may be either discourse or non-discourse.
Section 6.2, p. 14
Original: An interpretation J of V is an S-variant of I if it is exactly like I except that intJ and seqJ might differ with intI and seqI on what they assign to the members of S.
Proposal: An interpretation J of V is an S-variant of I if it is exactly like I except that intJ and seqJ might differ with intI and seqI on what they assign to the non-identifier members of S.
Section 6.3 p. 16
Original This section applies only to dialects which support importations and/or named texts.
Proposal This section applies only to dialects which support importations and/or named texts and/or modules.
(Insertion between para. 2 and 3 in Section 6.3.1, p. 16)
Particular dialects may, but are not required to, introduce means to designate which names are identifiers, e.g. through naming conventions, punctuation or declaration. All dialects must disallow identifiers occurring bound in a quantified sentence; however, a Common Logic dialect is not required to provide sufficient syntactic constraints to guarantee that identifiers are not bound in a quantified sentence in any syntactically legal text of the dialect.
Related Issues:
Background:
The CL standard mentions identifiers and identification in several places.
p.8 6.1.1.1 ... A piece of text shall optionally be identified by a name.
6.1.1.5 An importation contains a name. The intention is that the name identifies a piece of Common Logic content represented externally to the text, and the importation re-asserts that content in the text. The notion of identification is discussed more fully in clause 6.3.1 below.
UML diagrams: Figures 1, 3
p. 12 Dialects intended for transmission of content on a network should not impose arbitrary or unnecessary restrictions on the form of names, and shall provide for certain names to be used as identifiers of Common Logic texts; that is, character strings used as identifiers in a dialect shall be parseable as Common Logic names in that dialect. Dialects intended for use on the Web should allow Universal Resource Identifiers, International Resource Identifiers and URI references to be used as names [2] [4].
p. 13 A dialect may impose particular semantic conditions on some categories of names, and apply syntactic constraints to limit where such names occur in expressions. For example, the CLIF syntax treats numerals as having a fixed denotation, and prohibits their use as identifiers.
p. 16 ... a name used to identify a phrase in Common Logic is understood to be a globally rigid identifier of that text as written (see next section), so that the same name shall not be used to refer to a different text, even if the texts have the same meaning.
Names used to name texts on a network are understood to be rigid and to be global in scope, so that the name can be used to identify the thing named – in this case, the Common Logic text – across the entire communication network. (See [8] for more full discussion.) A name which is globally attached to its denotation in this way is an identifier, and is typically associated with a system of conventions and protocols which govern the use of such names to identify, locate and transmit pieces of information across the network on which the dialect is used. While the details of such conventions are beyond the scope of this International Standard, we can summarize their effect by saying that the act of publishing a named Common Logic text is intended to establish the name as a rigid identifier of the text, and Common Logic acknowledges this by requiring that all interpretations shall conform to such conventions when they apply to the network situation in which the publication takes place.
and Section 6.3 in general.
p. 29 (Annex A) Any name assigned to a named text or a module, and any name occurring inside an importation, shall be a network identifier. For Web applications at the time of writing, it should be an IRI
Additional concrete syntax to include in Annexes (e.g. Infix)
#40 introduced the notion of a CL document. Documents are commonly retrievable in a network (e.g. downloadable from a IRI if that IRI is a URL) and therefore, quite naturally, have network identifiers.
To avoid confusion and redundancy, we suggest that this name defines the base IRI (in terms of RFC 3986/3987) of the CL document, and that all relative IRIs used for names inside this document are to be interpreted relatively to that base. (Note that so far the "foo" in (cl-text foo)
has not been interpretable as an IRI, as the base wasn't defined!)
Suppose there is a document http://example.org/repo/foo
(the issue of whether this can be a file foo.clif
is separate and purely technical; doesn't have to be discussed here).
We propose:
If this document contains an unnamed text (as defined in #40), we implicitly assume that this text has a name: the network identifier = base IRI of the document. This still allows for purely unnamed texts: They can still be created on the fly, in memory, without the notion of an enclosing document.
If this document contains named texts, their names (and likewise any other network identifiers in the document) are to be resolved against the base IRI.
This is particularly compatible with the COLORE practice of having files named foo
(actually foo.clif
) that contain a single named text
(cl-text foo)
Taking "foo" as an IRI relative to the base, it refers to "the file foo in the current directory" (sloppily spoken), whose only CL text is exactly this text.
Beyond the COLORE practice, it is possible to have documents that contain multiple named texts, e.g.
(cl-text foo)
(cl-text bar)
This is not compatible with linked data practice, a practical way of distributing ontologies on the Internet, which recommends identifying things by those IRIs=URLs from which a description of these things can be downloaded.
Therefore, in the case of multiple texts in a document, we suggest having them as fragments of that document, i.e. .../document#foo
, .../document#bar
, written as
(cl-text #foo)
(cl-text #bar)
Once we get to namespace prefixes (quite soon, as a new issue), it will be possible to abbreviate this and get rid of writing the hash.
Defect Nos.: 22
Submitter: John Sowa
References in Document: p. 44 B.2.11 p. 50 B.3.8
Nature of Defect: The colon that separates the type field
from the referent field of a concept node is
usually optional. But in the definition of the
category text, it is required.There would be no
ambiguity if it were optional, and I suggest that
the two grammar rules for text should contain
brackets around ":" .
Making the colon optional does not correct any
technical error, but it makes the grammar more
consistent by allowing colons to be optional in
all concept nodes that have a type label.
Proposed Solution:
B.2.11 text
The first line of the grammar rule should be
text = "[", [comment],
"Proposition", [":"], [CGname], CG,
B.3.8 text
The second line of the translation rule should be
text = "[", [comment] ?cm?,
"Proposition", [":"], [CGname] ?n?,
Reference in Document: p.14, 5th paragraph (Section 6.2)
Nature of Defect: mention of "universe" without qualification "of reference"
Proposed Solution: Replace
"If E is a subset of UD_I, then the restriction of I to E is an
interpretation K of the same vocabulary and over the
same universe and with int_K = int_I and seq_K = seq_I,
but where UD_K = E, rel_K(v) is the restriction of rel_I(v) to E*
and fun_K(v) is the restriction of fun_I(v) to E*->E, for all v in the vocabulary of I."
with
"If E is a subset of UD_I, then the restriction of I to E is an
interpretation K of the same vocabulary and over the
same universe of reference (UR_K = UR_I)
and with int_K = int_I and seq_K = seq_I,
but where UD_K = E, rel_K(v) is the restriction of rel_I(v) to E*
and fun_K(v) is the restriction of fun_I(v) to E*->E, for all v in the vocabulary of I."
Discussion: this clarification has bearing on Issues #24, #25 and #35. This passage indicates that even unsegregated dialects (those that do not have a syntax for functions and relations separate from that of individuals) inherently have the concept of segregated interpretations (interpretations whose universe of discourse is a proper subset of the universe of reference) if they adopt the CL abstract semantics.
Defect Nos.: 16
Submitter: Chris Angus
References in Document: Annex C
Nature of Defect: Annex C makes no mention of how to represent sequence markers
Proposed Solution: NEED SPECIFIC TEXT CHANGES HERE
Defect Nos.: 20
Submitter: Chris Angus
References in Document:
Nature of Defect: XCL allows a element to contain multiple
elements. This conflicts with the
CommentedTerm construct in the abstract syntax
which allows for a single character string to be
associated with the Term being commented. One
can argue that the abstract syntax allows
CommentedTerms to be nested, however there is no
indication of how multiple elements
would map to implicit nested Commented Terms.
Proposed Solution: NEED SPECIFIC TEXT CHANGES HERE
"A dialect may require some names to be syntactic non-discourse names, which are understood to never denote entities in the universe of discourse. This requirement may be imposed, for example, by partitioning the vocabulary or by requiring names that occur in certain syntactic positions to be non-discourse. A dialect with syntactic non-discourse names is called segregated. In segregated dialects, names which are not non-discourse names are called discourse names.
A segregated dialect shall provide sufficient syntactic constraints to guarantee that in any syntactically legal text of the dialect:
Every name shall be classified as either discourse or as non-discourse;
No name shall be classified as both discourse and non-discourse;
No non-discourse name shall be an argument of an atom or functional term.
No non-discourse name shall be bound in a quantified sentence.
As the presence of non-discourse names affects the semantics, special conditions apply to segregated dialects.
A dialect which is not segregated is called non-segregated.
"
phrase = sentence | module | (open, 'cl:imports' , interpretablename , close) | (open,
'cl:comment', quotedstring, cltext, close);
cltext = { phrase } ;
namedtext = open, 'cl:text' interpretablename, text, close ;
cltext = module | namedtext | text ;
cltext occurs twice on the left side. The last line is probably right, and refers to the root of the grammar. (But see #40 for a new proposal to have documents at the root.)
But the first occurrence of cltext should be
text = { phrase }
(Thanks to Sören Schulze for spotting this problem!)
In phrase
, the ambiguos cltext occurs on the right side. The thing that is commented upon should most likely be a list of phrases; therefore we suggest the following as a revision of the first line:
phrase = sentence | module | (open, 'cl:imports' , interpretablename , close) | (open,
'cl:comment', quotedstring, text, close);
There is one more occurrence of the ambiguous cltext
in the standard, in A.2.3.10 Module:
module = open, 'cl:module' , interpretablename , [open, 'cl:excludes' , {name} , close ] , cltext, close;
We are quite sure that this should rather be
module = open, 'cl:module' , interpretablename , [open, 'cl:excludes' , {name} , close ] , text, close;
as it does not make sense that a module, which has a name, contains texts having different, possibly unrelated names.
there is a discrepancy to the definition in Tara and my proposal, which may not be intentional.
CLIF should be changed such that conservative and definitional extensions can be formulated. The proposed solution achieving this is to merge cl-text and cl-module into one construct, and introduce syntax @name for non-discourse names.
Submitter: Pat Hayes
References in Document: p.14 4th para, 2nd sentence
Nature of Defect:
Proposed Solution: Replace “differ with” using “differ from”
After Tara's presentation on XCL2 we discussed a terminological question. In the XCL2 draft the boolean operator that is often written <--> is called "equivalence". I think we should strive for consistency across the CL standard and call it "biconditional". This would be consistent with the terminology in the 2007 version of the standard, and it matches the terminology that is used in the logic books that I am aware of. (Equivalence is usually defined as a relationship in the metalanguage.)
In relation to #38 (MIME types for CL dialects) it may also be useful to recommend (rather than prescribe) filename extensions for the CL dialects, e.g. .clif for CLIF.
Once more let's see how this is done for OWL: http://www.w3.org/TR/owl2-xml-serialization/#Appendix:_Internet_Media_Type.2C_File_Extension.2C_and_Macintosh_File_Type
How are importations across dialects resolved?
In the network we are practically using, CL texts are not free-floating but occur in documents (think: files). We suggest that that top-level unit be called "CL document", and that the listing in A.2.3.11 be replaced with the following grammar:
cldocument = { namedtext } | text ;
namedtext = open, 'cl:text' interpretablename, text, close ;
text = { phrase }
phrase = ... (as discussed previously)
For phrase
, please see #39.
The first rule is justified by the following consideration: When talking about network identifiers (i.e. IRIs) of texts inside documents (see #41 in a few minutes), it doesn't make sense to have, on top level of a document, named texts intermixed with unnamed texts, as it wouldn't be clear how to identify the unnamed stuff.
We don't need modules on cldocument
level, as phrase = ... | module
allows for having modules anyway.
Submitter: Pat Hayes
Reference in Document: p.3 - 3.8
Nature of Defect: '3.8' and 'dialect' on same line
Proposed Solution: '3.8' and 'dialect' should be on separate lines
Additional logical connectives added to the abstract syntax
Submitter: Pat Hayes
References in Document: Annexes A and B
Nature of Defect: The CLIF syntax uses several reserved names with an
enclosed colon, such as "cl:imports". It has been pointed
out by commentators that this is likely to give rise to
clashes with a widely used XML convention called
Qnaming, whereby a 'root' URI is abbreviated by a short
prefix defined in the XML header, which is prefixed to a
local name separated by a colon, such as 'rdf:type' being
an abbreviation for the full URIreference
'http://www.w3.org/1999/02/22-rdf-syntax-ns#type'.
Solution: As this 'internal colon' convention serves no real
purpose, simply replace it with hyphen. This does not
change the language essentially and would require only
minimal changes to any extant CL parsers. Since these
'words' are reserved, it is better to not use up commonly
used words such as 'text' or 'comment', so rather than
eliminate the 'cl:' prefix entirely, we propose abbreviating
it without the comma, producing entirely artificial
neologisms.
Proposed Solution: Throughout Annexes A and B, make
the following textual substitutions:
'cl-module' for 'cl:module'
'cl-excludes' for 'cl:excludes'
'cl-imports' for 'cl:imports'
'cl-text' for 'cl:text'
'cl-comment' for 'cl:comment'
'cl-roleset' for 'roleset:'
These occur on pages 27 - 31, page
52 (table B.1, line E5, second part),
page 53, lines E12, E14, E17, E19,
E20.
The semantics of cl-module should be fixed, as described in the paper:
Fabian Neuhaus, Pat Hayes: Common Logic and the Horatio problem. Applied Ontology 7(2): 211-231 (2012)
Submitter: Pat Hayes
References in Document: p.18 – 6.4 last sentence
Nature of Defect: Missing period
Proposed Solution: Replace “of the entailment” with “of the entailment.”
Informative Annex on CL proof theory
CL ontologies will be published increasingly on the Web. When publishing stuff on the Web, particularly when publishing ontologies in a linked data compliant way, it is good practice that the web server indicates, in the HTTP header, a media type for anything it makes available for download. (I can provide further reasons for this if desired.)
CL doesn't specify media types for its dialects so far.
For comparison, consider, e.g., OWL, e.g. http://www.w3.org/TR/owl2-xml-serialization/#Appendix:_Internet_Media_Type.2C_File_Extension.2C_and_Macintosh_File_Type
The different serializations of OWL have the following media types:
I suggest we come up with something like
The CL standard does not introduce any means to abbreviate long names, which frequently appear as identifiers (e.g. IRIs on the Web). A commonly-used approach for such abbreviation is to define prefixes, such as "pre" and to write a corresponding "prefixed name" as "pre:local". The expansion of the prefixed name to an unprefixed name typically involves concatenating the text associated with the prefix, often called the "namespace" with the local part of the name, sometimes with a particular character inserted in between.
a) Should the CL revision mention such namespace/prefixing mechanisms in the abstract syntax?
b) Should prefixing be introduced into any of the concrete dialects?
c) If so, what form should the namespace/prefixing mechanism take?
The semantics of cl-imports needs to be clarified: are circular imports allowed? If yes, what is their semantics?
Defect Nos.: 17
Submitter: Chris Angus
References in Document: p.59-60 C.2 2.2
Nature of Defect: The abstract syntax metamodel explicitly makes
importation a subtype of phrase, an importation may
therefore form part of a text. The XCL specification
does not allow an element as a child of the
top level element, it limits it to being a child of
a element. This would appear to prevent
XCL being syntactically fully conformant.
Proposed Solution: Allow elements within the content
of a element.
NEED SPECIFIC TEXT CHANGES HERE
Informative Annex that includes the axiomatization of useful 'structural' axioms eg arity of relations, allDifferent, etc.. which are ontologically neutral
Defect Nos.: 13, 14, 15
Submitter: Chris Angus
References in Document: p.68 C.2 3.3 , p.68 C.2 3.3.2 , p.71 C.2 3.4.2
Nature of Defect: Examples includes ‘TBD’ in place of valid XCL
elements, thus they are neither correct XCL nor
informative
Proposed Solution: Provide valid example of atomic sentence
element, or omit Example section
NEED SPECIFIC TEXT CHANGES HERE
Informative Annex that provides a reserved vocabulary for structural descriptive names (in the sense of Tarski)
Defect Nos.: 23
Submitter: nicolas.f.rouque AT jpl.nasa.gov
References in Document: pp. 28-31
A.2.3.2
A.2.3.9
A.2.3.11
Nature of Defect:
CLIF semantics specifies no interpretation for
comments
which are currently defined in terms of interpreted
names (quotedstring)
instead of interpretable names (enclosedname)
A.2.3.9 affects Table A.1, p.30, the unnamed entry
between E12 and E13 which
defines the interpretation for an expression of the
form:
A sentence (cl:comment "string" P) is I(P)
This sentence expression is not syntactically valid
according to A.2.3.9:
commentsent = open, 'cl:comment', quotedstring ,
sentence , close ;
because A.2.2.2 and A.2.2.5 define, respectively:
stringquote = ''';
quotedstring = stringquote, { ... }, stringquote ;
A.2.3.11 affects Table A.1, p.31, the unnamed entry
between E14 and E17
which defines the interpretation for an expression of
the form:
A phrase (cl:comment "string") is: true
This sentence expression is not syntactically valid
according to A.2.3.11 for similar reason as above:
phrase = sentence | module | (open, 'cl:imports' ,
interpretablename ,
close) | (open, 'cl:comment', quotedstring, cltext,
close);syntax/semantic inconsistency for comment
sentences & comment
phrases
(see clause 10 in:
http://www.omg.org/cgi-bin/doc?ad/08-05-02)
The syntax of commented sentences (A.2.3.9) and
phrases (A.2.3.11) are in conflict with the key
principle governing the non interpretation of
comments in CLIF semantics succinctly stated in
6.2, on p. 16:
Proposed Solution:
A.2.3.9: commentsent = open, 'cl:comment',
quotedstring , sentence , close ;
It should be changed to a definition that uses an
interpretable name
instead:
A.2.3.9: commentsent = open, 'cl:comment',
enclosedname , sentence , close ;
Similarly, A.2.3.11 is also inconsistent with the
principle stated in 6.2:
A.2.3.11: phrase = sentence | module | (open,
'cl:imports' ,
interpretablename ,
close) | (open, 'cl:comment', quotedstring,
cltext, close);
It too should be changed to a definition that
uses an interpretable name
instead:
A.2.3.11: phrase = sentence | module | (open,
'cl:imports' ,
interpretablename ,
close) | (open, 'cl:comment', enclosedname [
cltext ], close);
Submitter: Pat Hayes
References in Document: p.20 – 6.6.1 last sentence
Nature of Defect:
Proposed Solution: Boldface “shall”
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.