Patrick
Hayes Institute for Human and Machine Cognition phayes@ihmc.us |
Christopher
Menzel Department of Philosophy Texas A&M University cmenzel@tamu.edu |
Simple Common Logic, or SCL, is a proposal for a unified syntactic/semantic framework for expressing full first-order logical content for transmission on a knowledge network such as the Web. SCL is the draft which was was recently submitted for ISO standardization as Common Logic, and has been incorporated into the OMG Ontology Definition Metamodel (ODM) standard. SCL extends conventional first-order notations in various ways and is a candidate formalism for expressing content which is currently represented in both description logics and rule languages. This paper outlines the design considerations of SCL and summarizes the main features of the proposal.
The chief design requirements for SCL were (1) that it should be a full first-order logic (with equality), with a conventional semantics which supports conventional proof theories; (2) that it should be described in a way which allows for a variety of surface forms to co-exist; and (3) that it should allow for free interchange of information on an open network without requiring complex translations or negotiations between agents. The first requirement rules out exotica such as modal, free, intuitionist, hybrid or other logical variations, although syntactic "hooks" are provided for adding them as extensions to SCL. The second requirement is met by describing the syntax of SCL abstractly and requiring concrete syntaxes ("dialects") to be specified in terms of the syntax classes of the abstract syntax. This allows for a variety of existing logical notations to be considered as SCL dialects if required. The third requirement has the most influence on the language, and requires an extended discussion.
Consider the following scenario. Two agents, A and B, each have a logical formalization of some knowledge and wish to communicate their knowledge to a third agent C which will make use of the combined information so as to draw some conclusions. 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. As far as possible, we want to make sure that C can use information independently of the particular styles used by A and B.
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 by allowing a symbol to play more than one role. SCL 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 a function name and vice versa. SCL conflating the various relational roles into a single notion of a variadic relation, and similarly for functions.
It is also possible that A uses a name such as "married" as an individual name while B uses it as a relation name. 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; in fact, it is quite common to introduce relations into a first-order theory by treating them as arguments to a "dummy" relation, writing expressions such as "(Holds R a b)" rather than "(R a b)". Thus, A's use of a name to denote an individual, and B's use of the same name to denote a relation, can both be right, and they can both correctly use first-order reasoning. In this case, however, the agent C is faced with a dilemma, since traditional first-order signature-based syntax is unable to accommodate both points of view at once. SCL relaxes this rigidity and allows "punning" between relation and individual names, as between relation and function names.
In this case, the requirement that C must be able to understand both A and B, 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))" the 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 meaning which can be taken directly from the conventional first-order 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, again, C must be able to use similar logical inferences on the name, even when it occurs in sentences from B as a relation name, producing sentences which are even less like conventional first-order syntax: "(exists (x) (x Jack Jill))" SCL also allows this as legal syntax, and treats it semantically in a first-order way: it asserts that there is something in the universe which can play a relational role and, in that role, is true between Jack and Jill; and of course, in this situation, there is indeed such an entity in the universe, viz. the denotation of the individual name married as used by A. 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. SCL also allows quantification over relations and functions and accepts the use of relation-valued functions, relations applied to other relations, and so on. The resulting syntax is reminiscent of a higher-order logic: but unlike traditional higher-order logic, SCL syntax is completely type-free. It requires no allocation of higher types to functionals such as ConjugalStatus, and imposes no type discipline. Higher-order languages traditionally require more elaborate signatures than first-order languages, in order to prohibit "circular" constructions involving self-application, such as "(rdfs:class rdfs:class)" (which expresses a basic semantic assumption of RDFS.) SCL syntax, in contrast, is obtained from conventional first-order syntax by removing signature restrictions, so that both SCL atomic sentences and terms can be described uniformly as a term followed by a sequence of argument terms. Such circular constructions are syntactically legal and semantically meaningful in SCL.
The resulting syntactic freedom can go a long way to overcoming interoperability problems, by allowing SCL axioms to be written which express relationships that would previously have required translations between different logical frameworks. For example, the following is legal SCL text (written in the core dialect) which expresses the same fact (in varying levels of detail) in a variety of formats:
The logical name "married" in these examples designates:
and, finally, although not named explicitly
In a fully expressive SCL dialect all these forms can be used at the same time, and can be related by SCL axioms such as
(forall (x y z) (implies (and (ConjugalStatusRelation x) (x y z)) (exists (t) (and (TimeInterval t) (= (when (x y z)) t)))))
which says that marriages must last for some time-period.
The abstract syntax of SCL can be described very compactly:
This completely describes the abstract syntax of SCL. Rules would appear typically as implications. The SCL specification requires any concrete syntax to map to these categories, but it may omit some, and may include other sentence forms provided they can be defined as syntactic sugar, eg restricted quantification, role-filler syntax for atoms and terms, other connectives are all permissible in SCL dialects. This allows for example a Horn rule language to be declared as an SCL dialect, provided its expressions can be given a logical semantic meaning.
Such constructions as modal sentences or non-monotonic operators, which cannot be reduced to first-order sentences, are required to parse as irregular sentences and are treated semantically in SCL as opaque sentence forms, i.e. essentially as propositional variables. Semantic extensions can however add further semantic conditions, and the resulting languages are considered to be SCL conformant if they respect the other SCL conformance conditions.
SCL has OWL-style importing, and the SCL semantics has a full treatment of the semantic conditions which are required for names to be used as identifiers for SCL Web resources. In addition, modules allow a text to be considered to have a "smaller" universe of discourse than the global one assumed on the communication network. This could be considered syntactic sugar, but providing it as a syntactic construction in the language facilitates the interoperabilty of dialects which forbid some names to denote (such as many existing first-order notations) with the more permissive SCL syntax style.
Space does not permit a full statement of the SCL semantics. For formal details, see Abstract Syntax and Semantics for SCL; for a somewhat friendlier version, see SCL: Simple Common Logic. SCL can be processed by any conventional first-order reasoner, but its syntactic style may obstruct some reasoning optimizations.
The SCL effort has produced two "official" dialects: the SCL core, modeled closely on KIF syntax, and XCL, a comprehensive but unreadable XML-based notation into which all other SCL dialects can be translated or transcribed. XCL is designed to be extendable, and to allow the recording of a variety of meta-information associated with SCL expressions, including for example the fact that a particular expression is in a named subclass. It is straightforward to translate OWL and SWRL into SCL so as to preserve semantic meanings (see Translating Semantic Web languages into SCL). This feature also allows the translations to be marked up in such a way that processors can identify their computational or processing subclass without needing to re-parse them. This allows XCL to fully express the logical form of a rule or a DL expression in a way that is semantically uniform across the full spectrum of SCL notations but also allows rules to be transmitted without losing their identity as rules, i.e. as belonging in a particular sub-language that admits particular styles of processing.
SCL follows KIF in allowing sequence variables, but restricts them to be free. This allows the expression of recursive axiom schemas without using an explicit fixed-point operator. As an example, the use of argument lists can be axiomatized in SCL thus (written in the core syntax where the three-dot ellipsis indicates a sequence variable):
(= nil (list)) (forall (x z) (iff (= x (list ...) (= (cons z x) (list z ...))) (forall (x) (iff (x ...) (x (list ...)) )) (forall (x) (= (x ...) (x (list ...)))
This gives the "Lisp" style (P (cons a (cons b (cons c nil)))); for the "RDF style" one would add the axioms
(= rdf:nil nil) (forall (x z) (iff (= x (list ...) (exists (y) (and (rdf:first y z) (rdf:rest y x) (= y (list z ...)))))
and now these are all logically equivalent:
(P a b c) (P (list a b c)) (P (cons a (cons b (cons c nil)))) (exists (l m n) (and (P l) (rdf:first l a) (rdf:rest l m) (rdf:first m b) (rdf:rest m n) (rdf:first n c) (rdf:rest n rdf:nil) ))
However, SCL axioms can also use the simple (P (list a b c)) form directly. The SCL core dialect has XSD datatypes built-in and also recognizes numerals and string quotation. It allows arbitrary character strings to be used as names, including URIs and URI references. It also allows atomic sentences to be expressed using role-value pairs rather than argument sequences, e.g., "(married (roleset: (husband Jack)(wife Jill)))".