ISO/IEC 24707:2018
(Main)Information technology — Common Logic (CL) — A framework for a family of logic-based languages
Information technology — Common Logic (CL) — A framework for a family of logic-based languages
This document specifies a family of logic languages designed for use in the representation and interchange of information and data among disparate computer systems. The following features are essential to the design of this document. — Languages in the family have declarative semantics. It is possible to understand the meaning of expressions in these languages without appeal to an interpreter for manipulating those expressions. — Languages in the family are logically comprehensive ? at its most general, they provide for the expression of arbitrary first-order logical sentences. — Languages in the family are translatable by a semantics-preserving transformation to a common XML-based syntax, facilitating interchange of information among heterogeneous computer systems. The following are within the scope of this document: — representation of information in ontologies and knowledge bases; — specification of expressions that are the input or output of inference engines; — formal interpretations of the symbols in the language. The following are outside the scope of this document: — specification of proof theory or inference rules; — specification of translators between the notations of heterogeneous computer systems; — computer-based operational methods of providing relationships between symbols in the logical "universe of discourse" and individuals in the "real world". This document describes Common Logic's syntax and semantics. This document defines an abstract syntax and an associated model-theoretic semantics for a specific extension of first-order logic. The intent is that the content of any system using first-order logic can be represented in this document. The purpose is to facilitate interchange of first-order logic-based information between systems. Issues relating to computability using this document (including efficiency, optimization, etc.) are not addressed.
Technologies de l'information — Logique Commune (CL) — Cadre pour une famille des langages logique-basés
General Information
Relations
Standards Content (Sample)
INTERNATIONAL ISO/IEC
STANDARD 24707
Second edition
2018-07
Information technology — Common
Logic (CL) — A framework for a family
of logic-based languages
Technologies de l'information — Logique Commune (CL) — Cadre
pour une famille des langages logique-basés
Reference number
©
ISO/IEC 2018
© ISO/IEC 2018
All rights reserved. Unless otherwise specified, or required in the context of its implementation, no part of this publication may
be reproduced or utilized otherwise in any form or by any means, electronic or mechanical, including photocopying, or posting
on the internet or an intranet, without prior written permission. Permission can be requested from either ISO at the address
below or ISO’s member body in the country of the requester.
ISO copyright office
CP 401 • Ch. de Blandonnet 8
CH-1214 Vernier, Geneva
Phone: +41 22 749 01 11
Fax: +41 22 749 09 47
Email: copyright@iso.org
Website: www.iso.org
Published in Switzerland
ii © ISO/IEC 2018 – All rights reserved
Contents Page
Foreword .iv
Introduction .v
1 Scope . 1
2 Normative references . 1
3 Terms and definitions . 2
4 Symbols and abbreviated terms . 4
4.1 Symbols . 4
4.2 Abbreviated terms . 5
5 Requirements and design overview . 5
5.1 Requirements . 5
5.1.1 Common Logic should include full first-order logic with equality . 5
5.1.2 Common Logic should provide a general-purpose syntax for
communicating logical expressions . 5
5.1.3 Common Logic should be easy and natural for use on the Web . 5
5.1.4 Common Logic should support open networks . 6
5.1.5 Common Logic should not make arbitrary assumptions about semantics . 6
5.2 A family of languages . 6
6 Common Logic abstract syntax and semantics . 6
6.1 Common Logic abstract syntax . 6
6.1.1 Abstract syntax categories . 6
6.1.2 Metamodel of the Common Logic abstract syntax . 8
6.1.3 Importation closure .15
6.1.4 Abstract syntactic structure of dialects .16
6.2 Common logic semantics .17
6.3 Datatypes .19
6.4 Satisfaction, validity and entailment .20
6.5 Sequence markers, recursion and argument lists: discussion .20
6.6 Special cases and translations between dialects .21
7 Conformance .21
7.1 Dialect conformance .21
7.1.1 Syntax .21
7.1.2 Semantics .22
7.1.3 Presupposing dialects .23
7.2 Application conformance .24
7.3 Network conformance .24
Annex A (normative) Common Logic Interchange Format (CLIF) .25
Annex B (normative) Conceptual Graph Interchange Format (CGIF) .36
Annex C (normative) eXtended Common Logic Markup Language (XCL) .57
Annex D (informative) Translating between dialects .69
Bibliography .70
© ISO/IEC 2018 – All rights reserved iii
Foreword
ISO (the International Organization for Standardization) and IEC (the International Electrotechnical
Commission) form the specialized system for worldwide standardization. National bodies that are
members of ISO or IEC participate in the development of International Standards through technical
committees established by the respective organization to deal with particular fields of technical
activity. ISO and IEC technical committees collaborate in fields of mutual interest. Other international
organizations, governmental and non-governmental, in liaison with ISO and IEC, also take part in the
work. In the field of information technology, ISO and IEC have established a joint technical committee,
ISO/IEC JTC 1.
The procedures used to develop this document and those intended for its further maintenance are
described in the ISO/IEC Directives, Part 1. In particular the different approval criteria needed for the
different types of ISO documents should be noted. This document was drafted in accordance with the
editorial rules of the ISO/IEC Directives, Part 2 (see www .iso .org/directives).
Attention is drawn to the possibility that some of the elements of this document may be the subject of
patent rights. ISO shall not be held responsible for identifying any or all such patent rights. Details of
any patent rights identified during the development of the document will be in the Introduction and/or
on the ISO list of patent declarations received (see www .iso .org/patents).
Any trade name used in this document is information given for the convenience of users and does not
constitute an endorsement.
For an explanation on the voluntary nature of standards, the meaning of ISO specific terms and
expressions related to conformity assessment, as well as information about ISO's adherence to the
World Trade Organization (WTO) principles in the Technical Barriers to Trade (TBT) see the following
URL: www .iso .org/iso/foreword .html.
This document was prepared by Technical Committee ISO/IEC JTC 1, Information technology, SC 32,
Data management and interchange.
This second edition cancels and replaces the first edition (ISO/IEC 24707:2007), which has been
technically revised.
The main changes compared to the previous edition are as follows:
— the list of syntactic errors that have already been identified in the Defect Report has been fixed;
— the XML syntax in Annex C has been corrected and completed;
— a more general approach to annotation of CL-texts has been made;
— semantics has been modified to allow the existence of definitional extensions in CL;
— support for circular imports;
— semantics of CL-module have been clarified;
— clarification of the distinction between segregated and non-segregated dialects;
— clarification of conformance conditions has been made.
Any feedback or questions on this document should be directed to the user’s national standards body. A
complete listing of these bodies can be found at www .iso .org/members .html.
iv © ISO/IEC 2018 – All rights reserved
Introduction
Common Logic is a logic framework intended for information exchange and transmission. The
framework allows for a variety of different syntactic forms, called dialects, all translatable by a
semantics-preserving transformation to a common XML-based syntax.
Common Logic has some novel features, chief among them being a syntax which permits “higher-
order” constructions, such as quantification over classes or relations while preserving a first-order
model theory, and a semantics which allows theories to describe intentional entities such as classes or
properties. It also has provision for the use of datatypes and for naming, importing and transmitting
content on the World Wide Web using XML.
© ISO/IEC 2018 – All rights reserved v
INTERNATIONAL STANDARD ISO/IEC 24707:2018(E)
Information technology — Common Logic (CL) — A
framework for a family of logic-based languages
1 Scope
This document specifies a family of logic languages designed for use in the representation and
interchange of information and data among disparate computer systems.
The following features are essential to the design of this document.
— Languages in the family have declarative semantics. It is possible to understand the meaning of
expressions in these languages without appeal to an interpreter for manipulating those expressions.
— Languages in the family are logically comprehensive – at its most general, they provide for the
expression of arbitrary first-order logical sentences.
— Languages in the family are translatable by a semantics-preserving transformation to a common
XML-based syntax, facilitating interchange of information among heterogeneous computer systems.
The following are within the scope of this document:
— representation of information in ontologies and knowledge bases;
— specification of expressions that are the input or output of inference engines;
— formal interpretations of the symbols in the language.
The following are outside the scope of this document:
— specification of proof theory or inference rules;
— specification of translators between the notations of heterogeneous computer systems;
— computer-based operational methods of providing relationships between symbols in the logical
“universe of discourse” and individuals in the “real world”.
This document describes Common Logic’s syntax and semantics.
This document defines an abstract syntax and an associated model-theoretic semantics for a specific
extension of first-order logic. The intent is that the content of any system using first-order logic can
be represented in this document. The purpose is to facilitate interchange of first-order logic-based
information between systems.
Issues relating to computability using this document (including efficiency, optimization, etc.) are not
addressed.
2 Normative references
The following documents are referred to in the text in such a way that some or all of their content
constitutes requirements of this document. For dated references, only the edition cited applies. For
undated references, the latest edition of the referenced document (including any amendments) applies.
ISO/IEC 2382:2015, Information technology — Vocabulary
ISO/IEC 10646:2014, Information technology — Universal Coded Character Set (UCS)
ISO/IEC 14977:1996, Information technology — Syntactic metalanguage — Extended BNF
© ISO/IEC 2018 – All rights reserved 1
3 Terms and definitions
For the purposes of this document, the following terms and definitions apply.
ISO and IEC maintain terminological databases for use in standardization at the following addresses:
— IEC Electropedia: available at http: //www .electropedia .org/
— ISO Online browsing platform: available at https: //www .iso .org/obp
3.1
axiom
any sentence (3.15), statement or text which is assumed to be true, or from which others are derived, or
by which they are entailed
Note 1 to entry: In a computational setting, an axiom is a sentence which is never posed as a goal to be proved,
but only used to prove other sentences.
3.2
conceptual graph
CG
graphical or textual display of symbols arranged according to the style of conceptual graph theory (3.3)
3.3
conceptual graph theory
form of first-order logic which represents existential quantification and conjunction via the assertion
of logical constructs called concepts and relations which are arranged in an abstract or visually
displayed graph
3.4
CLIF
text-based first-order formalism using a LISP-like list notation
Note 1 to entry: This is one of the concrete syntaxes for Common Logic (described in Annex A).
Note 2 to entry: CLIF is a KIF-based syntax that is used for illustration purposes in this document. KIF, introduced
[3]
by Mike Genesereth , originated with the Knowledge Sharing Effort sponsored by the U.S. DARPA. The name
“KIF” is not used for this syntax in order to distinguish it from the commonly used KIF dialects. No assumptions
are made in this document with respect to KIF semantics; in particular, no equivalence between CLIF and KIF is
intended.
Note 3 to entry: Historically, CLIF was an acronym for Common Logic Interchange Format. However, CLIF does
not hold a privileged position among Common Logic dialects (3.7), as the expanded name suggests. Further, XCL is
the recommended interchange format on the Web.
3.5
Conceptual Graph Interchange Format
CGIF
text version of conceptual graphs (3.2)
Note 1 to entry: Sometimes, this may refer to an example of a character string that conforms to Annex B, intended
to convey exactly the same structure and semantics as an equivalent conceptual graph.
3.6
denotation
relationship holding between a name or expression and the thing to which it refers
Note 1 to entry: Also used with “of” to mean the thing being named, i.e. the referent of a name or expression.
2 © ISO/IEC 2018 – All rights reserved
3.7
Common Logic dialect
concrete instance of Common Logic syntax that shares (at least some of) the uniform semantics of
Common Logic
Note 1 to entry: A dialect may be textual or graphical or possibly some other form. A dialect, by definition, is also
a conforming language (see 7.1 for further details).
3.8
eXtensible Common Logic Markup Language
XCL
XML-based syntax for Common Logic
3.9
individual
one element of the universe of discourse (3.17) of an interpretation (3.12)
Note 1 to entry: The universe of discourse of an interpretation is the set of all of its individuals.
3.10
internationalized resource identifier
IRI
string of Unicode characters intended for use as an Internet network identifier syntax which can
accommodate a wide variety of international character forms
3.11
inscription
structure of symbols that may be either linear or graphic
3.12
interpretation
formal specification of the meanings of the names in a vocabulary of a Common Logic dialect (3.7) in
terms of a universe of reference (3.18)
Note 1 to entry: A Common Logic interpretation, in turn, determines the semantic values of all complex
expressions of the dialect, in particular, the truth values of its sentences (3.15), statements and texts.
Note 2 to entry: See 6.2 for a more precise description of how an interpretation is defined.
3.13
operator
distinguished syntactic role played by a specified component within a functional term (3.16)
Note 1 to entry: The denotation (3.6) of a functional term in an interpretation (3.12) is determined by the
functional extension of the denotation of the operator together with the denotations of the arguments.
3.14
predicate
distinguished syntactic role played by exactly one component within a simple
sentence (3.15)
Note 1 to entry: The truth value of a simple sentence in an interpretation (3.12) is determined by the relational
extension of the denotation (3.6) of the predicate together with the denotations of the arguments.
3.15
sentence
expression in the syntactic form of a traditional first-order logical formula
EXAMPLE A simple sentence (see 6.1.1.15), Boolean sentence (see 6.1.1.14) or quantification (see 6.1.1.13).
© ISO/IEC 2018 – All rights reserved 3
3.16
term
expression which denotes an individual (3.9), consisting of either a name or,
recursively, a functional term applied to a sequence of arguments, which are themselves terms
Note 1 to entry: Languages for traditional first-order logic specifically exclude predicate (3.14) quantifiers and
the use of the same name in both predicate and argument position in simple sentences (3.15), both of which are
permitted (though not required) in Common Logic. Languages for traditional first-order logic fall within the
category of presupposing CL dialect, with a discourse presupposition of “non-discourse” for all names used as
function operators (3.13) or predicates, and “discourse” for all names used as the arguments of functional terms
or simple sentences or as bindings.
3.17
universe of discourse
domain of discourse
set of all the individuals (3.9) in an interpretation (3.12), i.e. the set over which the quantifiers range
Note 1 to entry: Required to be a subset of the universe of reference (3.18) and may be identical to it.
3.18
universe of reference
set of all the things needed to define the meanings of logical expressions in an interpretation (3.12)
Note 1 to entry: Required to be a superset of the universe of discourse (3.17) and may be identical to it.
4 Symbols and abbreviated terms
4.1 Symbols
fun mapping from UR to functions from UD * to UD
I I I I
I interpretation in the model-theoretic sense
int mapping from names in a vocabulary V to UR ; informally, a means of associating names in V
I I
to referents in UR
I
rel mapping from UR to subsets of UD *
I I I
seq mapping from sequence markers in V to UD *
I I
λ lexicon, which consists of a vocabulary, a set of sequence markers (Smark), and a set of
titles (Ttl)
V vocabulary, which is a set of names
Smark set of sequence markers
Ttl set of titles
UD universe of discourse; a non-empty set of individuals that an interpretation I is “about” and
I
over which the quantifiers are understood to range
UR universe of reference, i.e. the set of all referents of names in an interpretation I
I
X* set of finite sequences of the elements of X, for any set X. Thus, X* = { | x ,…,x ∈ X},
1 n 1 n
for any n ≥ 0. Note that the empty sequence is in X*, for any X.
4 © ISO/IEC 2018 – All rights reserved
4.2 Abbreviated terms
CL Common Logic
DF display form
EBNF Extended Backus-Naur Format (as in ISO/IEC 14977)
FO first-order
KIF Knowledge Interchange Format
OWL Web Ontology Language
RDF Resource Description Framework
RDFS Resource Description Framework Schema
TFOL traditional first-order logic
XML eXtensible Markup Language
5 Requirements and design overview
5.1 Requirements
5.1.1 Common Logic should include full first-order logic with equality
Common Logic abstract syntax and semantics shall provide for the full range of first-order syntactic
forms with their usual meanings. Any traditional first-order syntax will be directly translatable into
Common Logic without loss of information or alteration of meaning.
5.1.2 Common Logic should provide a general-purpose syntax for communicating logical
expressions
a) There should be a single XML syntax for communicating Common Logic content on the Web.
b) Common Logic languages should be able to express various commonly used “syntactic sugarings”
for logical forms or commonly used patterns of logical sentences.
c) The Common Logic abstract syntax should relate to existing conventions; in particular, it should be
capable of rendering any content expressible in RDF, RDFS or OWL.
d) There should be at least one human-readable presentation syntax defined which can be used to
express the entire language.
5.1.3 Common Logic should be easy and natural for use on the Web
a) The XML syntax should be compatible with the published specifications for XML, IRI syntax, XML
Schema, Unicode and other conventions relevant to transmission of information on the Web.
b) IRIs should be usable as names in the language.
c) IRIs should be usable to title texts and label expressions, in order to facilitate Web operations such
as retrieval, importation and cross-reference.
© ISO/IEC 2018 – All rights reserved 5
5.1.4 Common Logic should support open networks
a) Transmission of content between Common Logic-aware agents should not require negotiation
about syntactic roles of symbols or translations between syntactic roles.
b) Any piece of Common Logic text should have the same meaning, and support the same entailments,
everywhere on the network. Every name should have the same logical meaning at every node of the
network.
c) No agent should be able to limit the ability of another agent to refer to anything or to make
assertions about anything.
d) The language should support ways to refer to a local universe of discourse and be able to relate it to
other such universes.
e) Users of Common Logic should be free to invent new names and use them in published Common
Logic content.
5.1.5 Common Logic should not make arbitrary assumptions about semantics
a) Common Logic does not make gratuitous or arbitrary assumptions about logical relationships
between different expressions.
b) If possible, Common Logic agents should express these assumptions in Common Logic directly.
5.2 A family of languages
This subclause describes what is meant by a “family” of languages and gives some of the rationale
behind the development of Common Logic.
Following the convention whereby any language has a grammar, then Common Logic is a family
of languages rather than a single language. Different Common Logic languages, referred to in this
document as dialects, may differ sharply in their surface syntax, but they have a single uniform
semantics and can all be transcribed into the common abstract syntax. Membership in the family is
defined by being inter-translatable with the other dialects while preserving meaning, rather than by
having any particular syntactic form. Several existing logical notations and languages, therefore, can
be considered to be Common Logic dialects.
A Common Logic dialect called CLIF based on KIF (see Annex A) is used in giving examples throughout
[3]
this document. CLIF can be considered an updated and simplified form of KIF 3.0 and hence a
[1]
separate language in its own right. Conceptual graphs are also a well-known form of first-order logic
for machine processing; the CGIF language is specified in Annex B. An exactly conformant XML Dialect,
called XCL, is specified in Annex C, for the purpose of satisfying requirements 5.1.2 a) and 5.1.3 a).
6 Common Logic abstract syntax and semantics
6.1 Common Logic abstract syntax
6.1.1 Abstract syntax categories
6.1.1.1 Terms, sequence markers, sentences, statements and texts are well-formed expressions.
6.1.1.2 A text is a text construction, domain restriction, or importation.
6.1.1.3 A text construction contains a set, list or bag of sentences, statements and/or texts. A Common
Logic text may be a sequence, a set or a bag of sentences, statements and/or texts; dialects may
specify which is intended or leave this undefined. Re-orderings and repetitions of arguments of a text
6 © ISO/IEC 2018 – All rights reserved
construction are semantically irrelevant. However, applications which transmit or re-publish Common
Logic text shall preserve the structure of text constructions, since other applications are allowed to utilize
the structure for other purposes, such as indexing. If a dialect imposes conditions on text constructions,
then these conditions shall be preserved by conforming applications. A text construction may be empty.
6.1.1.4 A domain restriction consists of a term and a text called the body text. The term indicates the
“local” universe of discourse in which the text is understood.
6.1.1.5 An importation contains a title. The intention is that the title provides an identifier to an
external Common Logic text, and that the importation re-asserts that external text in the importing text.
6.1.1.6 An axiom is a statement, sentence or text.
6.1.1.7 A statement is either a discourse statement or a titling.
6.1.1.8 A discourse statement is either an out-of-discourse statement or an in-discourse statement.
6.1.1.9 An out-of-discourse statement contains a sequence of terms.
6.1.1.10 An in-discourse statement contains a sequence of terms.
6.1.1.11 A titling contains a name and a text. The titling assigns a title to a text. Titles are often IRIs,
which identify the text as resource.
6.1.1.12 A sentence is either a quantified sentence or a Boolean sentence or a simple sentence.
6.1.1.13 A quantified sentence has (i) a type, called a quantifier, (ii) a finite, nonrepeating sequence
of interpretable names 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. The abstract syntax
distinguishes the universal and the existential types of quantified sentence. A name which occurs in the
binding sequence is said to be bound in the body. Any name or sequence marker which is not bound in
the body is said to be free in the body.
6.1.1.14 A Boolean sentence has a type, called a connective, and a number of sentences called the
components of the Boolean sentence. The number depends on the particular type. The abstract syntax
distinguishes five types of Boolean sentences: conjunctions and disjunctions, which have any number
of components, implications and biconditionals, which have exactly two components, and negations,
which have exactly one component. The two components of an implication fill different roles; one is the
antecedent and the other is the consequent.
6.1.1.15 A simple sentence is either an equation containing two arguments, which are terms, or is an
atomic sentence, which consists of a term, called the predicate, and a term sequence called the argument
sequence, the elements of which are called arguments of the atomic sentence.
6.1.1.16 A term is either a name or a functional term. A term may have an attached comment. Further,
every name is a term.
6.1.1.17 A functional term consists of a term, called the operator, and a term sequence called the
argument sequence, the elements of which are called arguments of the functional term.
6.1.1.18 A term sequence is a finite sequence of terms and/or sequence markers. Term sequences
may be empty, but a functional term with an empty argument sequence shall not be identified with
its operator, and an atomic sentence with an empty argument sequence shall not be identified with its
predicate.
© ISO/IEC 2018 – All rights reserved 7
6.1.1.19 A lexicon is a set of names (i.e. the vocabulary of the lexicon), a set of sequence markers, and a
set of titles.
6.1.1.20 Irregular sentences in a concrete syntax are parsed into the abstract syntax as propositions
(i.e. nullary atomic sentences) with a new name for the predicate. In this way, irregular sentences can be
nested within texts, statement and (otherwise) regular compound sentences, and the semantics of the
resulting expressions is determined as usual from Table 2.
6.1.1.21 A comment is a piece of data. Any number of comments may be attached to well-formed
expressions that are texts, statements, sentences or functional terms, but not to names, sequence markers
or other comments. No particular restrictions are placed on the nature of Common Logic comments; in
particular, a comment may be Common Logic text. Particular dialects may impose conditions on the form
of comments.
6.1 completely describes the abstract syntactic structure of Common Logic. Any fully conformant
Common Logic dialect shall provide an unambiguous syntactic representation for each of the above
types of well-formed expressions.
Sentence types are commonly indicated by the inclusion of explicit text strings, such as “forall” for
universal sentence and “and” for conjunction. However, no conditions are imposed on how the various
syntactic categories are represented in the surface forms of a dialect. In particular, expressions in a
dialect are not required to consist of character strings.
6.1.2 Metamodel of the Common Logic abstract syntax
6.1.2.1 Names and sequence markers
The class of names and sequence markers of a Common Logic language is the classes obtained from
strings using the following operators:
— Voc : String → V
— Seqmark : String → Smark
— Titling : String → Ttl
— Binder = V ∪ Smark
6.1.2.2 Terms and term sequences
The class of terms of a Common Logic language is the class Term that includes all names in V and all
functional terms. The class of functional terms of a Common Logic language is the class FunctionalTerm
obtained by the recursive application of the operator Func to pairs made up of one term and one term
sequence. The class of term sequences of a Common Logic language is the class TermSequence that
includes all finite sequences of terms and/or sequence markers.
— F unc: Ter m × TermSequence → FunctionalTerm
— Term = V ∪ FunctionalTerm
— TSeq:(Term ∪ Smark) × . × (Term ∪ Smark) → TermSequence
6.1.2.3 Sentences
The class of sentences of a Common Logic language is the class Sentence that includes all simple
sentences (including equations, if applicable) formed by the application of the operation(s) Atomic (and
Id) from well-formed terms and term sequences and all compound sentences formed by the recursive
8 © ISO/IEC 2018 – All rights reserved
application of the set of operations Neg, Conj, Disj, Cond, BiCond, EQuant, and UQuant that satisfy the
following conditions:
— each operation is one-to-one;
— the range of the operations is pairwise disjoint and disjoint from the set of terms of λ.
— Atomic: Term × TermSequence → Sentence
— Id: Term × Term → Sentence
— Neg:S entence → Sentence
— Conj : Sentence × . × Sentence → Sentence
— Disj : Sentence × . × Sentence → Sentence
— Cond : Sentence × Sentence → Sentence
— BiCond:S entence × Sentence → Sentence
— EQuant: Binder × . × Binder × Sentence → Sentence, n ≥ 0
— UQuant: Binder × . × Binder × Sentence → Sentence, n ≥ 0
Figure 1 — Abstract syntax of texts
© ISO/IEC 2018 – All rights reserved 9
Figure 2 — Abstract syntax of text constructions
Figure 3 — Abstract syntax of statements
10 © ISO/IEC 2018 – All rights reserved
Figure 4 — Abstract syntax of terms
© ISO/IEC 2018 – All rights reserved 11
Figure 5 — Abstract syntax of a simple sentence
12 © ISO/IEC 2018 – All rights reserved
Figure 6 — Abstract syntax of sentences
Figure 7 — Abstract syntax of Boolean sentences
© ISO/IEC 2018 – All rights reserved 13
Figure 8 — Abstract syntax of a quantified sentence
6.1.2.4 Statements
The class of statements of a Common Logic language is the class Statement obtained from the recursive
application of operations outDiscourse, inDiscourse, and title under the following conditions:
— outDiscourse: TermSequence → DiscourseStatement
— inDiscourse: TermSequence → DiscourseStatement
— title : T t l × Text → Titling
Discourse statements and titlings are statements:
—
Statement = DiscourseStatement ∪ Titling
6.1.2.5 Texts
The class of texts of a Common Logic language is the class Text that is obtained from the recursive
application of the set of operations txt, imports, and domain under the following conditions:
— txt:(Sentence ∪ Statement ∪ Text) × . × (Sentence ∪ Statement ∪ Text) → TextConstruction
— imports: Ttl → Importation
— domain: Term × Text → DomainRestriction
Text Constructions, domain restrictions, and importations are texts:
—
Text = TextConstruction ∪ DomainRestriction ∪ Importation
14 © ISO/IEC 2018 – All rights reserved
Figure 9 — Abstract syntax of text constructions
package CL [ 10 Well-formed Expressions ]
WellFormedExpression
Term SequenceMarker Sentence Statement Text
Figure 10 — Abstract syntax of well-formed expressions
6.1.2.6 Well-Formed Expressions
Terms, sequence markers, sentences, sfitatements, and texts are well-formed expressions:
—
Wfe = Term ∪ SequenceMarker ∪ Sentence ∪ Statement ∪ Text
6.1.2.7 Metamodel
Figures 1 to 9 provide a non-normative metamodel showing relationships among the syntactic
categories.
6.1.3 Importation closure
An untitled importation in a text is an occurrence of an importation expression that is not a descendant
of a titling in the abstract syntax tree as defined in 6.1.2.
© ISO/IEC 2018 – All rights reserved 15
A corpus is a set of texts in the Common Logic abstract syntax. A corpus may be empty, finite, or infinite.
An importation fixed-point under a title mapping ttl is a corpus C such that if G is a text in C, then
C contains every text G' derived from G by replacing one occurrence of an untitled importation with
name N by the text which is the value ttl(N) of the title mapping. The importation closure of a corpus C
under a title mapping ttl is the intersection of all importation fixed-points under ttl that contain C. The
importation closure of every non-empty corpus in a Common Logic language is non-empty.
6.1.4 Abstract syntactic structure of dialects
Dialects may, in addition, provide for other forms of sentence construction not described by this syntax,
but in order to be fully conformant, such constructions shall either be new categories defined in terms
of these categories or be extensions of these categories (e.g. new kinds of Boolean sentence, or kinds
of quantifier) which are equivalent in meaning to a construction using just this syntax, interpreted
according to the Common Logic semantics; that is, they can be considered to be systematic abbreviations
or macros, also known as “syntactic sugar”. The CLIF dialect (described in Annex A) and XCL (described
in Annex C) contain a number of syntactic sugared forms for quantified and atomic sentences. (Other
types of compliance are also recognized: see Clause 7 for a full account of conformance.)
The only undefined terms in the abstract syntax clause are name, sequence marker, and title. The
only required syntactic constraint on the basic lexical categories of name and sequence marker is
that they shall be exclusive. 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 titles of Common Logic texts. Dialects intended for use on the Web should allow
[2][4]
Internationalized Resource Identifiers to be used as names . Common Logic dialects should define
names in terms of Unicode (ISO/IEC 10646) conventions.
There is no notion of “bound variable” in the CL abstract syntax. Names that can occur bound are not
required to be lexically distinguished from those that can (only) occur free, nor are names required
to be partitioned into distinct classes such as relation, function or individual names. There are no
sortal restrictions on names. Particular Common Logic dialects may make these or other distinctions
between subclasses of names, and impose extra restrictions on the occurrence of types of names or
terms in expressions — for example, by requiring that names that can occur bound (i.e. the variables
of traditional first-order languages) be written with a special prefix, as in KIF, or with a particular
style, as in Prolog; or by requiring that operators be in a distinguished category of relation names, as in
traditional first-order syntax.
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 and XCL syntaxes
treat numerals as having a fixed denotation and prohibit their use as titles.
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 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 a simple sentence or functional term, and
— no non-discourse name shall be bound in a quantified sentence.
A dialect may have additional mechanisms for embedding information within CL texts that may be
deleted without affecting the parsing of the text into the abstract syntax and may be omitted during the
translation into other concrete dialects.
16 © ISO/IEC 2018 – All rights reserved
6.2 Common logic semantics
The semantics of Common Logic is defined in terms of a satisfaction relation between Common Logic
text and mathematical structures called interpretations.
An interpretation I of a Common Logic language L with lexicon λ = (V , Smark , Ttl ) (where V ⊆ V,
λ λ λ λ
Smark ⊆ Smark, Ttl ⊆ Ttl) is a set UR , the universe of reference, with a distinguished subset UD , the
λ λ I I
universe of discourse, and five mappings:
— int from names in V to UR ;
I λ I
— rel from UR to the power set of UD *;
I I I
— fun from UR to total functions from UR * into UR ;
I I I I
— seq from sequence markers in Smark to UR *;
I λ I
— a title mapping ttl from Ttl to texts of L.
I λ
If UD is non-empty and the range of fun is total functions from UD * into UD , then it can be said that I
I I I I
is a core interpretation of L.
Intuitively, UD is the universe or domain of discourse containing all the individual things the
I
interpretation is “about” and over which the quantifiers range. UR is a potentially larger set of things
I
that might also contain entities which are not in the universe of discourse. In particular, UR might
I
contain relations not in UD to serve as the interpretations of the non-discourse names. All names are
I
interpreted in the same way, whether or not they are understood to denote something in the universe of
discourse; that is why there is only a single interpretation mapping that applies to all names regardless
of their syntactic role. In particular, rel (x) is in UD * even when x is not in UD . When considering only
I I I
classical dialects, the elements of the universe of reference which are outside the universe of discourse
may be identified with their corresponding values of the rel and fun mappings, which are then re-
I I
interpreted to be the identity mapping. The resulting construction maps predicates directly to relations
and operators to functions, yielding a more traditional interpretation structure for the segregated
syntax of traditional first-order logic.
Although sequence markers are mapped into finite sequences in an interpretation, these sequences are
not denoted by names, and so are not required to be in the universe of reference.
The assignment of semantic values to complex expressions — notably, the assignment of truth values to
sentences — requires some auxiliary definitions.
Let S be a subset of V ∪ Smark. An interpretation J of V is an S-variant of I if it is exactly like I except that
int and seq might differ with int and seq on what they assign to the members of S. More formally, J is
J J I I
an S-variant of I if UR = UR , UD = UD , rel = rel , fun = fun , ttl = ttl , int (n) = int (n) for names n ∉ S,
J I J I J I J I I J J I
int (n) ∈ UD for names n ∈ S, seq (s) = seq (s) for sequence markers s ∉ S, and seq (s) ∈ UD* for s ∈ S.
I J J I J J
If E is a subset of UD , then the restriction of I to E is an interpretation K of the same language L and over
I
the same universe of reference and with int = int and seq = seq , but where UD = E, rel (v) is the
K I K I K K
restriction of rel (v) to E* and fun (v) = fun (v) for all v in the vocabulary
...
Questions, Comments and Discussion
Ask us and Technical Secretary will try to provide an answer. You can facilitate discussion about the standard in here.
Loading comments...