ࡱ > @ i jbjbqq B 6W j l 2 2 2 2 2 2 2 4 ! ! ! ! h *" l $ ! R ) B p C C C JD 2V T [ , / O b , 2 2^ FD JD 2^ 2^ , ~ 2 2 C C 4 ) ~ ~ ~ 2^ 2 C 2 C | ~ f . . 2 2 2 2 2^ ~ ~ 0 2 2 f z' + ! ! ~ \ f z ~ f ~ ISO/IEC JTC 1/SC32N 1132
2004-06-07
ISO/WD24707
ISO/JTC 1/SC32/WG2
ANSI
Information technology Common Logic (CL) Framework for a family of logic-based languages
Editors note
Need a French title
Document type: International standard
Document subtype:
Document stage: (20) Preparation
Document language: E
Warning
This document is not an ISO International Standard. It is distributed for review and comment. It is subject to change without notice and may not be referred to as an International Standard.
Recipients of this draft are invited to submit, with their comments, notification of any relevant patent rights of which they are aware and to provide supporting documentation.
Copyright notice
This ISO document is a working draft or committee draft and is copyright-protected by ISO. While the reproduction of working drafts or committee drafts in any form for use by participants in the ISO standards development process is permitted without prior permission from ISO, neither this document nor any extract from it may be reproduced, stored or transmitted in any form for any other purpose without prior written permission from ISO.
Requests for permission to reproduce this document for the purpose of selling it should be addressed as shown below or to ISOs member body in the country of the requester:
[Indicate :
the full address
telephone number
fax number
telex number
and electronic mail address
as appropriate, of the Copyright Manager of the ISO member body responsible for the secretariat of the TC or SC within the framework of which the draft has been prepared]
Reproduction for sales purposes may be subject to royalty payments or a licensing agreement.
Violators may be prosecuted.
Contents Page
TOC \o "1-3" 1 Scope PAGEREF _Toc484628858 \h 1
2 Normative references PAGEREF _Toc484628859 \h 2
3 Terms and definitions PAGEREF _Toc484628860 \h 2
4 Symbols (and abbreviated terms) PAGEREF _Toc484628861 \h 3
5 Overview PAGEREF _Toc484628862 \h 4
6 Common Logic Core PAGEREF _Toc484628863 \h 5
6.1 Common Logic Core Syntax PAGEREF _Toc484628864 \h 5
6.1.1 Lexical syntax PAGEREF _Toc484628865 \h 6
6.1.2 Core expression syntax PAGEREF _Toc484628866 \h 8
6.2 Common Logic Core Semantics PAGEREF _Toc484628867 \h 9
6.2.1 Interpretations PAGEREF _Toc484628868 \h 9
6.2.2 Discussion PAGEREF _Toc484628869 \h 13
6.2.3 Special name interpretations PAGEREF _Toc484628870 \h 15
6.2.4 Common Logic satisfaction and entailment PAGEREF _Toc484628871 \h 16
7 The Common Logic Kernel PAGEREF _Toc484628872 \h 17
7.1 Special Cases leave until later? PAGEREF _Toc484628873 \h 18
7.2 Common Logic atoms and terms: discussion PAGEREF _Toc484628874 \h 19
7.2.1 Sequence variables, recursion and argument lists PAGEREF _Toc484628875 \h 19
7.2.2 Role-set syntax, eventualities and selections PAGEREF _Toc484628876 \h 20
7.2.3 Term Positions PAGEREF _Toc484628877 \h 21
7.2.4 Translating Common Logic atoms and terms into TFOL PAGEREF _Toc484628878 \h 22
7.2.5 Common Logic modules and headers PAGEREF _Toc484628879 \h 23
7.2.6 Special Name Theories PAGEREF _Toc484628880 \h 26
7.3 Surface syntax. PAGEREF _Toc484628881 \h 27
7.3.1 Contextual signatures PAGEREF _Toc484628882 \h 29
7.3.2 On being semantically first-order PAGEREF _Toc484628883 \h 31
7.3.3 Sequences and sequence variables PAGEREF _Toc484628884 \h 32
7.3.4 Modules, headers, naming and importing PAGEREF _Toc484628885 \h 33
8 Conformance PAGEREF _Toc484628886 \h 33
8.1 Syntactic Conformance PAGEREF _Toc484628887 \h 33
8.1.1 Full Syntactic Conformance PAGEREF _Toc484628888 \h 33
8.1.2 Restricted Syntactic Conformance PAGEREF _Toc484628889 \h 34
8.1.3 First-Order Conformance PAGEREF _Toc484628890 \h 34
8.1.4 Expanded Syntactic Conformance PAGEREF _Toc484628891 \h 34
8.2 Semantic Conformance PAGEREF _Toc484628892 \h 34
AnnexA (normative) Knowledge Interchange Format (KIF) Syntax and Semantics PAGEREF _Toc484628893 \h 35
A.1 Introduction PAGEREF _Toc484628894 \h 35
A.2 KIF Syntax PAGEREF _Toc484628895 \h 36
A.3 Characters PAGEREF _Toc484628896 \h 36
A.4 Lexemes PAGEREF _Toc484628897 \h 36
A.5 Character Strings PAGEREF _Toc484628898 \h 36
A.6 Words PAGEREF _Toc484628899 \h 36
8.3 Object Variables PAGEREF _Toc484628900 \h 37
A.7 Expressions PAGEREF _Toc484628901 \h 37
A.8 KIF Languages PAGEREF _Toc484628902 \h 37
A.9 Terms PAGEREF _Toc484628903 \h 37
A.10 Sentences PAGEREF _Toc484628904 \h 38
A.11 KIF Modules PAGEREF _Toc484628905 \h 39
A.12 Expressions for Module Management PAGEREF _Toc484628906 \h 39
A.13 EBNF Grammar for KIF PAGEREF _Toc484628907 \h 39
A.2. KIF Semantics PAGEREF _Toc484628908 \h 40
AnnexB (normative) Conceptual Graph Interchange Format (CGIF) Syntax and Semantics PAGEREF _Toc484628909 \h 41
B.1 General PAGEREF _Toc484628910 \h 41
B.2 Terms and Definitions PAGEREF _Toc484628911 \h 41
B.1. Conceptual Graph Abstract Syntax PAGEREF _Toc484628912 \h 44
A.1.1. Concept PAGEREF _Toc484628913 \h 45
A.1.2. Conceptual Relation PAGEREF _Toc484628914 \h 46
A.1.3. Lambda Expression PAGEREF _Toc484628915 \h 47
A.1.4. Concept Type PAGEREF _Toc484628916 \h 47
A.1.5. Relation Type PAGEREF _Toc484628917 \h 48
A.1.6. Referent PAGEREF _Toc484628918 \h 49
A.1.7. Context PAGEREF _Toc484628919 \h 50
A.1.8. Coreference Set PAGEREF _Toc484628920 \h 51
A.1.9. Module PAGEREF _Toc484628921 \h 52
B.2. CGIF Concrete Syntax PAGEREF _Toc484628922 \h 53
A.2.1. Lexical Categories PAGEREF _Toc484628923 \h 54
A.2.2. Syntactic Categories PAGEREF _Toc484628924 \h 56
B.3. CGIF Semantics PAGEREF _Toc484628925 \h 67
AnnexC (normative) Concrete Syntax extended Common Logic Markup Language (XCL) PAGEREF _Toc484628926 \h 68
B.4. General PAGEREF _Toc484628927 \h 68
B.5. XCL Syntax PAGEREF _Toc484628928 \h 68
B.6. XCL Semantics PAGEREF _Toc484628929 \h 68
B.3 XCL and dialects PAGEREF _Toc484628930 \h 68
AnnexD (normative) Concrete Syntax Common Logic Controlled English (CLCE) PAGEREF _Toc484628931 \h 70
B.7. General PAGEREF _Toc484628932 \h 70
B.8. CLCE Syntax PAGEREF _Toc484628933 \h 70
B.9. CLCE Semantics PAGEREF _Toc484628934 \h 70
AnnexE (normative) Conformance of Knowledge Interchange Format (KIF) to Common Logic PAGEREF _Toc484628935 \h 71
AnnexF (normative) Conformance of Conceptual Graph Interchange Format (CGIF) to Common Logic PAGEREF _Toc484628936 \h 72
AnnexG (normative) Conformance of XML-based Common Logic (XCL) to Common Logic PAGEREF _Toc484628937 \h 73
AnnexG (normative) Conformance of Common Logic Controlled English (CLCE) to Common Logic PAGEREF _Toc484628938 \h 74
Foreword
ISO (the International Organization for Standardization) is a worldwide federation of national standards bodies (ISO member bodies). The work of preparing International Standards is normally carried out through ISO technical committees. Each member body interested in a subject for which a technical committee has been established has the right to be represented on that committee. International organizations, governmental and non-governmental, in liaison with ISO, also take part in the work. ISO collaborates closely with the International Electrotechnical Commission (IEC) on all matters of electrotechnical standardization.
International Standards are drafted in accordance with the rules given in the ISO/IECDirectives, Part2.
The main task of technical committees is to prepare International Standards. Draft International Standards adopted by the technical committees are circulated to the member bodies for voting. Publication as an International Standard requires approval by at least 75% of the member bodies casting a vote.
Working Draft ISO/IEC24707 was prepared by Joint Technical Committee ISO/IECJTCJTC 1, Information technology, Subcommittee SC32, Data management and interchange.
Introduction
Common Logic is a first-order logic framework intended for information exchange and transmission. The framework allows for a variety of different syntactic forms, called dialects, all expressible within a common XML-based syntax and all sharing a single semantics.
Common Logic has some novel features, chief among them being the ability to express the signature of a piece of Common Logic text in Common Logic itself, a syntax which permits 'higher-order' constructions such as quantification over classes or relations, and a semantics which allows theories to describe intensional entities such as classes or properties. It also uses a few conventions in widespread use, such as numerals to denote integers and quotation marks to denote character strings, and has provision for the use of datatypes, appropriate access to databases, and for naming, importing and transmitting content on the World Wide Web using XML.
EDITORs NOTE. This entire document is taken from the results of an ad-hoc group of researchers who wrote a Simplified Common Logic (SCL) standard to be proposed to the W3C.
An editors note means a comment from the ISO editor and not the SCL ad-hoc group. A comment shown as
Something written in a box like this
is one of the original comments from the SCL developers.
Annexes A, B, C, and D will have similar structure they are intended to specify standard forms for four logic formalisms that have been specifically tailored to conform completely to the Common Logic standard: KIF, CGIF, XCL and CLCE. They are all normative.
Annexes E, F, G and H will also have a similar structure to each other. They will demonstrate conformance for each of the standard formalisms in A through D. They are all informative.
Information technology Common Logic (CL) Framework for a family of logic-based languages
Scope
This standard specifies a language designed for use in the representation and interchange of knowledge among disparate computer systems.
The following features are essential to the design of this standard:
The language has declarative semantics. It is possible to understand the meaning of expressions in the language without appeal to an interpreter for manipulating those expressions.
The language is logically comprehensiveat its most general, it provides for the expression of arbitrary logical sentences.
The following are within the scope of this standard:
interchange of knowledge among heterogeneous computer systems;
representation of knowledge in ontologies and knowledge bases;
specification of expressions that are the input or output of inference engines.
The following are outside the scope of this standard:
the specification of proof theory or inference rules;
specification of translators between the notations of heterogeneous computer systems.
second-order logic
generalized quantifiers
free logics
conditional logics
intuitionistic logics
modal logics
This document describes Common Logics syntax and semantics.
This document is applicable to any formal representation or system that uses first-order logic principles, whether intended for computer processing or not. The standard defines both an abstract syntax and an abstract semantics for first-order logic. The intent is that the content of any system using first-order logic can be represented in the standard. The purpose is to facilitate interchange of first-order logic-based knowledge and information between systems.
The standard addresses issues of syntax and formal semantics only. So-called Real-world semantics (i.e., interpretations based on human intuition or experience) are not addressed, in keeping with the general characteristics of model theory.
Issues relating to merging of (possibly conflicting) knowledge bases are not addressed. Issues relating to computability using the standard (including efficiency, optimization, etc.) are not addressed.
Normative references
EDITORs note : this section is incomplete
The following referenced documents are indispensable for the application 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.
HYPERLINK "http://www.iso.org/iso/en/CatalogueDetailPage.CatalogueDetail?CSNUMBER=4777&ICS1=35&ICS2=40&ICS3="ISO/IEC 646:1991, Information technology -- ISO 7-bit coded character set for information interchange
HYPERLINK "http://www.iso.org/iso/en/CatalogueDetailPage.CatalogueDetail?CSNUMBER=7257&ICS1=1&ICS2=40&ICS3=35"ISO/IEC 2382-15:1999, Information technology -- Vocabulary -- Part 15: Programming languages
HYPERLINK "http://www.iso.org/iso/en/CatalogueDetailPage.CatalogueDetail?CSNUMBER=39921&ICS1=35&ICS2=40&ICS3="ISO/IEC 10646:2003, Information technology -- Universal Multiple-Octet Coded Character Set (UCS)
ISO/IEC 14977, Information technology -- Syntactic metalanguage -- Extended BNF
Terms and definitions
EDITORs note : this section is very incomplete
For the purposes of this document, the following terms and definitions apply.
conceptual graph
A graphical or textual display of symbols arranged according to the style of conceptual graph theory as introduced by John Sowa ADDIN EN.CITE Sowa198470010000000700J.F. Sowa1984Conceptual Structures: Information Processing in Mind and MachineReading, Mass.Addison-Wesley481[1].
conceptual Graph Interchange Format
Rules for the formation of a textual string that conforms to Annex B of this document. Sometimes may refer to an example of a character string that conforms.
Knowledge Interchange Format
Traditional first-order logic
universe of discourse
A nonempty set of things called 'individuals' (as required by Tarskian semantics in first-order logic), but it does not mandate what kind of things must be in this set.
Symbols (and abbreviated terms)
EDITORs Note: this list may be out of date with respect to this draft.
CG: Conceptual Graphs
CGIF: Conceptual Graph Interchange Format
KIF: Knowledge Interchange Format
TFOL: Traditional first order logic
EMBED Unknown: set of individuals in a universe of discourse
EMBED Unknown : universe of discourse
EMBED Unknown : set of relations in a universe of discourse
ext : extension function
EMBED Unknown : interpretation function
EMBED Unknown : semantic value function
EMBED Unknown : satisfaction function
EMBED Unknown : language of an inference system EMBED Unknownas specified by its EBNF.
EMBED Unknown: a Common Logic language
EMBED Unknown: lexicon of a Common Logic language
EMBED Unknown: syntactic mapping EMBED Unknown from expressions in EMBED Unknown to sentences in EMBED Unknown.
EMBED Unknown: syntactic mapping EMBED Unknown from sentences in EMBED Unknown to expressions in EMBED Unknown.
EMBED Unknown : set of sequences of length n of members of EMBED Unknown
EMBED Unknown : set of all sequences over EMBED Unknown
EMBED Unknown : sequence of length 0
EMBED Unknown : concatenation of the rows EMBED Unknown
EMBED Unknown : variable
EMBED Unknown : relation word
EMBED Unknown : term
EMBED Unknown : sentence
EMBED Unknown : word in namespace
Overview
This section is informative.
Most of the design aspects of Common Logic can be understood by considering the following scenario.
Two people, or more generally two agents, A and B, each have a logical formalization of some knowledge. They now wish to communicate their knowledge to a third agent C which will make use of the combined information so as to draw some conclusions. All three agents are using first-order logic, so they should be able to communicate this information fully, so that any inferences which C draws from A's input should also be derivable by A using basic logical principles, and vice versa; and similarly for C and B. The goal of Common Logic is to provide a logical framework which can support this kind of communication and use without requiring complex negotations between the agents.
This ought to be simple, but in practice there are many barriers to such communication.
First, A and B may have used different surface syntactic forms to express their knowledge. This is a well-known problem and various proposals have been made to solve it, usually by defining a standard syntax into which others can be translated, such as KIF [refKIF]. Common Logic tackles this issue similarly by providing a common 'interlingua' syntax XCL into which the others can be translated. XCL uses XML concepts and design principles (inspired by MathML 2.0 [refMathML]) to provide a clean separation between the description of logical form and the surface syntactic form appropriate to a particular usage. It also allows for linking of Common Logic text across documents and conveying Common Logic written in non-XCL syntaxes between applications using XML protocols.
Second, A and B may have made divergent assumptions about the logical signatures of their formalizations. It is common for one agent to use a relation name for a concept described by another as a function, for example, or for two agents to use the same relation with different argument orderings or even different numbers of arguments. More radically, a particular concept, such as marriage, might be represented by A as an individual, but by B as a relation. Often, one can give mappings between the logical forms of such divergent choices, many of which are widely familiar; but in a conventional first-order framework, these have to be considered meta-mappings which translate between distinct formalizations; and very few general frameworks exist to define such meta-syntactic mappings on a principled basis, in a way that allows reasoning agents to draw appropriate conclusions. This problem has not been so widely recognized or discussed as the first one, but it is ubiquitous. Common Logic tackles this issue by as far as possible removing the conventional limitations on first-order signatures, allowing apparently divergent styles of formalization to co-exist and the relationships between them to be expressed axiomatically when required. For example, a name in Common Logic may serve both as an individual name and as a relation name. One of the new aspects of Common Logic is a formal technique for specifying a coherent first-order semantics for a signature-free logical syntax.
Third, A and B may have been writing with different intended universes of discourse in mind. This kind of situation is quite common: very few ontology composers are able to bear in mind that their assertions might be understood to be talking about things that they have not even conceived of. The results, when formal axioms are combined naively, can be quite unpredictable. If A is thinking about taxonomic classifications of animals, say, it is often difficult to bear in mind that the complement of the set of mammals may be taken by B, and hence by C, to include fruit, sodium molecules, styles of avant-garde paintings or the names of fictional characters in movies. Common Logic provides a special 'top-level' syntactic form called a module which automatically gives a name to the universe of discourse of a named ontology, and automatically inserts guards on any contained quantifiers when information is combined. This form is optional, to allow for applications where logical sentences are intended to be combined without applying any such transformations; but its use has many incidental advantages for general information exchange on a network, among them being that all such information is automatically expressed in a decideable subcase of first-order logic [refGuardFrag].
Common Logic also has some other features unusual in a conventional logic but which are intended to facilitate information exchange, including a general technique for using information from externally defined datatypes and databases and a provision for publishing named ontologies for 'public' use on a network.
Common Logic Core
The Common Logic Core is the basic 'readable' syntactic form of Common Logic relative to which the semantics is defined, and which is used to give examples throughout this document. It is not the recommended Common Logic syntax for information exchange. The choice of syntax for the core is somewhat arbitrary, but was based on KIF for historical legacy reasons and because this form, although slightly unconventional in appearance to an eye accustomed to textbook logical forms, has several advantages for machine processing. The Common Logic core syntax is not exactly that of KIF 3.0 [refKIF], and it defines a considerably smaller language.
Common Logic Core Syntax
Any Common Logic Core, or core, expression is encoded as a sequence of Unicode characters as defined in ISO/IEC 10646. Any character encoding which supports the repertoire of ISO 10646 may be used, but UTF-8 (ISO 10646 Annex D ) is preferred. Only characters in the US-ASCII subset are reserved for special use in the core itself, so that the language can be encoded as an ASCII text string if required. This document uses the ASCII encoding. Unicode characters outside that range are represented in ASCII text by a character coding sequence of the form \unnnn or \Unnnnnn where n is a hexadecimal digit character. When transforming an ASCII text string to a full-repertoire character encoding, such a sequence should be replaced by the corresponding direct encoding of the character.
The syntax of the core is designed to be easy to process mechanically and to impose minimal conditions on the character sequences which can be used as logical names. The syntax is defined in terms of disjoint blocks of characters called lexical tokens (in the sense used in ISO/IEC 2382-15). A character stream can be converted into a stream of lexical tokens by a simple process of lexicalisation which checks for a small number of delimiter characters, which indicate the termination of one lexical token and possibly the beginning of the next lexical token. Any consecutive sequence of whitespace characters acts as a separator between lexical tokens. Certain characters are reserved for special use as the first character in a lexical item; in particular, the single-quote (apostrophe U+002C) character is used to start and end quoted strings, which are lexical items which may contain interlexical characters, and the equality sign must be a single lexical item when it is the first character of an item. The use of the characters less-than < (U+003C), greater-than > (U+003C) ampersand & (U+0038) and double-quote " (U+0022) is deprecated, in order to minimise interactions with XML processors of Common Logic core text.
The backslash \ (reverse solidus U+005C) character is reserved for special use. Followed by the letter u or U and a four- or six-digit hexadecimal code respectively, it is used to transcribe non-ASCII Unicode characters in an ASCII character stream, as explained above. Any string of this form plays the same Common Logic syntactic role in an ASCII string rendering as a single ordinary character. The combination \' (U+005C, U+002C) is used to encode a single quote inside a common logic quoted string.
The following syntax is written using Extended Backus-Naur Form (EBNF), as specifed by HYPERLINK "http://www.cl.cam.ac.uk/~mgk25/iso-14977.pdf" International Standard ISO/IEC 14977. Literal chararacters are 'quoted', sequences of items are separated by commas, | indicates alternatives, { } indicates any sequence of expressions, - indicates an exception, [ ] indicates an optional item, and parentheses ( ) are used as grouping characters. Productions are terminated with ;.
The syntax is writen to apply to ASCII encodings. It also applies to full Unicode character encodings, with the change HYPERLINK "" \l "nonasciinote" noted below to the category HYPERLINK "" \l "scnonascii" nonascii.
The syntax is presented here in two parts. The first deals with parsing character streams into lexical items: the second is the logical syntax of Common Logic Core, written assuming that lexical items have been isolated from one another by a lexical analyser. This way of presenting the syntax allows the logical form to be stated without complications arising from whitespace handling. A complete EBNF syntax is given in section XXX which can be used as a basis for parsing Common Logic from a character stream.
Lexical syntax
white = space U+0020 | tab U+0009 | line U+0010 | page U+0012 | return U+0013 ;
Single quote (apostrophe) is used to delimit quoted strings, which obey special lexicalization rules. Quoted strings are the only Common Logic lexical items which can contain whitespace and parentheses. Parentheses outside quoted strings are self-delimiting; they are considered to be lexical tokens in their own right. Parentheses are the primary grouping device in Common Logic core syntax.
open = '(' ;
close = ')' ;
stringquote = ''' ;
char is all the remaining ASCII non-control characters, which can all be used to form lexical tokens (with some restrictions based on the first character of the lexical token). This includes all the alphanumeric characters.
The characters <, & and ' require the use of XML entity references when Common Logic core text is represented as XML content. It is recommended that the characters > and " are also XML-escaped within XML.
char = HYPERLINK "" \l "scdigit" digit | '~' | '!' | '#' | '$' | '%' | '^' | '&' | '*' | '_' | '+' | '{' | '}' | '|' | ':' | '"' | '<' | '>' | '?' | '`' | '-' | '=' | '[' | ']' | '\' | ';'| ',' | '.' | '/' | 'A' | 'B' | 'C' | 'D' | 'E' | 'F' | 'G' | 'H' | 'I' | 'J' | 'K' | 'L' | 'M' | 'N' | 'O' | 'P' | 'Q' | 'R' | 'S' | 'T' | 'U' | 'V' | 'W' | 'X' | 'Y' | 'Z' | 'a' | 'b' | 'c' | 'd' | 'e' | 'f' | 'g' | 'h' | 'i' | 'j' | 'k' | 'l' | 'm' | 'n' | 'o' | 'p' | 'q' | 'r' | 's' | 't' | 'u' | 'v' | 'w' | 'x' | 'y' | 'z' ;
digit = '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' ;
hexa = HYPERLINK "" \l "scdigit" digit | 'A' | 'B' | 'C' | 'D' | 'E' | 'F' | 'a' | 'b' | 'c' | 'd' | 'e' | 'f' ;
Certain character sequences are used to indicate the presence of a single character. nonascii is the set of characters or character sequences which indicate a Unicode character outside the ASCII range. Note. For input using a full Unicode character encoding, this production should be ignored and nonascii should be understood instead to be the set of all non-control characters of Unicode outside the ASCII range which are supported by the character encoding. The use of the \uxxxx and \Uxxxxxx sequences in text encoded using a full Unicode character repertoire is deprecated.
innerquote is used to indicate the presence of a single-quote character inside a quoted string. A quoted string can contain any character, including whitespace; however, a single-quote character can occur inside a quoted string only as part of an innerquote, i.e. when immediately preceded by a backslash character. The occurrence of a single-quote character in the character stream of a quoted string marks the end of the quoted string lexical token unless it is immediately preceded by a backslash character.
nonascii = '\u' , HYPERLINK "" \l "schexa" hexa, HYPERLINK "" \l "schexa" hexa, HYPERLINK "" \l "schexa" hexa, HYPERLINK "" \l "schexa" hexa | '\U' , HYPERLINK "" \l "schexa" hexa, HYPERLINK "" \l "schexa" hexa, HYPERLINK "" \l "schexa" hexa, HYPERLINK "" \l "schexa" hexa, HYPERLINK "" \l "schexa" hexa, HYPERLINK "" \l "schexa" hexa ;
innerquote = '\'' ;
numeral = HYPERLINK "" \l "scdigit" digit , { HYPERLINK "" \l "scdigit" digit } ;
Sequence variables are a distinctive syntactic form with a special meaning in Common Logic. Note that a bare ellipsis '...' is a sequence variable.
seqvar = '...' , { HYPERLINK "" \l "scchar" char } ;
Single quotes are delimiters for quoted strings. A quoted string denotes the text string inside the quotes, except that the combination \' indicates the presence of a single quote mark in the denoted string; and in an ASCII character encoding, the presence of a nonascii sequence indicates a Unicode character at the position in the denoted string. Any occurrence of the backslash character \ not immediately followed by the character ' or u or U simply indicates the backslash character itself. The combination \u or \U may be the initial part of a nonascii sequence which indicates a Unicode character in the denoted string, but if not part of such a sequence then it simply indicates itself. With these conventions, a quoted string denotes the string enclosed in the quote marks. For example, the quoted string 'a\(b\'c' denotes the string a\(b'c, and '\'a (b\\\') c \\'' denotes the string: 'a (b\\') c \'.
Quoted strings require a different lexicalization algorithm than other parts of Common Logic core text, since parentheses and whitespace do not break a quoted text stream into lexical tokens.
When Common Logic Core text is enclosed inside markup which uses character escaping conventions, the Common Logic quoted string conventions here described are understood to apply to the Common Logic text described or indicated by the conventions in use, which should be applied first. Thus for example the content of the XML element: 'a\'b<c&apos is the Common Logic core syntax quoted string 'a\'b'look_here'<==' are all HYPERLINK "" \l "scnamesequence" name sequences, and '...a', '...a...', '.....' and '...' are all legal HYPERLINK "" \l "scseqvar" seqvars. Identity of HYPERLINK "" \l "sclexicaltoken" lexical tokens can be checked by a simple character-by-character string match.
A name is any lexical token which is understood to denote. The expression syntax, below, uses this category; it is not required for lexicalization.
name = HYPERLINK "" \l "scnamesequence" namesequence | HYPERLINK "" \l "scnumeral" numeral | HYPERLINK "" \l "scquotedstring" quotedstring ;
Core expression syntax
This part of the syntax is written so as to apply to a sequence of HYPERLINK "" \l "sclexicaltoken" Common Logic lexical tokens rather than a character stream, so it ignores whitespace handling. A full EBNF syntax for Common Logic Core suitable for generating parsers of character-level data is given in section @@@..
Both terms and atomic sentences use the notion of a sequence of terms representing a vector of arguments to a function or relation.
termseq = { HYPERLINK "" \l "scterm" term } , HYPERLINK "" \l "scseqvar" seqvar? ;
Names count as terms, and a complex (application) term consists of a term denoting a function with a vector of arguments. Terms may also have an associated comment in the form of a quoted string. Note that this now requires an explicit comment marker in the core syntax.
term = HYPERLINK "" \l "scname" name | ( HYPERLINK "" \l "scopen" open, HYPERLINK "" \l "scterm" term , HYPERLINK "" \l "sctermseq" termseq, HYPERLINK "" \l "scclose" close ) | ( HYPERLINK "" \l "scopen" open, 'scl:comment', HYPERLINK "" \l "scquotedstring" quotedstring , HYPERLINK "" \l "scterm" term, HYPERLINK "" \l "scclose" close ) ;
Equations are distinguished as a special category because of their special semantic role and special handling by many applications. Note that the equality sign is not a term.This is a change from the previous version of the syntax.
equation = HYPERLINK "" \l "scopen" open, '=', HYPERLINK "" \l "scterm" term, HYPERLINK "" \l "scterm" term, HYPERLINK "" \l "scclose" close
Atomic sentences are similar in structure to terms. In addition, equations are considered to be atomic, and an atomic sentence may be represented using role-pairs consisting of a role-name and a term.
atomsent = HYPERLINK "" \l "scequation" equation | ( HYPERLINK "" \l "scopen" open, HYPERLINK "" \l "scterm" term , HYPERLINK "" \l "sctermseq" termseq, HYPERLINK "" \l "scclose" close ) | ( HYPERLINK "" \l "scopen" open, HYPERLINK "" \l "scterm" term, HYPERLINK "" \l "scopen" open, 'roleset:' , { HYPERLINK "" \l "scopen" open, HYPERLINK "" \l "scname" name, HYPERLINK "" \l "scterm" term, HYPERLINK "" \l "scclose" close } , HYPERLINK "" \l "scclose" close, HYPERLINK "" \l "scclose" close ) ;
Boolean sentences require implication and iff to be binary, but allow and and or to have any number of arguments (including zero).
boolsent = ( HYPERLINK "" \l "scopen" open, ('and' | 'or') , { HYPERLINK "" \l "scsentence" sentence }, HYPERLINK "" \l "scclose" close ) | ( HYPERLINK "" \l "scopen" open, ('implies' | 'iff') , HYPERLINK "" \l "scsentence" sentence , HYPERLINK "" \l "scsentence" sentence, HYPERLINK "" \l "scclose" close ) | ( HYPERLINK "" \l "scopen" open, 'not' , HYPERLINK "" \l "scsentence" sentence, HYPERLINK "" \l "scclose" close ;
Quantifiers may bind any number of variables and may be guarded; and bound variables may be restricted to a named category.
The guarded-quantifier syntax - the optional name immediately after the quantifier - is a new option not in the previous version. May 12.
quantsent = HYPERLINK "" \l "scopen" open, ('forall' | 'exists') , [ HYPERLINK "" \l "scname" name ] , HYPERLINK "" \l "scopen" open, { HYPERLINK "" \l "scname" name | ( HYPERLINK "" \l "scopen" open, HYPERLINK "" \l "scname" name, HYPERLINK "" \l "scterm" term, HYPERLINK "" \l "scclose" close )} , HYPERLINK "" \l "scclose" close, HYPERLINK "" \l "scsentence" sentence, HYPERLINK "" \l "scclose" close ;
Like terms, sentences may have comments attached.
sentence = HYPERLINK "" \l "scatom" atomsent | HYPERLINK "" \l "scboolsent" boolsent | HYPERLINK "" \l "scquantsent" quantsent | ( HYPERLINK "" \l "scopen" open, 'scl:comment', HYPERLINK "" \l "scquotedstring" quotedstring , HYPERLINK "" \l "scclose" close ) ;
Common Logic text is a sequence of phrases, each of which is either a 'top-level' sentence, an importation, or a bare comment. We distinguish sentence from phrase because phrases are considered to bind sequence variables. The name argument of an importation will usually be a URI.
phrase = HYPERLINK "" \l "scsentence" sentence | HYPERLINK "" \l "scopen" open,'scl:imports', HYPERLINK "" \l "scname" name , HYPERLINK "" \l "scclose" close | HYPERLINK "" \l "scopen" open, 'scl:comment', HYPERLINK "" \l "scquotedstring" quotedstring, HYPERLINK "" \l "scclose" close ;
scltext = { HYPERLINK "" \l "scphrase" phrase } ;
A Common Logic module is a named piece of text with an optional header containing text which is intended to convey 'meta-information'; details are given later in the document.
moduledefinition = HYPERLINK "" \l "scopen" open, 'scl:module' , HYPERLINK "" \l "scname" name , [ HYPERLINK "" \l "scopen" open, 'scl:header' , HYPERLINK "" \l "scscltext" scltext , HYPERLINK "" \l "scclose" close ] , HYPERLINK "" \l "scscltext" scltext , HYPERLINK "" \l "scclose" close ;
Specialname is a category of lexical tokens to which Common Logic attaches particular semantic meanings. Although they are not required to be distinguished for parsing purposes, the list of special forms in the Common Logic Core syntax is appended here for convenience. Other Common Logic dialects may extend this category to include other name forms reserved for special use, and headers may declare other classes of special forms. If a special form is used in any Common Logic text then its meaning as a special form cannot be over-ridden by any other interpretation of that text, so inappropriate uses of special forms may produce inconsistencies.
specialname = 'scl:same' | 'scl:different' | 'scl:arity' | 'scl:Ind' | 'scl:Rel' | 'scl:Fun' | 'scl:Integer' | 'scl:String' | HYPERLINK "" \l "scnumeral" numeral | HYPERLINK "" \l "scquotedstring" quotedstring;
Common Logic Core Semantics
The semantics of Common Logic is defined conventionally in terms of a satisfaction relation between Common Logic text and structures called interpretations. For Common Logic however the interpretations are required to extend the relational and function mappings into the domain so as to provide an appropriate relational interpretation for every individual which may be denoted by a term in a relation or function position. As discussed earlier, this generalizes the usual idea of an interpretation being defined on a fixed signature. In effect, this restricts interpretations to be those which would fit any signature under which the text could be considered to be syntactically legal.
Interpretations
Let T be a common logic text, VO(T) be the set of names occurring in object position in T , VR(T) be the set of names occurring in relation position in T, and VF(T) those occurring in function position in T; called respectively the object, relation and function vocabularies of T. Note that Common Logic syntax does not require that these vocabularies are mutually exclusive.
Define a relational extension over S to be any set of finite sequences of elements of S, and a functional extension over S to be any set of pairs where s is a sequence of elements of S and x is an element of S, such that if and are in the set then x = y. Say that a functional extension is total on n if it contains a pair for every sequence s of length n over S. Note that a functional extension may be total on several n, and may be total on n but not on m.
A bare interpretation of a vocabulary (VO,VR,VF) is defined by a set and three mappings:
A nonempty set UI called the universe;
A mapping intI from VO to UI;
A mapping relI from VR to the set RelI of relational extensions over UI
A mapping funI from VF to the set FunI of functional extensions over UI.
This is a conventional first-order interpretation structure, slightly generalized to allow variadic relations. Note however that Common Logic does not require that these various lexical categories be distinct.
It is conventional to also require that funI is total on the arity of any function name. This follows in our case from the 'folding conditions' defined below.
Common Logic syntax allows expressions in which a term other than a name, or a term containing variables, occurs in a relation or function position. In these cases, we will assume that the individual denoted by the term plays the appropriate role of a relation or function required by the syntactic position of the term. This requires extending the rel and fun mappings defined on the vocabulary by adding partial mappings from the universe to the appropriate extensions.
A folded interpretation, or simply an interpretation, of T is a bare interpretation I of T together with two partial mappings relationI and functionI, called fold maps, from UI to relational and functional extensions over UI respectively, which satisfy the conditions described below. In fact it is convenient to extend these mappings to include the interpretation mappings relI and funI on names, so we will define relationI to be a mapping from (RI union VR(T) ) to RelI and functionI a mapping from (FI union VF(T) ) to FunI , where RI and FI are subsets of UI
First, we require that folds respect both the individual and relational parts of the interpretation mappings wherever they overlap, and that when an individual name is also required to play a relational or functional role, that the appropriate extensions are associated with the denoted individual:
if relI(x) is defined then relationI(x) = relI(x); and if intI(x) is defined then relationI(intI(x)) = relationI(x);
if funI(x) is defined then functionI(x) = funI(x); and if intI(x) is defined then functionI(intI(x)) = functionI(x).
Intuitively, this can be seen as a 'folding' of conditions arising from the disparate requirements of two (or more) conventional interpretations represented by the several basic mappings, as illustrated by the figures below:
To combine these interpretations we simply merge relational extensions mapped from the same name, and similarly for functional extensions; note that the union of functional extensions defined on n and on m is itself defined on both n and m. If a name is required to identify both a relational and a functional extension then it can continue to play both roles. In cases where a name is required to map both to an extension and to an individual, however, we add a fold to associate the individual to the extension:
The effect of the fold maps is to ensure that the relational or functional extension identified by the name directly is the same as that identified by the name via its interpretation as denoting an individual. The further conditions described below follow this identification through the syntactic truth-recursions so as to guarantee that any term which occurs in multiple positions will always identify an extension appropriate to the position. This ensures that an interpretation will provide meaningful denotations for all possible expressions which can arise as a result of performing any first-order reasoning process on the text, such as variable instantiation and equality substitution.
It would be possible to define interpretations more simply, but less conventionally, by assuming that all names denote individuals, and associating every individual with both a relational and a functional extension. This obviates the need to consider 'folding' as a special construct and eliminates the need to state recursive conditions on the fold mappings. In many ways the resulting semantic framework, described in [refCLAS], is simpler and more elegant than the one described here; but this version has the advantage of reducing to the conventional Tarskian notion whenever the text fits the traditional syntactic form, so is more clearly a genuine generalization of conventional FO logical semantics. One might call the alternative version a 'maximally' folded semantics, while the current one is 'minimally' folded.
Define a name map on a set S of names to be any mapping from S to UI, and a sequence map to be any mapping from sequence variables to finite sequences of elements of UI. If A is a name or sequence map on S, define IA to be the interpretation which is like A on names or sequence variables in S, but otherwise is like I: formally, UIA = UI, relationIA = relationI, functionIA = functionI, and intIA(v) = A(v) when v is in S, otherwise intIA(v)= intI(v).
When A is a sequence map, this is a slight extension of the notion of interpretation. We use this to provide an interpretation of phrases containing sequence variables. The rest of the truth-conditions map transparently to this extension.
This notation associates to the left, so that IAB = (IA)B, meaning that if x is in the domain of B then intIAB(x)=B(x). In addition, we use the following notation: if s= and t= are finite sequences, then s;t is the concatenated sequence
The interpretation I(E) of any Common Logic core expression E, and the further conditions on the fold maps, are then combined in the following table. An empty cell in the third column indicates that an expression of that type introduces no extra conditions, other than those that arise from its subexpressions.
Table SEQ Table \* ARABIC 1. Interpretations of Common Logic Expressions.
Common Logic interpretation I of an expression E if E is aof the formthen I is an interpretation of E ifand I(E) =name numeral nintI(n) = the decimal value of nquoted string 'string'intI('string') = string with every HYPERLINK "" \l "scinnerquote" innerquote substring replaced by a single quote character '''name, in object positionintI(name)name, in relation positionrelationI(name) = relI(name);
and if I(name) is defined then
relationI(I(name)) = relI(name)name, in function positionfunctionI(name) = funI(name);
and if I(name) is defined then
functionI(I(name)) = funI(name)term sequence(t1 ... tn) (t1 ... tn @v) ; I(@v)term(f seq)functionI(f) is total on |I(seq)| ; and
if I(f) is defined then I(f) is in FI and
functionI(f) = functionI(I(f)).x, where functionI(f) contains < I(seq), x >(scl:comment 'string' term)I(term)atom(= t1 t2)true if I(t1)= I(t2), otherwise false.(r seq)If I(r) is defined then I(r) is in RI and
relationI(r) = relationI(I(r)).true if relationI(r) contains I(seq), otherwise false booleanSentence(not s)true if I(s) = false, otherwise false(and s1 ... sn)true if I(s1) = ... = I(sn) = true, otherwise false(or s1 ... sn)false if I(s1) = ... = I(sn) = false, otherwise true(implies s1 s2)false if I(s1) = true and I(s2) = false, otherwise true (iff s1 s2)true if I(s1) = I(s2), otherwise falsequantifiedSentence(forall (var) body)for any name map B on {var}, IB is an interpretation of every atom and term in bodyif for every name map B on {var}, IB(body) = true, then true;
otherwise, false.(exists (var) body)if for some name map B on {var}, IB(body) = true, then true;
otherwise, false.(forall ((var t) body)for any name map B on {var}, IB is an interpretation of every atom and term in body and of (t var)if for every name map B on {var}such that relationI(t) contains , IB(body) = true, then true;
otherwise, false.(exists ((var t) body)if for some name map B on {var}such that relationI(t) contains , IB(body) = true, then true;
otherwise, false.sentence(scl:comment 'string' sentence)I(sentence)phrase(scl:comment 'string')truesentencefor any sequence map A on the seqvars in sentence, IA is an interpretation of every atom and term in sentence.if for every sequence map A on the seqvars in sentence, IA(sentence) = true, then true;
otherwise false(scl:imports name)I is an interpretation of I(name)false if I(I(name)) = false, otherwise truescltexts1 ... snI is an interpretation of all of s1 ... sntrue if I(s1) = ... = I(sn) = true, otherwise false
If T is a text and I is a bare interpretation of the vocabulary of T, then any folded interpretation J= (I, relationJ, functionJ) which satisfies the conditions in the third column of the above table is a legal interpretation of T: we will call any such interpretation a folding of I. The conditions in the third column of the semantic table guarantee that all Common Logic terms will have a unique denotation in any interpretation.
Discussion
The above differs somewhat from a conventional semantic recursion, in which a bare interpretation is sufficient to determine the semantic values of all expressions. In our case, the syntax of the text also provides a guide to how part of the interpretation must be constructed.
The conditions in the third column in effect extend the basic folding maps from simple names to all expressions and all possible interpretational modifications which arise from the use of quantifiers. To see the effect of these conditions, consider the atomic sentence
((f a) b c)
Here, the term (f a) is required to denote something in the universe but it is also required to play a relational role. Following down the recursions, relationI( (f a)) must be defined, and since I((f a)) - that is, the individual x with <,x > in functionI(f) - is defined, the folding map is required to apply to this individual, so that relationI((f a)) = relationI(I( (f a) )). This ensures for example that if we also have the equation
(= (f a) foo)
then the result of performing equality substitution preserves the relational interpretation of the term when substituted into a relational position:
(foo b c)
since by virtue of the truth of the equation, I(foo)) = I( (f a) ); so relationI(foo) = relationI(I(foo)) = relationI(I( (f a) )) = relationI((f a)). Similar reasoning shows that the substitution of equated names occurring in functional positions preserves the functional meaning.
Note that the equational rules applied to this text:
(= thisfun thatfun) (P (thisfun a)) (Q (thatfun a b))
requires that there is an individual x = I(thisfun) = I(thatfun) with functionI(x) total on both 1 and 2. The use of a sequence variable in a term requires that the function name used in that term have an associated functional extension which is total on the length of the argument sequence and every higher number; for example:
(P (f a b ...x))
can only be legally interpreted by an I with relI(f) total on n for every n greater than or equal to 2.
The presence of a variable in a relation position, for example
(forall (R) (iff (transitive R) (forall (x y z)(implies (and (R x y)(R y z))(R x z))) ))
requires that the fold map relationI is defined on the entire universe of any interpretation.
To see why, observe that R occurs in relation position so relI(R) is defined; now choose some x in UI and consider the variable map A with A(R) = x, so IA(R) = x. IA is required to be an interpretation of the body
(iff (transitive R) (forall (x y z)(implies (and (R x y)(R y z))(R x z))) )
and hence of (R x y) and hence of the name R occurring in relation position; and since IA(R) exists, relationIA(x) must be defined: but this is relationI(x), by definition of IA.
However, this is in fact a trivial requirement, since one can simply define relationI(x) = { } for all x to which no stronger constraint applies. The strongest possible requirements on a fold arise when a term with a variable in function position also contains a sequence variable, for example:
(forall (f)(implies (functional f) (f (f ...x) ...x) ))
which is equivalent in meaning to the infinite conjunction
(and
(forall (f x)(implies (functional f) (f (f x) x) ))
(forall (f x y)(implies (functional f) (f (f x y) x y) ))
(forall (f x y z)(implies (functional f) (f (f x y z) x y z) ))
...)
This requires that any legal interpretation I provides a fold mapping functionI which is defined on the entire universe and every value of which is a total function for any number of arguments. However, this too can always be trivially satisfied, for example, by choosing a universal functional value c in the universe and defining functionI(x) to be the set { : s a finite sequence }, for all x in T to which no other constraints apply.
In many cases, the fold conditions can be understood as a recursive extension of the basic intepretation mappings on names. Not all pieces of Common Logic syntax support such a recursive interpretation, however. For example, consider the atomic sentence
(((f a) a) a)
in which f and (fa) both occur in function position, ((fa)a) in relation position and a in object position (three times). A bare intepretation I of this vocabulary provides a universe UI containing at least an individual I(a) = intI(a) - call it x - and a function extension funI(f) which is total on UI, so I((fa)) must be defined: call it y. The fold conditions require y to be in FI so that functionI((fa)) is defined and is identical to functionI(I((fa))), ie to functionI(y), and this also is total on UI , so has a value for the argument intI(a); this value is I(((fa)a)) - call it z - which is required to be in RI and so to have a corresponding relational extension relationI(((fa)a)): and the atom is true when that extension contains . The process is illustrated in figure 3:
In this case, the folding maps themselves require functional and relational extensions to exist which are not denoted directly by any name in the vocabulary, but are required in order to coherently interpret terms containing other terms in function or relation position. As the example also shows, it is possible for syntactically legal Common Logic terms to denote individuals which are not present in a bare interpretation of the vocabulary; that is, the fold maps may require the universe of a bare interpretation to be extended. This case will arise only when a complex term occurs in a function position but is not an argument of any other term or atom.
These conditions apply to all interpretations, not just to those which satisfy the text. A structure which fails to satisfy these conditions might fail to provide denotations for some expressions, or fail to assign a truth-value to some sentences. One way to think about these conditions is that they are in a sense the minimal outcome of a process of negotation concerning the appropriate signature role of a name or expression. Suppose two agents A and B are negotiating about the denotation of a name: A wishes it to denote something in the universe of discourse, while B wishes it to play the role of a relation: c.f. figure 1, above. They can both be satisfied if the entity that A takes to be the denotation is allowed to play the role of a relation when the name denoting it occurs in a relation position, and if the relational extension it uses in that role is identical to the relation denoted by the name: for then, all the relational assertions that B wishes to hold will be preserved. Thus, A and B can agree. The conditions on relationI and functionI are the result of following this hypothetical negotiation through the recursions defined by the syntax, in order to ensure that A and B can both assign a meaningful and mutually acceptable interpretation to every possible instance of every expression which can arise from any process of inference applied to their combined texts. In some cases, such as the previous example, this negotiation might require A and B to agree on aspects of an interpretation which do not arise from either of their preferred interpretations taken in isolation, but are imposed on the folded settlement by the syntactic requirements of the language.
Note that this hypothetical negotiation does not require that any items be added or removed from the universe, or changes made to the basic interpretation mappings intI, relI and funI; it is wholly concerned with the appropriate adjustments to the folding mappings. The above discussion shows that A and B can always reach an agreement without changing the basic interpretation structure of I. Editors note: This needs to be stated more carefully. There are cases where the universe neds to be enlarged, as in the Horrocks sentences.
HMMM, Im not so sure that this ever does happen in fact. Anything in the folded interpretation will be in ONE of the universes. There ought to be a provable result here, that any folded interpretation can be got by adding extensions and folds to a bare interpretation of the same text, without extending the universe. Even in the fig3 example, all the terms a (f a) and ((f a) a) are required to denote simply because they are terms, no matter what position they are in (??).
What is odd about this example is that it seems to have pieces missing. How could that atom arise from negotiation? Only way I can see is that it could be an equality substitution from (= R (f a)) folding with (R a), but then the R-thing would be in the universe already. We don't have it in our universe because we forgot to mention R explicitly. There is an implicit assumption of monotonicity (!) in this example, therefore, if it is to be motivated by the negotiation discussion. Hmm, interesting.
This construction may place additional requirements on the interpretation, so it is possible that a bare interpretation of the vocabulary of T may be insufficient to provide a basis for a suitable folding. In such a case the universe of I may need to be extended to provide enough distinct individuals to 'carry' the needed extensions. The construction in the third column of the semantic table is therefore both part of the definition of a folded interpretation and acts as a filter on bare interpretations, ruling out those that are too small to satisfy the text. Thus, a bare interpretation of the vocabulary of T may not be an interpretation of T.
Consider the notion of shrinking/expansion needed for the header stuff. This seems to apply here too. Then the result would be, given any bare interpr I of vocab(T), there is a J, a folding of an expansion of I which is an interpretation of T. That seems plausible and ought to be easy to prove by an induction on the syntax where J gets built by adding extensions and extending the universe where required.
It would be nice to be able to exactly characterize the conditions that require the universe to be extended. The example in fig 3 is one case, where a term occurs only in relation position. Are all cases like this? No, think of the case of (not (Thing foo)) in a header. Hmmm, maybe we should just make it illegal to use Thing inside a body text (??).
Special name interpretations
In addition to the basic semantic conditions, interpretations are required to satisfy constraints on the interpretations of the Common Logic special names, summarized in the following table.
Table SEQ Table \* ARABIC 2. Special name interpretations.
Special namesatisfies conditionscl:samerelI(scl:same) = {: x in UI }scl:differentrelI(scl:different) = {: x1,...,xn all in UI and xi =/= xj for 1<= i,j <=n}scl:IntegerrelI(scl:Integer) = {: n an non-negative integer in UI} scl:StringrelI(scl:String) = {: u a Unicode character string in UI} scl:ThingrelI(scl:Thing) ={ : x1,...,xn all in UI }This may need to be changed to allow for named UODs scl:RelrelI(scl:Rel) = {: x1,..., xn all in RI }scl:FunrelI(scl:Fun) = {: x1,..., xn all in FI }scl:arityrelI(scl:arity) ={: x1,...,xn all in RI and relationI(x1) ,..., relationI(xn) all contain an s with length(s)=m }All Common Logic dialects and extensions are required to satisfy these general conditions. Other Common Logic dialects and extensions may also impose semantic conditions on other categories of special names; some examples are given later.
scl:same and scl:different are convenient abbreviations for conjunctions of n equations and n(n-1) negated equations respectively, where n is the number of arguments.
Note that scl:different is identical in meaning to the negation of scl:same only in the case where both are applied to precisely two arguments.
The conventions for strings and numerals can be viewed as special 'built-in' datatypes, following the datatype convention described below: the other items are special vocabulary primarily intended for use in module headers, also described later.
Common Logic satisfaction and entailment
EDITORs NOTE: This section is still under construction.
Say that an interpretation I satisfies a common logic text T when I is an interpretation of T and I(T)=true.
If I is a bare interpretation of the vocabulary of T then say that I satisfies T if there is a folding (I, rI, fI) which satisfies T. Note that this is a requirement on I itself: in effect, it requires I to provide enough individuals and appropriate extensions sufficient to enable a suitable folding to be built on the foundation provided by the bare interpretation.
Need show that if I is a bare interpretation of V containing vocab(T) and vocab(S) and I satisfies T and S, then it satisfies T+S. The idea is to combine the folding conditions: need to show it can always be done so as to preserve satisfiability. This ought to be pretty trivial but does requirte an induction. Right now I need to go to bed.
This is the core point about folding: adding new vocabulary can always be handled by adding folds.
Suppose I satisfies T and J satisfies S. What can be said about satisfying (S+T) ? It had better be the case that satisfaction is preserved under deletion!
Again, it seems clear that if we have two traditional first order logic (TFOL) texts then it ought to be possible to project back from a model of their sum to the traditional first order logic models of them. What exactly is the nature of this projection? It ought to be allowing the universe to shrink and tossing out some folds, is all. And of course any extensions that arent used go away automatically.
NOTE the new formulation using functions completely does away with the old problems about entailment and the deduction theorem. :-)
and that S entails T when every interpretation which satisfies S also satisfies T; that T is unsatisfiable when it has no satisfying interpretations; and that it is valid when it is satisfied by every interpretation of it.
All of these definitions are standard, but the fact that the folding maps required by Common Logic interpretations are in a sense selected by the text itself requires us to establish some lemmas which are trivial or unnecessary in most conventional accounts of first-order logic.
The Common Logic Kernel
It is useful to distinguish a subset of the core syntax which is just sufficient to define the meanings of all the other logical constructions. The semantics will be defined on this minimal 'kernel', and the meanings of the remaining constructions defined by a systematic translation to the kernel.
The kernel syntax omits the role-pair syntax for atomic sentences, restricted quantification, the existential quantifier and all connectives other than and and not, and it does not support the module syntax, but is restricted to simple Common Logic text. HYPERLINK "" \l "scterm" Terms, HYPERLINK "" \l "sctermseq" term sequences and HYPERLINK "" \l "scequation" equations are identical to the core syntax, and the breakdown of the sentence category into four types is identical to that used in the core.
atomsent = HYPERLINK "" \l "scequation" equation | HYPERLINK "" \l "scopen" open, HYPERLINK "" \l "scterm" term, HYPERLINK "" \l "sctermseq" termseq, HYPERLINK "" \l "scclose" close ; compare core HYPERLINK "" \l "scatom" atomsent
boolsent = HYPERLINK "" \l "scopen" open, 'and' , { HYPERLINK "" \l "scksentence" sentence }, HYPERLINK "" \l "scclose" close | HYPERLINK "" \l "scopen" open, 'not' , HYPERLINK "" \l "scksentence" sentence , HYPERLINK "" \l "scclose" close ; compare core HYPERLINK "" \l "scboolsent" boolsent
quantsent = HYPERLINK "" \l "scopen" open, 'forall' , HYPERLINK "" \l "scopen" open, HYPERLINK "" \l "scname" name , HYPERLINK "" \l "scclose" close, HYPERLINK "" \l "scksentence" sentence , HYPERLINK "" \l "scclose" close ; compare core HYPERLINK "" \l "scquantsent" quantsent
sentence = HYPERLINK "" \l "sckatom" atomsent | HYPERLINK "" \l "sckboolsent" boolsent | HYPERLINK "" \l "sckquantsent" quantsent ; same subdivision into sentence categories as core
phrase = HYPERLINK "" \l "scksentence" sentence ; compare core HYPERLINK "" \l "scphrase" phrase
scltext = { HYPERLINK "" \l "sckphrase" phrase } ;
The translations of the other core expression patterns into the kernel are given by the following table. The first line defines the meaning of role-set atoms, discussed in more detail above: the variable x introduced in this line is assumed to be distinct from any other names occurring in the expression. The remaining translations are the standard textbook reductions of logical expressions to the forall-and-not subcase. Need to add a translation for guarded quantifiers
Table SEQ Table \* ARABIC 3. Translations from CL core to CL kernel.
expression E of typewith syntactic formtranslates to kernel expression K[E] atomsent(t (roleset: (n1 t1) ... (nm tm)))K[ (exists (x) (and (t x) (= t1 (n1 x)) ... (= tm (nm x)) )) ]boolsent(or s1 ... sn)(not (and (not K[s1]) ... (not K[sn]) ))(implies s1 s2)(not (and K[s1] (not K[s2]) ))(iff s1 s2)(and K[ (implies s1 s2) ] K[ (implies s2 s1) ] )quantsent(forall g (...) s)K[ (forall (...) K[ (implies (g ) s )) ] ] DAMN this is very hard to describe recursively. Maybe I'll have to resort to text. (forall ((x t) ...) s)(forall (x) K[ (implies (t x) (forall (...) s) ))) ](forall (x ...) s)(forall (x) K[ (forall (...) s) ] )(forall () s)K[ s ](exists (...) s)(not K[ (forall (...) (not K[ s ])) ] sentence(scl:comment 'string' s)K[ s ]The earlier example
(forall (x) (implies (Boy x) (exists (y) (and (Girl y)(Kissed x y) )) ))
can also be expressed in the core syntax by using quantifier restrictions:
(forall ((x Boy)) (exists ((y Girl)) (Kissed x y) ))
Both translate into the Common Logic kernel form:
(forall (x) (not (and (Boy x) (forall (y) (not (and (Girl y)(Kissed x y) ))) )))
Note that comments, 'vacuous' quantifiers which do not bind a variable, comments and
Special Cases leave until later?
Several special cases of the kernel syntax can be identified, largely by restrictions on the syntax of atomic sentences and terms.
Text is first-order if it contains no sequence variables, the only terms which occur in relation or function positions are names, and every name occurs in only one kind of position. If no term occurs in function or relation position in two atoms or terms with different numbers of arguments, then the text is fixed-arity. Fixed-arity first-order text corresponds to the traditional notion of a first-order signature: the names in the vocabulary can be subdivided into relation, function and individual names, each occurring only in its alloted role in the syntax, and with each function or relation having a fixed number of arguments. We will refer to this case as goffol text.
If all terms are names, so there are no expressions in function position, the text is pure relational.
If no variable occurs in any term in function position, then the text is rigid. Rigid text represents a useful compromise between the syntactic freedom of general Common Logic and the syntactic predictability of goffol syntax. Notice that rigidity only restricts the occurrence of variables inside terms in function position: rigid text allows arbitrary terms to occur in relation position, and names in relation position may be bound by quantifiers. Its probably no longer worth distinguishing this case, unless it shows up naturally in the metatheory.
This means that the content of a non-rigid text can often be expressed in equivalent rigid text by unpacking all the non-rigid terms and replacing them with suitable relational atoms, for example by re-writing:
(forall (x y)( ... (R ((f y) x)) ... ))
as:
(forall (x y) (exists (z) (and (f z y) (functional f) ( ... (R (z x)) ... ))))
with the additional axiom:
(forall (f) (iff (functional f) (forall (x y)(implies (and (f x ...)(f y ...)) (= x y)))))
Common Logic atoms and terms: discussion
Apart from the top-level syntax for defining headers and ontologies, the only unconventional aspects of Common Logic are the syntax for atomic sentences and terms, which reflect the type-free catholicity imposed by the need to allow multiple lexical perspectives to co-exist. This section discusses these features in more detail.
Need a section commenting on the lexical freedom in eg allowing numerals and strings to be relations.
Sequence variables, recursion and argument lists
A sequence variable stands for an 'arbitrary' sequence of arguments. Since sequence variables are implicitly universally quantified, any top-level expression in which a sequence variable occurs has the same semantic import as the countably infinite conjunction of all the expressions obtained by replacing the sequence variable by a finite sequence of variables, all universally quantified at the top (phrase) level. For example, the top-level sentence
(R ...)
has the same meaning as the infinite conjunction:
(and
(R)
(forall (x)(R x))
(forall (x y)(R x y))
(forall (x y z)(R x y z))
... )
This includes the 'trivial' case for zero arguments:
(forall ( ) (R))
where the vacuous quantifier is omitted. To omit this case, write the top-level atomic sentence with one quantified variable and a sequence variable:
(forall (x)(R x ...))
Sequence variables can be used to write 'recursive' axiom schemes. Rather than attempt a fully general description of this technique, we will illustrate it with a canonical example. Consider the following sentences:
(= nil (list))
(forall (x z) (iff (= x (list ...) (= (cons z x) (list z ...)))
which have the same meaning as the infinite set of sentences:
(= nil (list))
(forall (x z) (iff (= x (list) (= (cons z x) (list z))))
(forall (x z x1) (iff (= x (list x1)) (= (cons z x) (list z x1)) ))
(forall (x z x1 x2) (iff (= x (list x1 x2)) (= (cons z x) (list z x1 x2)) ))
(forall (x z x1 x2 x3) (iff (= x (list x1 x2 x3)) (= (cons z x) (list z x1 x2 x3)) ))
...
(forall (x z x1 x2 ... xn) (iff (= x (list x1 ... xn) (= (cons z x) (list z x1 ... xn)) ))
... )
which clearly entails for any finite sequence t1 ... tn of terms, that
(= (cons t1 (cons t2 (cons ... (cons tn nil) ... ))) (list t1 ... tn) )
and thus provides the familiar LISP technique of writing a sequence of items as a cons-nil list, used more recently as the RDF 'collection' vocabulary [refRDF]. The tail-recursion represented by the axiom is re-expressed here as induction on the length of a proof.
Common Logic sequence variables do not actually provide a true recursive definition, as the 'schema' can be used only as a source of assertions and cannot itself be derived by using an inductive argument. The more powerful language obtained by allowing sequence variables to be bound by sequence quantifiers does provide true recursive powers, and is therefore in a higher expressive class than any first-order language. For example, it is not compact. A more tractable language can probably be obtained by adding an explicit 'least fixed point' operator, as in the mu-calculus, but this idea goes beyond the scope of this document.
This general technique of imitating tail-recursive definitions by writing them as implications using sequence variables was pioneered by KIF [refKIF] and is one of the primary uses for sequence variables in Common Logic. What this construction shows, however, is that the use of sequence variables can be replaced, when required, by the use of explicit cons-nil lists as arguments, represented in Common Logic by nested terms. This convention is widely used in logic programming applications, and in RDF and OWL. The general rule can itself be stated in Common Logic by using a sequence variable:
(forall (x) (iff (x ...) (x (list ...)) ))
This thus provides a general technique for replacing the use of sequence variables by explicit quantification over argument lists. The costs of this translation are a considerable reduction in syntactic clarity and readability, and the need to allow lists as entities in the universe of discourse. The advantage is the ability of rendering arbitrary argument sequences using only a small number of primitives with a fixed, low arity. Common Logic can use either convention or both together, and can describe the relationship between them.
Role-set syntax, eventualities and selections
Atomic sentences which use the roleset: construction, for example
(Married (roleset: (wife Jill) (husband Jack)))
are considered to take a set of arguments in the form of role-value pairs. In this role-set syntax, the connection between the relation and its arguments is indicated by the role labels rather than by position in an argument sequence, which avoids the necessity of remembering the argument order when writing sentences, and provides some insurance against communication errors arising from sentences using different argument-order conventions.
In Common Logic, the roles are considered to be binary relations between an entity to which the main predicate applies and the argument, so for example the above atom is equivalent to the existential conjunction:
(exists (x) (and (Married x) (= Jack (husband x)) (= Jill (wife x)) ))
where x indicates an entity which has been variously called an eventuality, fact, situation, event, state or trope, and might be rendered in English as "Jack and Jill's being married" or "the state of marriage between Jack and Jill". For Common Logic purposes however it is possible to think of x more prosaically as being a vector or sequence of arguments, and the role-names as selectors on the elements of this sequence.
This syntax allows arguments to be provided in a piecemeal fashion, and allows arguments to be omitted: such arguments are implicitly existentially quantified. In fact, any such atom entails a similar atom with some of the role-pairs omitted. Notice the difference in meaning between Married, (Married) and (Married (roleset:)). The first is a term which denotes the relational entity and makes no assertion. The second is an atomic sentence which asserts positively that Married is true of the empty sequence - probably false in the actual world - while the third, also an atomic sentence, merely asserts that Married is true of something, to which other things may be related by unknown roles: in effect, it asserts that a marriage exists, and so is true in the actual world.
This role-set convention does not itself specify any relationship between the same fact expressed as a role set and by using an argument sequence, but since Common Logic allows variadic relations, it is possible to use the same relation in both ways, and they can be related axiomatically. For example,
(forall (x y) (iff (Married x y) (exists (z) (and (Married z) (= x (wife z)) (= y (husband z))) ))
indicates the convention by which a wife must be the first argument of a marriage. Again, Common Logic provides for both kinds of syntax, separately or together, and can describe a relationship between them using Common Logic axioms.
Term Positions
It might be worth extending the notion of vocabulary to terms, and then the folds are natural extensions of the interpretation mappings. We need rel(t) becasue of t's position and so if we have int(t) we assign relation(int(t)) and define relation(t) = relation(int(t)). The only part of this that is a at all creative is the assignment, and that comes from B's interpretation.
Terms which occur in Common Logic text are required to play various semantic roles depending on the position in which they occur. This generalizes the usual notions of signature category for relation, function and individual names. If any term occurs in more than one position then it must be interpretable in several ways. In this section we define these positional notions, which are understood to be relative to a text.
Any term which occurs as the first term in any atomic sentence, or as the first item in a role pair, or paired with a bound variable in a quantifier, is said to occur in relation position. Terms in relation position must be interpretable as designating a relation.
Any term t which occurs as the first term in any other term of the form (tt1...tn) is said to occur in function position on n; if it is the first term in another term of the form (tt1...tn...x) ending with a sequence variable then it is said to occur in function position above n, or equivalently to occur in function position on m for all m>=n; and if it occurs as the first item in a role pair then it is in function position on 1. Terms in these positions are required to be interpretable as designating functions with the appropriate arity or arities.
Any name occurring as an argument of any other term or atom, or as the second item in a role pair, and any term other than a name, is said to be in object position, or to be a denoting term. Denoting terms are required to denote an individual in the domain of an interpretation.
The only terms which are not denoting terms in an expression are names which occur only in a function or relation position in that expression. Such names are not required to denote individuals (although in the Common Logic semantics, they may do so, allowing other pieces of text to be consistently added).
For example, in the following text (which is not intended to be particularly meaningful):
(iff (forall (x) (= (f (f x)) (f x)) ) (g f))
((f a) ((f a) a ...))
(R (roleset: (a b)))
the terms f, x, a, (f x), (f a) , (f (f x)) , ((f a) a ...) and b are all denoting terms; the terms g, R and (f a) all occur in relation position; f and a occur in function position on 1 while (f a) occurs in function position above 1. In this text, the term (f a) plays three distinct roles and the names a and f each play two roles. In contrast, b is only a denoting term and g and R occur only in relation position.
Clearly, if a term occurs in a position in a text then it also occurs in that position in any larger text. Concatenating two pieces of Common Logic text may therefore cause a term occurring in either one of them to be required to play more roles in the combined text.
Translating Common Logic atoms and terms into TFOL
Lets rewrite this using 'atom/term' for 'holds/app'. KISS.
Consider any Common Logic kernel text no seqvars T written using names from some vocabulary V. One can translate this into a TFOL text ha[T] with essentially the same meaning by applying the holds-app translation.
Might be best to do this without treating = specially, and distinguish these cases as ha= and rha=. Make this decision later when the lemmas are written.
The signature of ha[T] contains all of V, classified as individual names, plus the countable sets {holds-0, holds-1,...} of relation names with arities respectively 1, 2, ... and {app-0, app-1,...} of function names with arities respectively 2, 3,... , and the translation maps terms and atoms of T into those of ha[T] by the recursive application of the following translation rules to every atomic sentence in T
for any name n, ha[n] = n
for any term (t t1 ... tn), ha[(t t1 ... tn)] --> (app-n ha[t] ha[t1] ... ha[tn])
for any atom (t t1 ... tn) with t not equal to '=', ha[(t t1 ... tn)] --> (holds-n ha[t] ha[t1] ... ha[tn])
For example,
ha[(forall (x y) (implies (Boy x)) (exists (y) (and (Girl y) (Kissed x y) (= y (lover x)) )))]
=
(forall (x y) (implies (holds-2 Boy x)) (exists (y) (and (holds-2 Girl y) (holds-3 Kissed x y) (= y (app-2 lover x)) )))
The relation and function names of ha[T] play no real expressive role: they exist merely to provide a TFOL 'wrapper', allowing every name in V to be treated uniformly as denoting non-relational entities in the universe, i.e. individuals in TFOL.
Later we will show that T is satisfiable iff ha[T] is: in fact, that any model of T can be transformed into a model of ha[T], and vice versa. The construction is fairly obvious.
Its even nicer now, since the folds correspond exactly to the holds and apps.
If some symbols of V occur only in relation position in T, then a more restricted translation can be used in which the translation rules above are applied only to terms and atoms in V whose leading term has a subterm which also occurs in an object position, so that any parts of the vocbaulary which are strictly first-order are left unchanged by the translation. We will refer to this as rha[T]. For example, rha leaves the above example unchanged. This restricted translation is idempotent on TFOL texts, unlike the full translation; but it has the severe practical limitation of not being preserved under textual combinations.
Write T;S for the text obtained by concatenating the texts T and S, then we have for any T and S,
ha[T] =/= T
and
ha[T;S] = ha[T] ; ha[S]
In contrast, for any TFOL text T,
rha[T] = T
so that for example rha[rha[T]] = rha[T]; but there exist texts T and S with
rha[T;S] =/= rha[T] ; rha[S].
This will occur whenever a name is in object position in S but only in relation position in T, for example. An application which is translating Common Logic into TFOL using rha could therefore find itself needing to re-apply the translation mapping when new sentences are added to a text, which is likely to be an unacceptable cost for many applications.
Part of the intended function of the Common Logic header is to allow a common logic module to 'declare' explicitly which of the symbols in its vocabulary do not occur in object position, enabling a common logic engine to safely translate Common Logic into TFOL using the more efficient restricted rha mapping.
For convenience later, we define the inverse syntactic mappings ah and ahr by the equations ah[ha[x]] = x and ahr[rha[x]] = x
remark that seqvars can be translated using lists, which gets the whole language into TFOL.
Common Logic modules and headers
This whole section needs to be re-thought.
A common logic module is a named piece of Common Logic text, called the body text, with an optional formal preamble called a header. A module without a header is simply a named piece of Common Logic text which can be imported into other text by using the name inside an scl:imports expression, similar to an OWL ontology [refOWL].
Headers provide another level of functionality. The header is itself Common Logic text, interpreted using the same semantics (and hence subject to the same inference processes) as other Common Logic text; but the relationship between the semantics of the header and body text is special: in particular, the header is allowed to quantify over entities which are not in the intended universe of discourse of the body text. The primary intended roles of a header are to allow a module to describe its signature explicitly, to state syntactic conventions used in the body of the module, and to delineate and provide a name for the intended universe of discourse. These are often thought of as syntactic issues requiring translations between distinct languages: following the design principles of Common Logic, they are here handled withing the same language by using the same uniform semantic framework, allowing Common Logic processors to reason about the content of Common Logic modules. By convention, however, any inconsistency between the header of a module and the body text may be considered to be a syntactic error in the body text.
Headers may be defined to be countably infinite, provided that the effect of such an infinite header can be reproduced by a suitable computable operation on expressions. This convention can be used to provide a semantic connection between procedural 'attachments' or 'call-outs' and the model theoretic semantics, and to provide a coherent approach to the incorporation of data-structure conventions into Common Logic. This conventions, together with the use of the module naming convention, allows headers to describe certain kinds of 'closed-worlds', for example allowing Common Logic modules to act like databases when required.
There are 2 issues here. One is simply the advantages of being able to check syntax and provide guarantees of mergability and of being in a particular subcase. The other is this whole business of comparing universes of discourse and merging requiring protective guards on quantifiers. We may need to abandon the latter for the first draft.
In order to describe the interpretation of headers we need a new semantic notion. Say that an interpretation I is a shrinking of J, and that J is an expansion of I, when I can be obtained from J by deleting some things from the universe of I and possibly some names from the vocabulary. Formally, when the vocabulary of I is a subset of that of J, intI(v) =intJ(v) and relJ(v)=relJ(v) for all v in the vocabulary of I; UI is a subset of UJ, RI is a subset of RJ, and for all x in RI, relJ(x) = relI(x). Intuitively, the expansion J may include new individuals and some entirely new relations, but it cannot change the extensions of relations named in I.
Then the semantics of a module with a header can be stated as follows: an interpretation I fits a module when it is an interpretation of the body and has an expansion which satisfies the header, and it satisfies the module when it fits the module and satisfies the body:
if E is aof the formthen I(E) =module(scl:head head ) bodyif I(body)=true and for some expansion J of I, J(head)=true, then true; otherwise falseNote that an interpretation which satisfies the body but which cannot be expanded to satisfy the header is considered to be a non-fitting interpretation of the module: this is the sense in which the conditions expressed by the header are considered syntactic.The four relation names scl:Ind, scl:Rel, scl:Fun and scl:Arity are called the header vocabulary.
The header vocabulary can be used anywhere in any Common Logic text; but when used in a module header, the semantic conditions require that the header classifications are understood to refer to interpretations of the body of the module, rather than of the header itself. To see the difference this makes, consider the following module with an empty header:
(scl:module example1 ( (not (scl:Ind R)) ))
This is a contradiction - has no satisfying interpretations - since any interpretation which fits the inner sentence would require R to denote an individual in U, but the sentence asserts that is not in U.
The sentence
(forall (x) (scl:Ind x))
is a tautology in any module body, since scl:Ind is true of everything in the universe: one could in fact transcribe (scl:Ind term) in the body (though not in the header) as any tautologous assertion, in particular as ( term = term ).
However, the same sentence in the header yields a satisfiable module:
(scl:module example2 ((scl:head (not (scl:Ind R)) ) (R a) ))
This is satisfied for example by an Herbrand interpretation H in which the interpretation mapping is the identity, with UH={a}, RH={R} and extH(R)={}; the fit is guaranteed by the extension J with UJ={a, R}, RJ={R, scl:Ind} and extJ(scl:Ind)={}. Note that although R is an individual in J, it is not in H; and that the interpretation rules for the entire module require that extH(scl:Ind) = {}.
If the body of the module had 'mis-used' the relation symbol as an individual name, for example:
((scl:head (not (scl:Ind R)) ) (Q R) )
then once again the module would be unsatisfiable, since there are no interpretations which fit such a module, so no interpretations which satisfy it. It is useful to distinguish this kind of unsatisfiability from an unsatisfiability arising from a simple contradiction in the body of the module, such as:
( (Q R) (not (Q R)) )
since in the former case the body alone is satisfiable. The contradiction in the first case arises from an essentially syntactic incompatibility between the fitting conditions proscribed by the header and the actual usage in the body.
We will describe this case, of a module which has no interpretations which fit it, as an unfit module. Unfit ontologies have no interpretations, so have no satisfying interpretations; but their unsatisfiability arises from a different source than a mere contradiction. Common Logic applications may consider an unfit module to be a syntactic error, even if the unfitness can only be detected by semantic reasoning processes.
The header vocabulary can be used in fairly obvious ways to 'declare' constraints on the allowable signature of a module. A conventional first-order language can be specified by asserting scl:Ind of every individual, scl:Rel of every relation, and scl:Fun of every function, and specifying the arity of each relation and function using scl:Arity. For example, the following header specifies a small conventional first-order language signature suitable for expressing the earlier example:
Need a different example
Im not entirely happy with this header vocabulary. It would be better to have the ontology name itself be used as the name of its universe. This would allow one module to refer to the universe of discourse of another universe, and allow 'bridging' ontlogies to declare relationships between alternative universes of discourse. The arity/relation/function stuff is really only needed for syntax checking, but the universe of discourse is something deeper.
Which leads to the following thought. We need to be able to say that something is(/is not) in the universe of discourse, preferably in a way which can also be used meaningfully in another ontology. Which suggests a 'universe' functional, eg (scl:UOD ontologyname). The problem with this might be that it uses non-TFOL notation essentially: ((scl:UOD foo) x). Or we could have a general convention that an ontology name used as a predicate is that ontology's 'thing' classification... but this overloads the ontology name, which the W3Cers won't like. OK, need to take a decision on this.
It smells like the datatype trick of using the name both as a class and as a function. That overloading works OK, though, so why not this one?
BUt to return to the general point: what else do we need in the header vocabulary? To allow 'type checking' we need to be able to declare arity and functionality. Do we really need an explicit Rel?? Ans: yes, becus it has a direct syntactic check associated with it.
If Ind is relativized to an ontology, why aren't Rel and Fun also relativized? Ans: because Ind alone is connected with the quantifiers and with equality. In fact we need to get this connection with = sorted out better. Maybe = is enough: (ind x) is just (= x x). Aha! We havnt said what happens to the special vocabulary conditions in an expansion: clearly this is of critical importance, need to get it right. This might be the key.
Surely we will want = to mean = even in the header, right? So that meaning must be extendable, which already is a problem with the definition of expansion given. NEEDS MORE THOUGHT.
All of this is tightly connected with the Common Logic->TFOL embedding and the need to treat = specially. There is one important thing hidden here which I havnt got it completely straight yet. The idea is that when talking about A from 'outside', one has to interpret its quantifiers as restricted to its universe. The header has to be explicit about this 'outside' view.
Another thought: should importing be sensitive to the UOD? That is, the simple OWL-inspired importing is based on this unrealistic notion of a shared UOD, maybe we need to do better since we are facing up to this issue. But the simple case must be available as a syntactic default, so how do we manage that? One guideline is that importing a plain module ought to be the default case: which suggests that it is the header itself which declares the universe of discourse; just plain Common Logic text has no such committment. In turn suggests analysing more carefully what that process of naming really amounts to. Importing M requires that (OUD M) is the universe of the quantifiers in the sentences of M. Importing text is just a committment to satisfy it. On this view, then, giving a name to a module is a bigger deal; but what has that got to do with the header?? Nothing, so we don't get the easy default. Hmmm.
The older intuition was that one could transfer the header into the body with some quantifier restrictions. If so, importing these ought to be similar.
(scl:head
(forall (x) (not (and (scl:Ind x) (scl:Rel x) )))
(scl:Rel Boy Girl Kissed)
(= 1 (scl:Arity Boy))
(= 1 (scl:Arity Girl))
(= 2 (scl:Arity Kissed))
)
The first sentence expresses the conventional that relation symbols must not be used as individual names and vice versa: this is satisfied by every conventional first-order signature. The arity assertions here take advantage of the Common Logic fitting conditions. Note that it is consistent to allow a relation to take several different numbers of arguments, in general, so for example this is consistent:
(scl:Arity 2 R) (scl:Arity 3 R) (scl:Arity 5 R)
but the use of 'scl:Arity' in a function position requires that it denote a functional relation in any fitting interpretation; so the only consistent way to interpret this header is with scl:Arity interpreted as a functional relation, ensuring that all relations in the body have a fixed number of arguments.
Note that if the body of a module is syntactically correct TFOL, then including the appropriate header does not impose any extra conditions on the fit of an interpretation. It does however make these conditions explicit so that they can be checked.
Special Name Theories
Headers may also be used to declare special names of various forms. By convention, a header may be specified to be (equivalent to) a special name theory which consists of an recursively enumerable set of ground axioms specifying the positive and negative cases of some lexical categorization, typically the lexical space of a datatype represented by a predicate. Such headers can be imported into other headers, serving there as a form of declaration that the lexical forms are considered to be special names in the module body. In particular, Common Logic recognizes the built-in datatypes in HYPERLINK "http://www.w3.org/TR/xmlschema-2/" XML Schema Part 2: Datatypes [ HYPERLINK "" \l "ref-xmls" XML-SCHEMA2], listed in the following table:
XSD datatypes HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "string" xsd:string, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "boolean" xsd:boolean, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "decimal" xsd:decimal, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "float" xsd:float, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "double" xsd:double, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "dateTime" xsd:dateTime, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "time" xsd:time, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "date" xsd:date, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "gYearMonth" xsd:gYearMonth, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "gYear" xsd:gYear, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "gMonthDay" xsd:gMonthDay, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "gDay" xsd:gDay, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "gMonth" xsd:gMonth, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "hexBinary" xsd:hexBinary, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "base64Binary" xsd:base64Binary, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "anyURI" xsd:anyURI, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "normalizedString" xsd:normalizedString, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "token" xsd:token, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "language" xsd:language, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "NMTOKEN" xsd:NMTOKEN, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "Name" xsd:Name, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "NCName" xsd:NCName, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "integer" xsd:integer, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "nonPositiveInteger" xsd:nonPositiveInteger, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "negativeInteger" xsd:negativeInteger, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "long" xsd:long, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "int" xsd:int, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "short" xsd:short, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "byte" xsd:byte, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "nonNegativeInteger" xsd:nonNegativeInteger, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "unsignedLong" xsd:unsignedLong, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "unsignedInt" xsd:unsignedInt, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "unsignedShort" xsd:unsignedShort, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "unsignedByte" xsd:unsignedByte, HYPERLINK "http://www.w3.org/TR/2001/REC-xmlschema-2-20010502/" \l "positiveInteger" xsd:positiveInteger For each such name xsd:sss, the corresponding special name header consists of the axioms
(xsd:sss (xsd:sss name))
for each name which is a legal lexical form for xsd:sss;
(not (xsd:sss (xsd:sss name)))
for each name which is not a legal lexical form for xsd:sss;
(= (xsd:sss name1) (xsd:sss name2))
for each pair of names which are legal lexical forms for xsd:sss and map to the same item in the value space of xsd:sss. The datatype name serves here both as a function (mapping the lexical form to the value) and as a predicate on the value space: this follows the convention used in RDF [refRDF]. In addition, we use the datatype URI reference as the name for the module, so that the appropriate datatype can be included in a header by writing for example:
(scl:import xsd:nonPositiveInteger)
in the header. Note that importing a special name theory into the body of a module amounts to including an infinite set of axioms, but importing it into a header only imposes the appropriate semantic conditions on the special names actually used in the the vocabulary of the body.
When the header of a module imports a special name theory, then all the legal lexical forms of the theory are considered to be special names in that module.
The two remaining constructions allow ontologies to be given global names and to be imported into other ontologies. The idea of naming a module makes sense only if we can assume some 'global' naming convention which has a larger scope than a single module, and which interpretations are required to respect. In XCL we will use URI references as global names. in accordance with the emerging WWWeb conventions, which are elaborately described elsewhere. For semantic purposes, we simply assume that there is a fixed function ont from module names to module values. The exact nature of module values is not specified, other than that they are entities which can be parsed into Common Logic kernel syntax and to which an interpretation mapping can be applied. (One can think of a module value as a quoted string containing a character representation of a module written using the kernel syntax.)
Table SEQ Table \* ARABIC 4. Global names and importing.
if E is anof the formthen I(E) =phrase(scl:import name)false if I(ont(name)) = false, otherwise truemodule definition(scl:module name = (text))if for any interpretation J, J(ont(name)) = true iff J(text) = true, then true; otherwise false.An assertion of a module definition is required to have miraculous semantic powers: if it is ever true in any interpretation, then the name is attached to the defined module in all interpretations. Thus, if by convention we say that publishing any Common Logic module definitions amounts to asserting it, then a publication of a module definition requires any interpretation of any Common Logic module containing an importation of that name to treat it as having the same effect as copying out the sentences of the defined module in place of the importation. To actually achieve such miraculous powers requires a global naming convention: XCL uses universal resource identifiers (URIs) [refRFC2396] for this purpose.
Surface syntax.
It is clear that the 'same' logical expression can be rendered in a variety of different syntactic, or even graphical, forms: connectives can be written as infix, postfix or prefix, groupings indicated by brackets, groups of dots or graphically by enclosing circles, etc.. The differences in appearance between surface forms can be quite extreme. A simple logical expression written in introductory text-book form:
((x)(Boy(x) ( ((y)(Girl(y) & Kissed(x,y)))
appears in conceptual graph interchange form [ref CGIF] as:
[@every *x] [If: (Boy ?x) [Then: [*y] (Girl ?y) (Kissed ?x ?y) ]]
which is itself a 'linear' rendering of a diagrammatic representation:
Extremely compact notations have been used, such as the postfix convention which requires no parentheses:
KissedxyGirly&EyBoyxIAx
while at the other extreme, this example can be rendered as MathML [refMathML] content markup:
x
Boy
x
y GirlyKissedxy
give example in John's controlled English
To provide for information exchange between such a plethora of syntactic alternatives, Common Logic follows the lead of the KIF initiative by providing a single 'standard' logical interchange language XCL (based on XML rather than LISP)
Note. There is a divergence of ideas/approaches here. Best thinking is that the XML is the true 'abstract' syntax' for interchange and the core is simply a minimal 'clean' version of the language written using a KIF-style dialect. This will require rewriting this section. Stance wil be: XCL is for interchange, Kernel is for semantic specification and metatheory. XCL is rebarbative and extendable and covers all the syntactic options; Kernel is terse, minimal and easy to parse. Core is a KIF-like compromise for established logic applications, a useable extension to Kernel providing a variety of handy syntax forms. Also note that other dialects can be defined and indeed are encouraged, and XCL provides for their inclusion.
and a general technique for translating other notations, called Common Logic dialects, into XCL. One 'human-readable' Common Logic dialect, the Common Logic Core syntax, designed to be similar to KIF syntax, is defined carefully in this document using ENBF, and is used to give examples. A minimal subset of the core syntax, called the Common Logic kernel, which uses only conjunction, negation and simple universal quantification, is sufficient to express the meaning of all other forms. It is used to define the Common Logic model theory and to prove metamathematical results. All of Common Logic can be translated into the kernel, and the semantics is defined on the kernel syntax.
Following KIF, all Common Logic core expressions consist of a pair of parentheses enclosing the logical subexpressions of the expression in question, usually with a word immediately following the opening parenthesis which indicates the logical category of the expression. Atoms and terms are written in the form
(R a b) rather than the more usual R(a b) , and connectives are written as prefixes rather than infixed. The above example in Common Logic core syntax is:
(forall (x) (implies (Boy x) (exists (y) (and (Girl y)(Kissed x y) )) ))
which translates into the Common Logic kernel form
(forall (x) (not (and (Boy x) (forall (y) (not (and (Girl y)(Kissed x y) ))) )))
A detailed syntax for Common Logic Core is given later.
Common Logic can be expressed a variety of dialects, and this document defines several which provide Common Logic variants similar to existing logical notations in widespread use, and a general XML-based syntax, XCL, for general purposes of information exchange. XCL allows assertions to declare their dialect, and so can be used as a general-purpose interchange notation and mark-up language for any conforming Common Logic syntax. XCL is also considered to be the definitive 'abstract syntax' of Common Logic, in the sense that any language which can be parsed into XCL so as to preserve its semantic meaning may be considered to be a common logic dialect.
Contextual signatures
Conventionally, a first-order language is defined relative to a particular signature, which is a lexicon sorted into disjoint sublexica of individual names, relation names and perhaps function names, the latter two each associated with a particular arity, i.e. a fixed number of arguments with which it must be provided. This provides a simple context-free method of checking well-formedness of terms and atomic sentences, and ensures that any expression obtained by substitution of well-formed terms for variables will be assigned a meaningful interpretation.
The notion of signature is appropriate for textbook uses of logic and for stand-alone formalizations: but applied to an interchange situation, where sentences are distributed and transmitted over a network (in particular, on the WWWeb) and may be utilized in ways that are remote from their source, this would require either that a single global convention for signatures be adopted, or else that all communication between agents must involve a negotation about how to translate one signature into another. Both of which are impractical. Common Logic therefore is designed to have no built-in assumptions about signatures: it allows information to be combined even when it is written using divergent assumptions about the appropriate signature. In fact, there is no notion of signature in Common Logic syntax: it is replaced with the idea that the semantic role of a name - in fact, of any term - is determined by its syntactic context, that is, by the position it occupies inside another expression. This has a number of consequences for both the syntax and semantics of Common Logic.
Consider the situation of two agents A and B communicating information to C, and suppose that there is some concept used by both A and B but with different signatures. For example, A might use a relation married with two arguments (the people who are married), while B might use it with three (two people and a time-interval); or as a function from people to time-intervals. Cases like this can be handled very simply merely by allowing a symbol to play more than one role. Common Logic simply allows relation and function symbols to be variadic, i.e. to take any number of arguments, and it allows a relation name to be used as as function name and vice versa. Thinking in traditional terms, this amounts to allowing a kind of 'punning', often allowed in mechanized inference systems, where a single name is allowed to play several syntactic (and hence semantic) roles at once. Common Logic treats this more simply by conflating the various relational roles into a single notion of a variadic relation, and similarly for functions.
(Common Logic modules, described later, allow the user to fix the arity of any function or relation name if this is required, for example for purposes of syntactic checking.)
Note that this is purely a syntactic 'permission' to use a name in multiple roles: Common Logic does not assume any particular relationship between the truth of sentences in which the name plays these various roles, so for example (R a) (i.e., R with one argument) neither entails nor is entailed by (R a b) or (exists (x) (R a x)) or any other sentence constructed using R with two arguments; and similarly there are no logical entailments between sentences using R as a relation and other sentences using R as a function. Such conventions can be stated as axioms in Common Logic itself, but the Common Logic semantics does not impose them as a matter of logical necessity. Since there are no relevant logical principles which would mandate any such connection if distinct names were used for the various signature-distinct cases of the name, this punning does not violate the 'common logic' principle.
It is also possible that A uses a name such as married as an individual name while B uses it as a relation name. For example, A might have an ontology of interpersonal states, perhaps categorized in some way. It is important to understand that this is not necessarily an irreconcilable difference of opinion between A and B. The traditional Tarskian semantics for first-order logic requires that the universe of discourse be a nonempty set of things called 'individuals', but it does not mandate what kind of things must be in this set. In particular, there is no requirement that individuals be in any sense inherently non-relational in nature. Thus, A's use of a name to denote an individual, and B's use of the same name to denote a relation, need not be considered a difference of opinion: they can both be right, and can both correctly use first-order reasoning. In this case, however, the agent C who wishes to make use of both their sentences is faced with a dilemma, since traditional first-order signature-based syntax is unable to accomodate both points of view at once. Common Logic relaxes this rigidity and allows 'punning' between relation and individual names, as between relation and function names. In this case, however, the requirement that C must be able to understand both uses and still be able to reason appropriately has some more significant consequences. Since A can state equations between individuals and use terms to denote them, as for example in an equation such as
(= married (conjugalRelationBetween Joe Jane))
our 'common logic' requirement implies that C must be able to reason similarly, even when faced with an expression from B in which the name appears in a relation position:
(married Jack Jill)
The resulting expression has a term in a relation position and would be considered syntactically illegal in most traditional syntaxes for first-order logic:
((conjugalRelationBetween Joe Jane) Jack Jill)
However, it has a perfectly clear first-order reading which can be taken directly from the conventional readings of the sentences used by A and B, viz.: the relational entity which is the value of the term (conjugalRelationBetween Joe Jane), being identical to married, holds true between Jack and Jill.
Similarly, since A may use existential generalization on this individual name, for example to infer
(exists (x) (= x (conjugalRelationBetween Joe Jane)))
then C must be able to use similar logical inferences on the name, even when it occurs in sentences from B as a relation (or function) name, producing sentences even less conventional when viewed as first-order syntax:
(exists (x) (x Jack Jill))
Common Logic also allows this as legal syntax.
The resulting syntactic freedom allows a wide variety of alternative first-order axiomatic styles to co-exist within a common syntactic framework, with their meanings related by axioms, all expressed in a single uniform language. For example, the idea of marriage can be rendered in a formal ontology as a binary relation between persons, or a more complex relation between persons, legal or ecclesiastical authorities and times; or as as a legal state which 'obtains', or as a class or category of 'eventualities', or as a kind of event. Much the same factual information can be expressed with any of these ontological options, but resulting in highly divergent signatures in the resulting formal sentences. Rather than requiring that one of these be considered to be correct and the others translated into it by some external syntactic transformation, Common Logic allows them all to co-exist, with the connections between the various ontological frameworks to be expressed in the logic itself. For example, consider the following sentences (all written in the Common Logic core syntax):
(married Jack Jill)
(married (roleset: (husband Jack) (wife Jill)))
(exists (x)(and (married x) (= Jack (husband x)) (= Jill (wife x)) ))
(= (when (married Jack Jill)) (hour 3 (pm (thursday (week 12 (year 1997))))) )
(= (wife (married 32456)) Jill)
(ConjugalStatus married Jack)
((ConjugalStatus Jack) Jill)
These all express similar propositions about a Jack and Jill's being married, but in widely different ways. The logical name married appears here as a binary relation between people; a unary property of a state of affairs, with associated roles and fillers; a three-place relation between two persons and a time; a function from numbers to individuals; as an individual 'status', and finally, although not named explicitly, as the value of a function from persons to predicates on persons. In Common Logic all these forms can be used at the same time: the conjunction of the above set of sentences is syntactically correct Common Logic.
Common Logic also allows quantification over relations and functions. Common Logic syntax accepts the use of relation-valued functions, and relations applied to other relations, and so on. The resulting syntax is similar to that of a higher-order logic; but unlike traditional omega-order HO logic, Common Logic syntax is completely type-free. It requires no allocation of higher types to functionals such as ConjugalStatus, and imposes no type discipline. HOL languages traditionally requires quite elaborate signatures in order to prohibit 'circular' constructions involving self-application, such as
(rdfs:Class rdfs:Class)
Common Logic syntax, in contrast, is obtained from conventional FO syntax by removing signatureal restrictions, so that both Common Logic atomic sentences and terms can be described uniformly as a term followed by a sequence of argument terms. The above example, which expresses a basic semantic assumption of RDFS [RDFS], is legal (and meaningful) in Common Logic.
On being semantically first-order
Readers familiar with conventional first-order syntax will recognize that this syntactic freedom is unusual, and may suspect that Common Logic is a higher-order logic in disguise. However, as has been previously noted on several occasions [ref HILOG][refHenkin?], a superficially 'higher-order' syntax can be given a completely first-order semantics, and Common Logic indeed has a purely first-order semantics, and satisfies all the usual semantic criteria for a first-order language, such as compactness and the Skolem-Lowenheim property.
What makes a language semantically first-order is the way that its names and quantifiers are interpreted. A first-order interpretation has a single homogenous universe of individuals over which all quantifers range; any expression that can be substituted for a quantified variable is required to denote something in this universe. The only logical requirement on this universe is that is a non-empty set. Relations hold between finite sequences of individuals, and all that can be said about an individual is the relations it takes part in: there is no other structure. Individuals are 'logically atomic' in a first-order language: they have no logically relevant structure other than the relationships in which they participate. Expressed mathematically, a first-order intepretation is a purely relational structure. It is exactly this essential simplicity which gives first-order logic much of its power: it achieves great generality by refusing to countenance any restrictions on what kinds of 'thing' it talks about; it requires only that they stand in relationships to one another.
Contrast this with for example higher-order type theory, which requires an interpretation to be sorted into an infinite heirarchy of types, satisfying very strong conditions. In HOL, a quantification over a higher type is required to be understood as ranging over all possible entities of that type; often an infinite set. The goal of higher-order logic is to express logical truths about the domain of all relations over some basic universe, so a higher-order logic supports the use of comprehension principles which guarantee that relations exist. In contrast, Common Logic only allows the universe to contain relations, but imposes no conditions on what relations exist other than those required to ensure that every name has a referent.
In FO semantics, a relation name is interpreted as denoting a set of sequences of individuals, being the sequences between which the relation holds: call this a relation set, or a relational extension. In the Common Logic syntax, the same name might be used to refer to an individual. To retain the essentially first-order nature of the interpretation in cases like this, Common Logic assumes that a relation name used as an individual name must refer to an individual which, if it is ever called upon the play the role of a relation, is true of exactly the same sequences. The relational individual is 'associated' with same relation set as its name. This ensures that the name retains a single meaning in all contexts of use. The mappings which define such associations between individuals and relational and function extensions are called folds.
The intuition behind this terminology is the sense of 'folding' used in cookery: HYPERLINK "http://www.m-w.com/cgi-bin/dictionary?book=Dictionary&va=fold&x=16&y=19" Merriam-Webster Online Dictionary: fold[3, verb] sense 6: "6 a : to incorporate (a food ingredient) into a mixture by repeated gentle overturnings without stirring or beating; b : to incorporate closely."
Note that we do not assume that the individual denoted by the relation symbol is the relation set itself. While that interpretation might be thought set-theoretically more natural, to require an individual to be a large set containing structures containing other individuals would be a clear violation of the essentially first-order nature of Common Logic semantics.
This semantic strategy also allows several distinct individuals to be associated with the same relational extension, which provides an extra measure of descriptive flexibility. One can think of a relational individual as a relation in an intensional sense, and a relation set as a relation in a narrower extensional sense. Common Logic may be said to embody an intensional theory of relations as objects, although the Common Logic truth-conditions are purely extensional.
Sequences and sequence variables
Finite sequences play a central role in Common Logic syntax and semantics. Atomic sentences consist of an application of one term, denoting a relation, to a finite sequence of other terms. Such argument sequences may be empty, but they must be present in the syntax, as an application of a relation term to an empty sequence does not have the same meaning as the relation term alone.
Common Logic also allows relations to be take any number of arguments: such a relation is called variadic. (Married is an example of a variadic relation.) Common Logic follows KIF also in providing a special syntactic form called sequence variables to allow generic assertions to be made which apply to arbitrary argument sequences. Sequence varaibles are indicated in the Common Logic core syntax by an ellipsis ... optionally followed by a distinguishing character string. If an argument sequence ends with a sequence variable, then the presence of the variable indicates that the sequence may be arbitrarily extended, and the sentence is required to hold for all the possible extensions.
A common logic axiom using sequence variables can be viewed as a first-order axiom scheme, standing in for a countably infinite set of first-order instances.
Sequence variables are quite a powerful device: in effect, they allow a finite sentence to assert infinitely many quantifications all at the same time. Indeed, if arbitrary quantification over sequence variables is permitted, then the resulting language is a subset of the infinitary logic Lw1w, of a higher expressiveness than first-order logic, and for example is not compact [refHayMenzel]. The restrictions on sequence variables in Common Logic have been chosen to restrict the language to first-order while providing much of the practical utility of sequence variables for writing 'recursive' axioms to define lists and other recursively defined constructions. In Common Logic, sequence variables are allowed to occur only in the last position in an argument sequence, and are not bound by quantifiers: this keeps the language first-order and makes term-unification decideable [refKutsia]. Sequence variables can be replaced by a more conventional notation, at some considerable cost in elegance, by introducing argument lists explicitly: we provide a generic header which can be used for this kind of elimination, which is commonly adopted in practical KR notations.
Modules, headers, naming and importing
Common Logic text is any set or sequence of Common Logic top-level sentences, called Common Logic phrases.
The Common Logic core syntax uses sequences throughout, for convenience in defining iterative syntactic operations, but no particular significance attaches to the ordering of the sequence, and other Common Logic dialects may adopt a set-based syntactic convention.
A common logic module, or simply a module, is some Common Logic text together with an optional header consisting of Common Logic text, and which has a global name in the form of a Uniform Resource Identifier [refURI].Headers have a special semantic role and are treated in a distinct way in the semantics: they provide a general method for encoding syntactic and other 'background' information about the module. A special header vocabulary is provided which is sufficient to describe many standard signatures and syntactic conventions; but any Common Logic text may be included or imported into a header.
The terminology of "text" and "module" is intended to be a neutral terminology used to refer to any coherent piece of Common Logic which can be published, transmitted or asserted. It is not intended to convey any particular categorization or to indicate an intended use or philosophical stance. Other terms in widespread use in various communities include "ontology", "knowledge base", "axiom set" , "set of sentences", "metadata", "data model" and "model", as well as such particular usages as "RDF graph" and "document".
The core also provides an importing syntax, which indicates that a named module is being included into another module. The intended meanings of these constructions are fairly obvious, but the formal semantic statement requires that we assume the existence of a global module-naming convention, and that module names refer to entities in formal interpretations. This can all be stated abstractly, but is more directly conveyed by the observation that Common Logic uses the emerging semantic web conventions, as used in RDF and OWL, which are based on the W3C URI naming protocols [ref RFC2396]. The Common Logic 1.0 importing syntax provides only a very basic functionality for referring to modules, and we anticipate that it will be extended in future versions.
This "top-level" Common Logic syntax also provides for modules to declare their intended domain of discourse, and other functions intended to be useful in exchanging information.
Conformance
Editors Note: This is the heart of the document and is still undergoing discussion. It may be desirable to have levels of conformance (either syntactic and/or semantic) or it may be desirable to partition the standard into groups of features that are not ordered or hierarchical and then define conformance with respect to which groups a particular implementation supports.
Syntactic Conformance
This clause specifies semantic criteria for building inference systems that conform to the Common Logic standard.
Full Syntactic Conformance
An inference system EMBED Unknownhas full syntactic conformance with Common Logic if and only if it has simple semantic conformance with EMBED Unknown.
Restricted Syntactic Conformance
An inference system EMBED Unknownhas restricted syntactic conformance with Common Logic if and only if there exists a sublanguage EMBED Unknownsuch that EMBED Unknown has simple semantic conformance with EMBED Unknown.
First-Order Conformance
An inference system EMBED Unknownhas simple first-order conformance with Common Logic if and only if EMBED Unknown has simple semantic conformance with the sublanguage of EMBED Unknown that does not contain row variables.
Expanded Syntactic Conformance
An inference system EMBED Unknownhas expanded syntactic conformance with Common Logic if and only if there exists a sublanguage EMBED Unknownsuch that EMBED Unknown has simple semantic conformance with EMBED Unknown.
Semantic Conformance
This clause specifies semantic criteria for building inference systems that conform to the Common Logic standard.
Soundness
An inference system EMBED Unknownhas simple semantic conformance to EMBED Unknown if and only if there exists a syntactic mapping EMBED Unknownsuch that for any sentence EMBED Unknown that EMBED Unknowndecides to be satisfiable with module EMBED Unknown, there exists EMBED Unknownsuch that EMBED Unknownand EMBED Unknownis satisfied by a model of EMBED Unknown.
NOTE: This is equivalent to saying that an inference system is sound with respect to the semantics of Common Logic -- every sentence that the inference system decides to be satisfiable by a module, is satisfied by some Common Logic model of the module.
Completeness
An inference system EMBED Unknownhas strong semantic conformance to EMBED Unknown if and only if there exists a syntactic mapping EMBED Unknown such that for any sentence EMBED Unknown that is satisfied by a model of EMBED Unknown, there exists EMBED Unknown such that EMBED Unknown and EMBED Unknowndecides EMBED Unknownto be satisfiable withEMBED Unknown.
NOTE: This is equivalent to saying that an inference system is complete with respect to the semantics of Common Logic -- every sentence that is entailed by some Common Logic model of a module will be decided by the inference system to be satisfiable by the module.
AnnexA(normative)Knowledge Interchange Format (KIF) Syntax and Semantics
Editors note about the annexes
Annexes A, B, C, and D will have similar structure they are intended to specify standard forms for four logic formalisms that have been specifically tailored to conform completely to the Common Logic standard: KIF, CGIF, XCL and CLCE. They are all normative.
Annexes E, F, G and H will also have a similar structure to each other. They will demonstrate conformance for each of the standard formalisms in A through D. They are all informative.
Introduction
Historically, the Common Logic project arose from an effort, called the Common Logic initiative, to update and rationalize the design of KIF [refCL][refKIF], which was first proposed as a 'knowledge interchange format' over a decade ago and, in a simplified form, has become a de facto standard notation in many applications of logic. Several features of Common Logic, most notably its use of sequence variables, are explicitly borrowed from KIF. However, the design philosophy of Common Logic differs from that of KIF in various ways, which we briefly review here.
First, the goals of the languages are different. KIF was intended to be a common notation into which a variety of other languages could be translated without loss of meaning. Common Logic is intended to be used for information interchange over a network, as far as possible without requiring any translation to be done; and when it must be done, Common Logic provides a single common semantic framework, rather than a syntactically defined interlingua.
Second, largely as a consequence of this, KIF was seen as a 'full' language, containing representative syntax for a wide variety of forms of expressions, including for example quantifier sorting, various definition formats and with a fully expressive meta-language. The goal was to provide a single language into which a wide variety of other languages could be directly mapped. Common Logic, in contrast, has been deliberately kept 'minimal': the kernel in particular is a tiny language. This makes it easier to state a precise semantics and to place exact bounds on the expressiveness of subsets of the language, and allows extended languages to be defined as encodings of axiomatic theories expressed in Common Logic, or by reduction to the Common Logic kernel.
Third, KIF was based explicitly on LISP. KIF syntax was defined to be LISP S-expressions; and LISP-based ideas were incorporated into the semantics of KIF, for example in the way that the semantics of sequence variables were defined. Although the Common Logic core surface syntax retains a superficially LISP-like appearance in its use of a nested unlabelled parentheses, and could be readily parsed as LISP S-expressions, Common Logic is not LISP-based and makes no basic assumptions of any LISP structures. The recommended Common Logic interchange notation is based on XML, a standard which was not available when KIF was originally designed.
Finally, many of the 'new' features of Common Logic have been motivated directly by the ideas arising from new work on languages for the semantic web [refSW], and in particular, Common Logic is intended to be useable as a slightly improved Lbase [refLbase], i.e. as serving the role of a semantic reference language for other SW notations.
KIF Syntax
The syntax of KIF is described in three layers. First, there are the basic characters of the language. These characters can be combined to form lexemes. Finally, the lexemes of the language can be combined to form grammatically legal expressions.
In this clause, the syntax of KIF is presented using a modified BNF notation. The notation nonterminal* means zero or more occurrences; nonterminal+ means one or more occurrences; The nonterminals space, tab, return, linefeed, and page refer to the characters corresponding to ascii codes 32, 9, 13, 10, and 12, respectively. The nonterminal character denotes the set of all 128 ascii characters. The alphabet of KIF consists of 7 bit blocks of data. In this document, we refer to KIF data blocks via their usual ASCII encodings as characters (as given in ISO 646:1983).
Apart from being a smaller language, Common Logic Core syntax differs from KIF in the following respects.
(1) Variables are not required to be marked syntactically, and free variables are impossible.
(2) .... finish this list later and make it into an appendix or something: notes for implementers.
Characters
KIF characters are classified as upper case letters, lower case letters, digits, alpha characters (non-alphabetic characters that are used in the same way that letters are used), special characters, white space, and other characters (every ascii character that is not in one of the other categories).
::= A | B | C | D | E | F | G | H | I | J | K | L | M |
N | O | P | Q | R | S | T | U | V | W | X | Y | Z
a | b | c | d | e | f | g | h | i | j | k | l | m |
n | o | p | q | r | s | t | u | v | w | x | y | z
::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
::= @|#|?|`|.|=|/|[|:|%
::= !|$|%|&| * | + |,| - | ; | ] | ^ | _ | { | } | ~ | > | '
::= | | | |
::= | ( | ) | | \
::= | | |
Use of characters in special for word characters is discouraged as they may be given particular meaning in future versions of the standard or its extensions.
Lexemes
Character Strings
A character string is a series of characters enclosed in quotation marks. The escape character \ is used to permit the inclusion of quotation marks and the \ character itself within such strings.
::= | | (|)
::= *
Words
A word is a letter or digit followed by any number of other legal word characters.
::= { | }
::= +
For the purpose of grammatical analysis, it is useful to subdivide the class of words a little further, viz. as variables, operators, and constants.
Object Variables
An object variable is a word in which the first character is ?.
::= ?
Row Variables
A row variable is a word in which the first character is @.
::= @
Operators
Operators are used in forming complex expressions of various sorts. Within KIF, there are only sentence operators, which are used in forming complex sentences.
::= = | not | and | or | implies | iff forall | exists
Constants
All other words are called constants.
::= - -
Expressions
The legal expressions of KIF are formed from lexemes according to the rules presented in this clause.
KIF Languages
A namespace N consists of a recursive set of words. The elements of this namespace are constant names that refer to the distinguished individuals, properties, classes, and relations in a conceptualization.
The KIF language lN g e n e r a t e d b y t h e n a m e s p a c e N i s t h e s e t o f e x p r e s s i o n s g e n e r a t e d b y t h e a b o v e B N F w h e n N i s t h e s e t o f a l l <