26 October 2003
Abstract. Common Logic (CL) is a framework for analyzing, specifying, and relating the semantics of a family of declarative languages and notations. Its purpose is to ensure that content exchanged between CL-conformant languages has identical semantics in each language. Among the languages in the CL family are first-order predicate calculus, the Knowledge Interchange Format (KIF), the Conceptual Graph Interchange Format (CGIF), the Web Ontology Language (OWL), the Resource Description Facility (RDF), and RDF Schema (RDFS). Closely related languages that are also being considered as potential members of the CL family include the Z Formal Specification Language (Z), the Unified Modeling Language (UML), and the language of the Cyc Project (CycL). The CL Working Group is also developing a methodology that the designers and implementers of declarative languages can use to specify a CL-conformant semantics for their language. This report presents an overview of the status, goals, and directions of the CL project and includes some material extracted from documents produced by members of that project.
Note: This report uses mathematical and logical symbols that are not supported by older browsers, such as Internet Explorer 5.x and 6.x. Readers should download a modern browser, such as Mozilla 1.x, Netscape 7.x, or the compact and speedy Firebird. (These browsers are also less susceptible to the viruses that plague IE.)
Common Logic (CL) is a framework for a family of logic-based languages that are used for knowledge representation, software design, and ontology specification. CL semantics is defined in terms of an abstract syntax that can be specialized to the concrete syntax of any language in the CL family. The Common Logic Working Group has produced a series of documents, which define the semantics of CL, its abstract syntax, and the methods for relating the abstract syntax of CL to the concrete syntaxes of other versions of logic. Members of the CL Working Group have been collaborating with standards organizations, with the W3C Consortium, and with the developers of other versions of logic to ensure that the CL semantics can support a wide range of logics. The ultimate goal is to promote the interchange of content and interoperability of tools among heterogeneous systems that use various logic-based languages.
All modern systems of logic, including CL, are based on the work of two pioneers, Gottlob Frege (1879) and Charles Sanders Peirce (1880, 1885), who independently developed notations for what is now called first-order logic. Frege's version, which he called Begriffsschrift (concept writing), had a tree notation, which no one else adopted, but which incorporated many important ideas that had a strong influence on later developments. Peirce's notation, which was based on a generalization of Boolean algebra, was adopted by Giuseppe Peano (1889), who modified some of the symbols to create today's most widely used notation for logic. In 1897, Peirce invented a graphic notation, called existential graphs, which had exactly the same expressive power as as his earlier algebraic notation and Frege's Begriffsschrift.
To illustrate these notations, consider the English sentence Every cat is on a mat and its translations to logic. In Peirce's algebraic notation of 1885, that sentence could be expressed by the following formula:
Π_{x} Σ_{y} (cat_{x} (mat_{y} × on_{x,y}))Peirce called Π_{x} a universal quantifier, which may be expressed by the phrase for every x. He called Σ_{y} an existential quantifier, which may be expressed by the phrase there exists a y. Peirce followed Boole in using the symbols + for or and × for and. For implication, he introduced the symbol , which may be read if-then. Literally, the formula may be read For every x, there exists a y such that if x is a cat, then y is a mat and x is on y. Peano adopted Peirce's notation, but he changed the symbols because he wanted to reserve +, ×, Π, and Σ for mathematical operators. The following formula in the modern notation of predicate calculus uses Peano's symbols:
∀x ∃y (cat(x) ⊃ (mat(y) ∧ on(x,y)))Since Peano adopted his notation from Peirce, it is not surprising that it has the same semantics. What is remarkable is that the algebraic formulas have the same semantics as the diagrams in Figure 1, which use Frege's notation of 1879 and Peirce's notation of 1897.
Figure 1: Two representations for Every cat is on a mat
For the Begriffsschrift, Frege used only four operators: a vertical bar at the left of the formula to represent an assertion; a cup symbol, which contains a variable such as x to represent a universal quantifier; a short downward line to represent negation; and a hook symbol to represent implication. The Begriffsschrift in Figure 1 may be translated to the following formula:
∀x (cat(x) ⊃ ~(∀y (mat(y) ⊃ ~on(x,y))))This formula may be read For every x, if x is a cat, then it is false that for every y, if y is a mat, then x is not on y. This roundabout paraphrase is logically equivalent to the previous formulas for Every cat is on a mat. Peano was familiar with Frege's work, but he said that its convoluted paraphrases were "unreadable."
For existential graphs, Peirce chose a different set of four operators: the act of writing a graph on a blank "sheet of assertion" was the equivalent of Frege's vertical bar; conjunction or and was represented by writing two or more graphs or subgraphs in the same area of a sheet; negation by drawing an oval around the graph or subgraph to be negated; and existence by a bar or "line of identity", which was attached to the names of the relations. The EG in Figure 1 could be translated to the following formula:
~(∃x (cat(x) ∧ ~(∃y (mat(y) ∧ ~on(x,y)))))This formula may be read It is false that there exists a cat x and there does not exist a mat y for which x is on y — or more simply, There is no cat that is not on a mat. Although existential graphs do not have a primitive for if-then, Peirce treated a nest of two ovals as an implication. His reading of the EG in Figure 1 would be If there is a cat, then it is on a mat.
All the notations above were invented in the 19th century, and except for Frege's Begriffsschrift, they are still used today. In the 20th century, more syntactic innovations were invented for a variety of reasons, such as human readability, computational efficiency, or ease of translation to or from other notations. One innovation that can improve both human readability and computer efficiency is to include a type or sort restriction on the quantifiers. With that option, the sentence Every cat is on a mat could be translated to the following formula:
(∀x:Cat)(∃y:Mat)on(x,y)Literally, this formula may be read For every x of type Cat, there exists a y of type Mat such that x is on y. Despite the differences in notation, this formula is logically equivalent to each of the linear and graphic notations above.
Working independently, Frege and Peirce developed very different notations with different choices of primitives, yet their notations had identical semantics: anything expressed in either one can be translated to the other without loss or distortion. That commonality in semantics despite variability in notation indicates something fundamental about first-order logic that transcends notation. The common core of first-order logic, or some subset of it, is also present in most of the declarative languages that are in use today. Many languages also implement extensions to FOL for modal logics, metalanguages, and quantifiers that range over predicates; those extensions can also be handled with a small number of additional semantic features.
The goal of the CL project is to standardize the common semantics that underlies the superficial variations. Most of the declarative languages used for databases, knowledge bases, and the semantic web can be represented with a common semantics and with a systematic methodology for relating the concrete syntax of each language to a common abstract syntax that would be the same for all. This report presents an overview of the problems involved, the solutions proposed by the CL Working Group, and the methodology for relating current languages to the common semantics.
The Common Logic project evolved from two separate projects to develop standards for the Knowledge Interchange Format (Genesereth & Fikes 1998) and Conceptual Graphs (Sowa 2001). The editors of both projects tried to keep their semantics as similar as possible, but they realized that maintaining parallel updates to two documents was harder than adopting a common foundation for both. Therefore, they agreed to define the semantics in terms of a common abstract syntax and to relate it to the concrete syntaxes of KIF and CGs. As an example, Figure 2 shows a conceptual graph for the sentence Every cat is on a mat.
Figure 2: Conceptual graph for Every cat is on a mat
A diagram such as Figure 2 is called the display form for conceptual graphs. It is a highly readable graphic notation, but it is not suitable for interchange between systems. The Conceptual Graph Interchange Format (CGIF) is a logically equivalent linear notation, which is used to store CGs in a compact form and to interchange CGs between different implementations. Following is the CGIF version of Figure 2:
[Cat: @every*x] [Mat: *y] (On ?x ?y)The concrete syntax for CGIF is defined in terms of the CL abstract syntax, which enables CGIF to inherit the CL semantics. Following is the equivalent statement in KIF:
(forall ((?x Cat)) (exists ((?y Mat)) (On ?x ?y)))Although the CL abstract syntax does not have any printable form, it can be represented directly in an XML version called Common Logic Markup Language (CLML). Following is a CLML representation for Every cat is on a mat:
<formula> <forall> <var>x</var> <formula> <implies> <formula> <atom> <con>Cat</con> <var>x</var> </atom> </formula> <formula> <exists> <var>y</var> <formula> <and> <formula> <atom> <con>Mat</con> <var>x</var> </atom> </formula> <formula> <atom> <con>On</con> <var>x</var> <var>y</var> </atom> </formula> </and> </formula> </exists> </formula> </implies> </forall> </formula>Systems that use conceptual graphs as their internal representation can use CGIF for knowledge interchange. Many knowledge-based systems and theorem provers use KIF. But systems that are based on XML tools can use CLML. Any other notations that conform to the CL semantics and abstract syntax can be automatically translated to CLML, KIF, or CGIF.
One of the members of the CL Working Group, Patrick Hayes, worked as a consultant to the W3C Working Group to apply the CL semantics to the languages being developed for the Semantic Web. The result is the logic base (LBase) for the Web Ontology Language (OWL) and the Resource Description Facility (RDF) (Guha & Hayes 2003). The formal definitions in LBase enable anything represented in the semantic web languages to be translated automatically to the languages in the CL family. Therefore, the tools developed to support CL languages can be use to process information extracted from the semantic web.
In logic, the existential quantifier ∃ is a notation for asserting that something exists. But logic itself has no vocabulary for describing the things that exist. Ontology fills that gap: it is the study of existence, of all the kinds of entities — abstract and concrete — that make up the world. Ontology supplies the predicates of predicate calculus and the labels that fill the boxes and circles of conceptual graphs. A choice of ontological categories is the first step in designing a database, a knowledge base, or an object-oriented system. In database theory the categories are usually called domains, in AI they are called types, in object-oriented systems they are called classes, and in logic they are called types or sorts. Whatever they are called, the selection of categories determines everything that can be represented.
Although logic is the most precise and the most fundamental of all declarative languages, it is by no means the only one. New notations, both graphic and linear, are constantly being invented in every field of science, engineering, business, and art. Musical notation, for example, has a history as long as logic. The mathematical relationships between the notes and scales were discovered by Pythagoras and his followers in ancient Greece. The modern notation with notes, staves, and clefs was developed by medieval monks working next door to the ones who were busily copying the textbooks on logic. Yet musical notation and other specialized notations are not competitors, but supplements to logic. Each of them represents a subset of logic with a built-in ontology tailored to a particular domain of interest.
Figure 3: A sample melody to be represented in logic
As an example, Figure 3 shows a sample melody, called "Frère Jacques" in French or "Brother John" in English. At the beginning of the first line, the key signature indicates one sharp for the key of G; the time signature 4/4 indicates 4 beats per measure with the quarter note having a duration of one time unit. The vertical bars divide the melody in 8 measures, with a total of 32 notes. The vertical position of each note on the staff indicates a tone, designated by a letter from A through G (the letter may be qualified by a sharp or flat sign or by a number that indicates the octave). The shape of the note indicates duration: one time unit or beat for a quarter note; two units for a half note; or half a unit for an eighth note. The horizontal position of each note indicates that it is sounded after the one on the left and before the one on the right. These features, which represent the elements of an ontology for music, can be translated to logic supplemented with three predicates or relations:
(∃x_{1})(∃x_{2})(∃x_{3})...(∃x_{3}_{2}) (tone(x_{1},G) ∧ dur(x_{1},1) ∧ next(x_{1},x_{2}) ∧ tone(x_{2},A) ∧ dur(x_{2},1) ∧ next(x_{2},x_{3}) ∧ tone(x_{3},B) ∧ dur(x_{3},1) ∧ next(x_{3},x_{4}) ∧ ... ∧ tone(x_{3}_{2},G) ∧ dur(x_{3}_{2},2)).
Any musician would prefer to read music in the familiar notation of Figure 3 than in a translation to any of the notations for logic illustrated in Section 1. But a translation to logic is a step toward implementing a program for analyzing the music or synthesizing it digitally. Logic is an ontologically neutral notation that can be adapted to any subject by adding one or more domain-dependent relations. The full musical notation has many more features than those shown in Figure 3. Loudness, for example, is usually represented by abbreviations like mf for mezzoforte (medium loud). That feature could be represented by a predicate mf(t_{1}, t_{2}), which indicates that a mezzoforte passage extends from time t_{1} to t_{2}. But loudness is a continuously varying feature that is only roughly approximated by an abbreviation mf or predicate mf(t_{1}, t_{2}). Subtle gradations in volume, timing, and phrasing make all the difference between a performance by Jascha Heifetz and the kid next door practicing the violin. Neither the musical score nor the logical formula represents those differences; each captures or omits exactly the same information.
Another observation about the translation gets to the essence of what logic can contribute: the only logical operators used in the formula are the existential quantifier ∃ and the conjunction ∧. As a musical score becomes more detailed and complex, new kinds of predicates like mf(t_{1},t_{2}) may be needed, but the universal quantifier ∀ and the other Boolean operators are never used. The existential-conjunctive (EC) subset of logic with only ∃ and ∧ is a common version used to represent the basic data of many different fields. It is also the subset used for all the information stored in commercial database systems, both relational and object-oriented. EC logic is therefore an extremely important subset, but it has one serious limitation: it cannot represent any generalizations, negations, implications, or alternatives. For that, the operators ∀, ~, ⊃, and ∨ are necessary.
One useful generalization is the principle that certain intervals are difficult to sing and should be avoided. In particular, the interval of three whole tones, called a tritone, is considered so dissonant that it was called the diabolus in musica in the Middle Ages. In the key of C, the tritone is the interval from B to F or from F to B; in the key of G, it is the interval from F# to C or from C to F#. The next formula rules out the transition from B to F:
This formula says that for every x and y, if the tone of x is B and the next note after x is y, then the tone of y is not F. More rules like this would be needed to rule out the transition from F to B, from C to F#, and so on. A more general rule could be stated in terms of another predicate called tritone:(∀x)(∀y)((tone(x,B) ∧ next(x,y)) ⊃ ~tone(y,F)).
This formula says that for every x, y, z, and w, if the next note after x is y, the tone of x is z, and the tone of y is w, then z and w do not form a tritone. Rules like this cannot be stated in traditional musical notation because they use the operators ∀, ⊃, and ~.(∀x)(∀y)(∀z)(∀w) ((next(x,y) ∧ tone(x,z) ∧ tone(y,w)) ⊃ ~tritone(z,w)).
The song "Frère Jacques" is intended to be sung as a round, in which a second voice begins the melody when the first voice reaches measure 3. That kind of parallelism tends to be obscured by a linear notation, and graphs can often show the relationships more clearly. To show the third measure with two voices singing in harmony, Figure 4 uses a conceptual graph. Each of the seven notes in the measure is represented by a separate concept [Note]. Each note is attached to conceptual relations that correspond to the tone, next, and dur predicates: the Tone relation links the concept of the note to a concept that indicates the type of tone; the Next relation links to the concept of the next note; and the Dur relation links to a concept of a time interval of the specified duration. Two notes that are sounded simultaneously are linked to the same concept. But at the end of the measure, the upper voice is a half note that lasts as long as the two quarter notes in the lower voice. Therefore, the interval for the half note is linked by two Part relations to the intervals for each of the quarter notes.
Figure 4: Conceptual graph for two voices singing in harmony
Each concept box in Figure 4 represents something that exists: a note, an interval, or a type of tone. When the CG is translated to predicate calculus, the corresponding existential quantifiers must be shown explicitly:
(∃x_{1},x_{2},x_{3},x_{4},x_{5},x_{6},x_{7}:Note) (∃y_{1},y_{2},y_{3},y_{4},y_{5}:Interval) (tone(x_{1},B) ∧ dur(x_{1},y_{1}) ∧ hasAmount(y_{1},1beat) ∧ next(x_{1},x_{2}) ∧ tone(x_{2},C) ∧ dur(x_{2},y_{2}) ∧ hasAmount(y_{2},1beat) ∧ next(x_{2},x_{3}) ∧ tone(x_{3},D) ∧ dur(x_{3},y_{3}) ∧ hasAmount(y_{3},2beat) ∧ tone(x_{4},G) ∧ dur(x_{4},y_{1}) ∧ next(x_{4},x_{5}) ∧ tone(x_{5},A) ∧ dur(x_{5},y_{2}) ∧ next(x_{5},x_{6}) ∧ tone(x_{6},B) ∧ dur(x_{6},y_{4}) ∧ hasAmount(y_{4},1beat) ∧ next(x_{6},x_{7}) ∧ tone(x_{7},G) ∧ dur(x_{7},y_{5}) ∧ hasAmount(y_{5},1beat) ∧ part(y_{3},y_{4}) ∧ part(y_{3},y_{5}) ).The quantifiers at the beginning of this formula specify x_{1} through x_{7} as notes and y_{1} through y_{5} as intervals. What makes the formula difficult to read is not the quantifiers, but the proliferation of variables. In the graph, all the information about an entity is localized — either inside the concept box itself or in the relations attached directly to the box. But when the graph is mapped to a linear string, there is no way to preserve the locality of information: the variables that represent the links tend to get scattered throughout the formula.
Since Figure 4 is a direct translation from a musical score, it uses only the existential-conjunctive subset of logic. But logic, in both the graphic and linear notations, has much more expressive power for stating rules and generalizations about music.
The full scope of the CL semantics is still under discussion, but an essential core, called Simplified Common Logic (SCL), is defined in this section. SCL supports full first-order logic plus features that enable quantifiers to range over relations. Those features enable SCL to support metalanguages and many other versions of logic while retaining a first-order style of model theory. The LBase used for the semantic web languages is a subset of SCL.
SCL provides an abstract syntax that can be realized in infinitely many distinct forms called concrete syntaxes. Each syntax consists of a stock of initial lexical elements and a grammar that specifies the classes of terms and formulas built upon those elements. A language is defined as a set of formulas generated by a given grammar and a given lexicon. SCL specifies the structural constraints that must be met for any such language to be considered conformant.
An SCL language is based upon an initial stock of primitive syntactic entities. Specifically, an SCL lexicon λ will consist of the following sets:
If SeqVar is empty, then λ is known as a first-order lexicon.
Con = PredCon ∪ IndCon is known as the set of constants of λ. Var = GenVar ∪ SeqVar is known as the set of variables of λ. GenVar and SeqVar shall be disjoint, and Var shall be disjoint from Con ∪ FnSym. Let PrimTrm = IndCon ∪ GenVar. PrimTrm is known as the set of primitive terms of λ.
Lexicons λ also come with a function arity that maps each predicate constant and function symbol into the set N ∪ {ω}, where N is the set of natural numbers and ω is any object not in N. For predicates π, arity will indicate the number of arguments π will take. (This will of course be expressed explicitly in the grammar below.) If arity(π) = n ∈ N, then π is said to be an n-place predicate; otherwise π is variably polyadic. Variably polyadic predicates will be able to take any number of arguments. We let PredCon_{n} be the set of n-place predicates, and PredCon_{ω} the set of variably polyadic predicates. Because we will interpret function symbols as functional relations, we will let the arity of a function symbol correspond to the arity of the relation it denotes rather than to the number of arguments it takes. This will also enable the predicates of an SCL lexicon to do double duty as function symbols — note that there is no requirement that PredCon and FnSym be disjoint. Accordingly, for function symbols α, if arity(α) = n+1, we say that α is an n-place function symbol; otherwise α is variably polyadic. We stipulate that arity(α) ≠ 0, for any function symbol α. We let FnSym_{n} be the set of n-place function symbols, and FnSym_{ω} the set of variably polyadic function symbols.
Over and above presence of sequence variables, SCL lexicons differ from traditional first-order lexicons in three important ways. First, SCL generalizes the notion of arity by allowing variably polyadic predicate constants and function symbols, i.e., predicate constants and function symbols that can take arbitrarily many arguments. Variably polyadicity is especially useful and appropriate in SCL languages containing sequence variables.
Second, it is not required that PredCon, IndCon, and FnSym be pairwise disjoint. This reflects SCL's goal of generality. Many knowledge representation languages are "type-free" to one extent or another; that is, they treat properties, propositions, classes, functions, and other so-called "higher-order" entities as "first-class citizens" in their own right, capable of being referred to and quantified over along with individuals. Natural language itself reflects this "dual role" that properties and their ilk can play in the gerundive construction, whereby verb phrases expressing properties and relations — e.g., is a linguist — are transformed into noun phrases — being a linguist. By allowing predicate constants and function sybols simultaneously to serve as individual constants, and by allowing variables to serve as predicable terms, SCL provides a formal correlate to these constructions and thereby provides a rigorous framework in which this common knowledge representation construction is fully sanctioned.
It is useful explicitly to pick out several important limiting cases of SCL languages that are determined by minimally or maximally tweaking arity and the degree of overlapamong constants and function symbols. Specifically, say that an SCL lexicon λ is fully typed if (PredCon ∪ FnSym) ∩ IndCon = ∅; arity-fixed if, for all predicate constants and function symbols κ, arity(κ) = n, for some n ∈ N; and traditional first-order (TFO) if λ is both fully-typed and arity-fixed. By contrast, say that λ is arity-free if, for all predicate constants and function symbols κ, arity(κ) = ω; type-free if PredCon ∪ FnSym ⊆ IndCon; and unconstrained if λ is both arity-free and type-free. In between the extremes of TFO and unconstrained lexicons, of course, lie a number of interesting intermediate possibilities.
Given an SCL lexicon λ, we define the notion of a term class based on λ. Intuitively, a term is either a primitive term (constant or variable) or the result of "applying" a function symbol to some nonempty sequence of terms. Because we are defining an abstract syntax, we do not want to specify the exact form that the application of a function symbol to its arguments should take. Hence, we simply specify the general constraints than any syntax of application must satisfy; we do this in terms of a certain type of syntactic function.
As groundwork for this definition, for any set M, let M^{ω} be the set of finite sequences of elements of M, i.e., M^{ω} = ∪_{n∈N}M^{n}, where M^{n} is the set of all n-tuples of elements of M. Given this, say that T is a term class for λ if T contains all of the primitive terms of λ and is the smallest class^{1} closed under a one-to-one operation App — called a term generator for λ — such that
App : ∪_{n∈N}{FnSym_{n} × T^{n}} ∪ (FnSym_{ω} × (T^{ω} ∪ (T^{ω} × SeqVar))) → T.
That is, for τ_{1},…,τ_{n} ∈ T, if α is an n-place function symbol, then App(α,τ_{1},…,τ_{n}) ∈ T, and if α is a variably polyadic functional, then in addition for any sequence variable σ, App(α,τ_{1},…,τ_{n},σ) ∈ T;
We say that App generates the corresponding term class T. For any term generator App for λ, let FnTrm = Range(App),^{2} . FnTrm is the set of function terms of λ (relative to App).
So, for example, if a and b were among the constants of a lexicon λ and f and g among its function symbols, then any of the following might among the function terms produced by different generators: f(a,g(b),s), (f a (g b) s), s[bg]af (somewhat perversely), and even
<term> <fnsym>f</fnsym> <indcon>a</indcon> <term> <fnsym>g</fnsym> <indcon>b</indcon> </term> <seqvar>s</seqvar> </term>
This example illustrates the use of a sequence variable — note that such variables can only occur in a single distinguished position (typically, "tail" position) in a function term.
As hinted at above, and as will be spelled out in more detail in the model theory below, one of the important features of SCL is that it allows for a "type-free" semantics in which properties and relations are treated as first-class individuals. Languages with such a semantics will there be allowed to refer to and quantify over such "reified" entities directly. In particular, it is important to allow such languages to quantify over them in their predicative roles. Syntactically speaking, this means that we must allow variables to occur in predicate position in atomic formulas.
However, because it is important that SCL encompass more traditional first-order languages as well, type-freedom should be optional. Accordingly, whether or not variables (and other expressions, more generally) can occur in predicative position along with predicate constants will be specified in the grammar for a language, rather than being predetermined by the chosen lexicon. Consequently, we define the set Pred_{n} of n-place predicables to be either simply the set PredCon_{n} ∪ Pred_{ω} (since variably polyadic predicates be predicated of any finite number of arguments — hence, in particular of n) or the set PredCon_{n} ∪ Pred_{ω} ∪ GenVar. A similar generalization that allows variables to occur in function position in complex terms adds a certain elegance and convenience at the cost of a great deal of semantic complexity, but the gains are minimal for the purposes envisioned for SCL.^{0}.
In light of the above, we now do for formulas what we did for terms. Let λ be an SCL lexicon, and let Trm be the term class for λ generated by some term generator App. First, we need a class of basic formulas. Let Holds be a one-to-one function on
∪_{n∈N}{Pred_{n} × T^{n}} ∪ (Pred_{ω} × (T^{ω} ∪ (T^{ω} × SeqVar))).
That is, given an n-place predicable and n terms, or a variably polyadic predicable, n terms and a sequence variable, Holds returns a unique formula. Any such function Holds is said to be a predication operation for λ based on App. As with term generators, the outputs of different predication functions might take very different forms. The only constraint is that distinct inputs always yield distinct outputs.^{3} Given a term generator, the range of a predication operation Holds for λ is said to be the class of atomic formulas for λ generated by Holds.
Let At be the class of atomic formulas for λ based on a predication operator Holds. Say that F is a formula class for λ, relative to Holds, if it is the smallest class that includes At and is closed under a set Op — known as a formula generator for λ based on Holds — of operations Id, Neg, Conj, Disj, Cond, Bicond, ExQuant, UnivQuant that satisfy the following conditions:
Let Fla be range of the operations in Op. We say that Fla is the formula class generated by Op.
As with terms, depending on one's choice of term generator, predication operation, and generator set, SCL languages can come in many different concrete forms. So, for example, the standard, first-order "logical form" of 'Every boy kissed a girl' in terms of our abstract syntax is
UnivQuant(ν_{1},Cond(Holds(π_{1},ν_{1}),ExQuant(ν_{2},Conj(Holds(π_{2},ν_{2}),Holds(π_{3},ν_{1}, ν_{2}))))),
where π_{1}, π_{2}, and π_{3}, are "slots" for the predicates constants of the appropriate arity chosen from any particular lexicon to represent boyhood, girlhood, and kissing, and ν_{1} and ν_{2} represent some choice of variables. In one SCL language, this form might be realized by its familiar introductory text-book form:
(∀x)(Boy(x) → (∃y)(Girl(y) & Kissed(x,y)))
A conceptual graph interchange form (CGIF) implementation has a rather different appearance:
[@every*x] [If: (Boy ?x) [Then: [*y] (Girl ?y) (Kissed ?x ?y) ]]
As does a KIF-like implementation:
(forall (?x ?y) (implies (Boy ?x)) (exists (?y) (and (Girl ?y) (Kissed ?x ?y))))
Note also that the clauses for quantified formulas above, i.e., those entities in the ranges of ExQuant and UnivQuant, allow for the use of restricted quantifiers. Thus, the logical form of "Every boy kissed a girl" using such quantifiers, implementated in our standard textbook form might be:
(∀x:Boy)(∃y:Girl)Kissed(x,y)
An in CGIF and KIF-like implementations:
[Boy: @every*x] [Girl: *y] (Kissed ?x ?y)
(forall ((?x Boy)) (exists ((?y Girl)) (Kissed ?x ?y)))
The advantages of restricted quantifiers for readability are apparent.
It is important to observe that, because the operations in a generator set for a formula class Fla for λ are all one-to-one and disjoint in their ranges, every element of Fla will have exactly one "decomposition" under the inverses of those operations, and that all such decompositions are finite. ^{4} Let φ ∈ Fla. An object ε in the decomposition of φ is an atom of φ just in case ε is element of the lexicon λ. ψ is a subformula of φ if ψ ∈ Fla and ψ is in the decomposition of φ.
Hand in glove with the capacity to treat predicates as individual constants, as noted, is the ability of suitably defined SCL languages to have quantified variables occur in predicate position. The motivation is clear: since properties and relations can be treated as individuals, it should be possible to talk about them in general. This, of course, we can do in a basic way simply in virtue of their occurring as individuals in the domain of quantification. However, what we want to say about them might concern their predicative roles. Hence, we want to allow the variables that range over them to be able to occur in predicate position in atomic formulas as well. Similar remarks apply to functions.
As a simple example, one can axiomatize the property of symmetry for 2-place relations generally in the obvious way:
(forall (?x ?y ?F) (implies (Symmetric ?F) (implies (?F ?x ?y) (?F ?y ?x))))
Let App be a term generator for λ, where Trm is the set generated by App, and let Holds be based upon App. Let Op be a formula generator for λ based on Holds, and let L be the formula class generated by Op. We define any such set L to be an SCL language for the SCL lexicon λ, and we say that λ underlies L. Trm is said to be the set of terms of L. If λ and λ′ are SCL lexicons with the same sets of constants and function symbols, and L and L′ are SCL languages for λ and λ′, respectively, then L and L′ are said to be equivalent. If λ is a first-order lexicon, then a language for λ is said to be a first-order SCL language, or an SCL
The CL project, of which SCL is a part, is an outgrowth of the KIF project. CL for the most part simply abstracts away from the particularities of KIF — its choice of basic syntactic elements, its use of parenthesis, its choice of keywords, etc. A full CL language will therefore be structurally identical to a KIF language, but might differ in its surface form. Not surprisingly, then, it is rather straightforward to demonstrate that any KIF language is also an SCL language. SCL abstracts from a somewhat simpler version of KIF known as SKIF (Hayes and Menzel, 2001). We will demonstrate that SKIF is an instance of an SCL language in this section.
For purposes here, we will take SKIF expressions to be strings. Let A be the usual set of alphanumeric characters together with the characters "-" and "_". Our first task is to specify a lexicon for a SKIF language. Although the syntax for SKIF is now based more generally upon unicode, for purposes here we can take the sets PredCon, IndCon, and FnSym of a SKIF lexicon to be a set of (finite) strings over A, minus the usual SKIF keywords (i.e., "forall", "exists", "not", etc.). GenVar consists of the result of prefixing "?" to all strings over A, and SeqVar the result of prefixing "@" to those same strings. Clearly, these sets meet the disjointness requirements on SCL lexicons. Relative to this lexicon, then, Var is the set GenVar ∪ SeqVar, PrimTrm is the set Con ∪ GenVar, and PredTrm is the set PredCon ∪ GenVar. arity for SKIF is the constant function ω (i.e., all predicate constants and function symbols are variably polyadic).
Consider now the set S of strings over the set A ∪ {"?", " ", "(", ")"} (" " being the space character). Define an operation App* on FnSym × (S* ∪ (S* × SeqVar)) such that App*(t, s_{1}, …, s_{n}) = ⌈(t s_{1} … s_{n})⌉. ("⌈" and "⌉" here are quasi-quotes, or "Quine corners".) Let Trm be the smallest set containing PrimTrm that is closed under App*, and let App be App* restricted to FnSym × (Trm* ∪ (Trm* × SeqVar)). It is easy to see that App is a generator for Trm and that Trm is the set of SKIF function terms that is determined by the given lexicon. Given Trm, we define the operation Holds on PredTrm × (Trm* ∪ (Trm* × SeqVar)) such that Holds*(π, τ_{1}, …, τ_{n}) = ⌈(π τ_{1} … τ_{n})⌉. Let AtFla be the atomic formulas for our given lexicon, i.e., the range of Holds.
Consider now the following operations:
Let F be the smallest set containing AtFla that is closed under these operations. F is exactly the set of formulas of the SKIF language determined by the given lexicon, i.e., the above operations, restricted to F, jointly constitute a generator set for F.
XML provides another important framework for defining SCL languages. The following simple Document Type Definition (DTD) provides a convenient XML expression of an SCL language relative to some an unspecified lexicon that includes sequence variables. For simplicity's sake, we also assume that the lexicon is fully-typed and arity-free. The DTD's URI is http://cl.tamu.edu/docs/scl/scl-latest. dtd. This DTD validates the XML rendering of "Every boy kissed a girl" above.
<!ELEMENT formula (and | or | implies | iff | not | forall | exists | atom)> <!ELEMENT and (formula*)> <!ELEMENT or (formula*)> <!ELEMENT implies (formula, formula)> <!ELEMENT iff (formula, formula)> <!ELEMENT not (formula)> <!ELEMENT forall (varlist, formula)> <!ELEMENT exists (varlist, formula)> <!ELEMENT varlist (genvar | sortvar)+> <!ELEMENT sortvar (genvar, predcon)> <!ELEMENT atom (pred, (indcon | genvar | fnterm)*, seqvar{0,1})> <!ELEMENT fnterm (fnsym, (indcon | genvar | fnterm)*, seqvar{0,1})> <!ELEMENT pred (predcon | genvar) (#PCDATA)> <!ELEMENT indcon (#PCDATA)> <!ELEMENT predcon (#PCDATA)> <!ELEMENT fnsym (#PCDATA)> <!ELEMENT genvar (#PCDATA)> <!ELEMENT seqvar (#PCDATA)>
Let λ be an SCL lexicon. An SCL interpretation I for λ is a 4-tuple 〈I,R,ext,V〉 satisfying the following conditions. First, I and R are nonempty sets. Intuitively, I represents the set of individuals of I, and will serve as the range of the quantifiers and its members will serve as the denotations of terms. R is the set of relations^{5} whose members are the denotations of predicate constants. To allow for type-freedom, there is no requirement that I and R be disjoint; indeed any degree of overlap, from partial to complete, is allowed. Those relations that are also members of I are said to be reified. Intuitively, reified relations are relations that can also be thought of as individuals. Accordingly, they can also be the values of individual constants and individual variables.
R is itself the union of countable sets R_{ω}, R_{1}, R_{2}, R_{3}, …. All are possibly empty with the exception of R_{2}, which contains a distinguished element Id, intended to serve as the identity relation. Intuitively, R_{ω} is the set of variably polyadic relations, and each R_{n} the set of n-place relations. Accordingly, ext is a corresponding extension function from R into ℘(I^{ω}) subject to the constraint that, for any natural number n > 0, if r ∈ R_{n}, then ext(r) ⊆ I^{n}; in particular, ext(Id) = {〈a,a〉 : a ∈ I}.
Intuitively, of course ext(r) represents the extension of r. For elements r of R_{ω }, if ext(r) is a total (extensional) function on I^{ω},^{6} then we say that r is a function on I^{ω}. For n+1-place relations, r, if ext(r) is a total (extensional) function on I^{n},^{6} then we also say that r is a function on I^{n}, or an n-place function.
Finally, V is a "denotation" function that assigns appropriate values to the constants and function symbols of L. Specifically,
Note, importantly, that it is not required that I and R be disjoint. This is the semantic correlate of the type-freedom permitted (though not required) in SCL languages. Specifically, an SCL language L can allow a primitive term κ to do double duty as both a predicate constant and an individual constant. Consequently, the denotation function V in any interpretation I of L must by definition map κ, qua predicate constant, to an element of R; it must also map κ, qua individual constant, qua individual constant, to an element of I. Consequently, to satisfy these constraints, I, V(κ) will have to be in both I and R, i.e., it will have to be both a relation and an individual. And this is just what the semantics allows. In a similar fashion, predicate constants can do double duty as function symbols.
Given the notion of an interpretation for a lexicon λ, we can now define what it is for a formula of an SCL language L based on λ to be true in an interpretation.
Some additional apparatus will be useful in defining truth for quantified formulas (i.e., formulas in the range of ExQuant and UnivQuant). First, given an interpretation I, define a variable assignment for I to be a function that maps individual variables into I and sequence variables into I^{ω}. To define the semantics of quantification, what we need is the notion of a variable assignment v′ that is exactly like a given assignment v except that it might not agree with v on what to assign to some finite set of individual variables. The idea is straightforward, but the presence of restricted quantifiers forces us to proceed with some care. Let I = 〈I, R, ext, V〉 be an interpretation for L, and let v be a variable assignment for I. In our syntax, a quantifier can bind an entire sequence consisting of (individual) variables and variable/predicate pairs. So let χ_{1}, …, χ_{n} be such a sequence, and say that a variable assignment v′ for I is a [χ_{1},…,χ_{n}]-variant of v iff
So let L be an SCL language for a lexicon λ, where App generates the set Trm of terms of L, and let I = 〈I,R,ext,V〉 be an interpretation for L. Given I and a variable assignment v, let V_{v} be the union of V and v. Given I and a variable assignment v, the denotations of the function terms of L in I are completely determined by V_{v}. This can be expressed in terms of a unique extension V_{v}^{#} of V such that, for any term τ ∈ Trm:
Given V, we define satisfaction for the formulas of L by a variable assignment v for our interpretation I as follows. Let φ ∈ L:
Finally, then, a formula φ is true in I iff every variable assignment for I satisfies φ.
Note that, on this semantics, free individual variables are implicitly universally quantified; that is, if φ is a formula containing a free individual variable ν, then φ is true in I iff UnivQuant(ν,φ) is true in I. We do not have a similar metatheorem for formulas with free sequence variables because sequence variables are not explicitly quantified. It should be clear, however, that the above definition of truth treats free sequence variables as if they were universally quantified as well: a formula φ containing a free sequence variable σ will be true in an interpretation I iff every variable assignment v satisfies φ, and hence iff every [σ]-variant of every variable assignment satisfies φ.
It is convenient for many applications to introduce truth functional constants denoting truth and falsity. Given the syntax and semantics for SCL above, these notions can be introduced simply as definitions. Specifically, the syntax generates both the empty conjunction Conj(∅) and the empty disjunction Disj(∅) for any given generator set. (In KIF, for example, these would correspond to the formulas '(and)' and '(or)', respectively.) On the semantics for these operators, Conj(∅) is true in all interpretations and Disj(∅) is false in all interpretations. Hence, in any given SCL language, constants for truth and falsity can be introduced and defined axiomatically to be equivalent to these formulas. Thus, for example, in KIF, one might add the constants 'true' and 'false' and the axioms '(iff true (and))' and '(iff false (or))'.
SCL is rather less constrained than traditional logical logical languages and it is expressively quite powerful. In many contexts, especially the constructions of ontologies, a language is used that is more structured, less expressive, or both — as is the case with most familiar first-order languages. If conformance with SCL required adoption of all of its features, it is unlikely that it would see wide adoption. Hence, conformance comes in two varieties: direct, for languages that fully embrace both SCL's unconstrained syntax and its semantic expressiveness, and indirect, for more languages that are more constrained syntactically, semantically, or both.
A given language is directly conformant with the SCL standard just in case it is an instance of an SCL language. Hence, as just illustrated, to demonstrate that a language L* is directly conformant, one must simply:
As indicated, more constrained languages can still be thought of as CL conformant in a robust, well-defined sense. Specifically, where L is a CL language, we define a subset L′ ⊆ L to be indirectly conformant relative to L just in case L′ is recursive. Hence, in general, to show that a given language L′ (simply a set of formulas, recall) is indirectly conformant, one must simply provide a recursive specification of L′ relative to some CL language L. Typically, of course, a specification of an indirectly conformant language will be provided independent of any specific CL language.
A language will be said to be SCL conformant (conformant, for short) just in case it is either a SCL language or indirectly conformant relative to some SCL language.
It is easy to demonstrate that the presence of sequence variables pushes SCL beyond the power of first-order logic. For example, let 's' be a sequence variable and 'P' a variably polyadic predicate constant; then every finite subset of the the following set is satisfiable, but the set itself is not:
{(∃s)~Ps, P, (∀x_{1})Px_{1}, (∀x_{1}x_{2})Px_{1}x_{2}, …}
Hence, the compactness property fails for full SCL. However, despite its nontraditional extended features --- notably, the ability to quantify over so-called "higher-order" objects like properties and relations, SCL without sequence variables — call this "SCL_{1}" — is fully first-order. Notably, it is easy to prove that SCL_{1} has both the compactness property and the downward Löwenheim-Skolem property, the two defining properties of first-order logic, by Lindstrom's famous theorem [REF]. Nonetheless, other features permitted in SCL_{1} languages — variables occurring in predicate position in atomic formulas and in function position in complex terms, predicates and function symbols serving simultaneous as arguments to other predicates and function symbols — lead to logical forms that are unfamiliar in traditional first-order (TFO) languages. It is important, therefore, to explore the connections between SCL_{1} and TFO languages.
We first note that TFO languages can be defined in a way that shows them to be indirectly SCL conformant. Specifically, let L be an SCL language for some lexicon λ such that
L_{1} is clearly indirectly conformant.
It is straightforward to circumscribe a subclass of SCL interpretations for the lexicon λ, and a corresponding notion of truth — viz., "truth_{1}" — for TFO languages based on λ, relative to which validity is coextensive with more traditional first-order model theory. Let L be an SCL_{1} language based on λ and L_{1} be the traditional first-order sublanguage of L determined by an arity function arity for λ. An interpretation I = 〈I,R, ext, V〉 for λ is TFO-agreeable relative to arity just in case the following conditions hold (henceforth reference to arity will be suppressed when it can be determined from the context):
Let L_{1} be a TFO sublanguage of L determined by arity, and let I = 〈I,R,ext,V〉 be TFO-agreeable interpretation of λ. The definition of what it is for a formula φ of L_{1} to be true_{1} in I is identical to the definition of truth in I except for the quantificational clauses, which have to be restricted to TFO-agreeable interpretations; specifically:
φ is valid_{1} iff it is true_{1} in all TFO-agreeable interpretations of λ.
It is utterly trivial to transform a TFO-agreeable interpretation I into a structurally similar, more traditional "Tarskian" first-order interpretation I* of L_{1} (call this the Tarski correlate of I). We simply replace V and ext with their composition V • ext, thereby mapping individual constants to elements of I and predicate constants and function symbols directly to extensions. More exactly, where I = 〈I,R, ext, V〉 is an L_{1}-agreeable interpretation, let I* = 〈I,V*〉, where V*(κ) = V(κ) for individual constants κ and V*(β) = ext(V)(β), for predicate constants and function symbols β. It is easy to see that a formula is true_{1} in a TFO-agreeable interpretation I iff it is true in its Tarski correlate.
It is nearly as trivial to transform a Tarskian interpretation I* = 〈I,V*〉 of L_{1} into a structurally similar L_{1}-agreeable interpretation I = 〈I,R, ext, V〉, where:
Once again, it is obvious that a sentence of L_{1} is true in a Tarskian interpretation I* iff it is true in its L_{1}-agreeable counterpart. Hence, the valid_{1} formulas of L_{1} are exactly the traditional first-order validities of L_{1}. That is to say, the logical properties of a TFO language are identical regardless of whether one interprets the language according to SCL's model theory for TFO languages or traditional Tarskian model theory.
As noted, SCL_{1} languages — SCL languages without sequence variables — are fully first-order. The easiest way to demonstrate this is to define a simple translation scheme from an arbitrary SCL_{1} language and a TFO language. Note that this scheme has not only theoretical value, but also suggests a general approach for making use of existing first-order automated reasoning engines that are not tuned to SCL's freer syntax.
So L be an arbitrary SCL_{1} language based on a given lexicon λ. We let PredCon, IndCon, FnSym, and GenVar be the stock of primitive lexical items of λ. We begin by defining the notion of a fully typed correlate λ* of λ. The idea here, first, is to purge λ of its type-free elements, viz., those predicate constants and function symbols that double as individual constants. To accomplish this, we first separate off the "pure" predicates of λ, those that are not also individual constants. So let PurePred = PredCon – IndCon.
We next lay the groundwork for adding an arity function. Thus, for each element π of PurePred we stipulate there is a unique predicate π_{n}, and we let PurePred* be the set {π_{n} : π ∈ PurePred, n > 0}. Next, let Holds be a set of countable many new predicates 'Holds_{1}', 'Holds_{2}', ….
We need a similar treatment for functions symbols. We first purge the type-free elements. So let PureFn = FnSym – IndCon. Next, for each element α of PureFn we stipulate there is a new function symbol α_{n}, for all n, and we let PureFn_{TFO} be the set {α_{n} : α ∈ PureFn, n > 0}. Next, let App be a set of countably many new function symbols 'App_{1}', 'App_{2}', ….
Given this, we define λ* as follows:
λ* now determines a class of equivalent SCL_{1} languages. Let L* be one of these languages. Let App, Holds, Id, … be L's term generator, predication operator, and formula generator, and let App*, Holds*, Id*, … be those of L*. Since PredCon*, IndCon*, and FnSym* are pairwise disjoint, L* serves as the basis for a TFO language; all we need is an arity function. It is clear enough what we want. for every pure predicate π of L, and every n > 0, we let arity(π_{n}) = arity(⌈Holds_{n}⌉) = n. Similarly, for every pure function symbol α of L, and every n > 0, we let arity(α_{n}) = arity(⌈App_{n}⌉) = n. Call this the natural arity function for λ*. Let L*_{1} be the TFO sublanguage of L* based on arity.
Our translation scheme from L into L*_{1} runs as follows. First, for terms τ of L:
Now let φ ∈ L:
Recall that the general form of quantified formulas allows for restricted quantifiers; in the existentially quantified case, ExQuant(χ_{1},…,χ_{n},ψ), where the χ_{i} are either single individual variables or pairs of the form 〈ν,κ〉, where ν is an individual variable and κ is a predicate. In the latter case we need to distinguish between the cases where κ is a predicate only (i.e., where κ ∈ PurePred) and those where κ is also an individual constant. Thus, for a sequence χ_{1},…,χ_{n} of the relevant sort, let ξ_{1},…,ξ_{i} be those members of the sequence, in order, that are either single individual variables or pairs 〈ν,κ〉 where κ ∈ PurePred. In the latter case, let 〈ν,κ〉* be 〈ν,κ_{1}〉 (κ_{1}, recall, being the 1-place predicate of λ* corresponding to κ). The remaining elements of the sequence are thus all variable / predicate constant pairs 〈ν^{1},κ^{1}〉, …, 〈ν^{j},κ^{j}〉. Our translation continues as follows:
To illustrate, consider a KIF-like language L containing an individual constants 'a' and 'b', function symbols 'f' and 'g', , and predicates 'foo', 'bar', and 'baz'. Suppose also 'f' and 'foo' have also been designated individual constants. We suppose 'f_{1}', 'f_{2}', … are the n-place function symbols corresponding to 'f' in λ*; similarly for 'foo'. We suppose the grammar of L* be similar in form to L to simplify the example. Then the following would be example translations according to the above scheme:
(g a (f a b))* = (g_{2} a (App_{2} f a b)) (foo (g a) b (g f (f a)))* = (Holds_{3} foo (g_{1} a) b (g_{2} f (App_{1} f a))) (forall (?x (?y foo) (?u foo)) (exists (?z (?w bar)) (and (baz ?x (f (g ?y))) (not (foo ?x ?z (g (f ?x ?w)))))))* = (forall (?x) (implies (and (Holds_{1} foo ?y) (Holds_{1} foo ?u)) (exists (?z (?w bar_{1})) (and (baz_{2} ?x (App_{1} f (g_{1} ?y))) (not (Holds_{3} foo ?x ?z (g_{1} (App_{2} f ?x ?w))))))))
[SOMETHING'S MISSING HERE…] intuitively meaning preserving. This intuition can be expressed precisely in our model theory. This is primarily a matter of defining a method for transforming any interpretation of the lexicon λ on which our SCL_{1} language L is based into an "equivalent" TFO-agreeable interpretation of λ's fully typed correlate λ*.
The method is quite obvious. Recall again that λ* is defined as follows:
Recall also that we have an arity function for the predicates and function symbols of λ*. So let I = 〈I,R, ext, V〉 be an interpretation for L. Define I* = 〈I^{ω},R*,ext*, V*〉 as follows. For each π_{n} ∈ PurePred*, 'Holds_{n}' ∈ Holds, α_{n} ∈ PureFn*, 'App_{n}' ∈ App, let p_{n}, holds_{n}, f_{n}, and app_{n} be new objects not already in I ∪ R. Let P, H, A, and F be the sets of all of these new objects, respectively.
It is straightforward to show that I* is a TFO-agreeable interpretation of λ*. Call any such I* a TFO-agreeable correlate of I. The following is an easy induction on the complexity of formulas:
Theorem: Let L be an SCL_{1} language based on a lexicon λ, let L* be a language based on a fully typed correlate λ* of λ, and L*_{1} the TFO sublanguage of L* based on the natural arity function arity for λ*. Then a sentence φ of L is true in an interpretation I iff its translation φ* into L*_{1} is true_{1} in any TFO-agreeable correlate I* of I.
0.
The complexity arises from the fact that, to keep the semantics
classical, one must introduce a mechanism that guarantees that
every term, no matter what it's semantic value, can be applied
to arguments in such a way as to "return" a unique value. Such
a semantics is worked out in the full
1. T is the smallest such class just in case it satisfies the conditions in question but is not a proper superclass of any other class satisfying those conditions.
2. Where Range(App) = {τ ∈ Trm : for some x, App(x) = τ}.
3. Practically, speaking, of course, Holds should be computable and reversible; that is, given any inputs, we should be able to compute Holds's output, and given any of its outputs, we should be able to compute the arguments that yielded that output.
4. Suppose φ ∈ Fla has an infinite decomposition. Then Fla – {φ} still satisfies the conditions above, as closure under the operations in the generator set only requires finite compositions of those operations applied to the base sets. But then Fla is not a smallest class of the relevant sort, contrary to its definition. This will be important for the semantics of SCL languages below.
5.It is possible to model of the members of R extensionally as sets, though this will in general require non-well-founded set theory, since a relation, qua individual, can be in its own extension.
6. An extensional relation A on a set M is simply a subset of M^{ω}. A is variably polyadic if there are tuples of different lengths in A. A is an n-place extensional relation if every element of A is of length n. An extensional, variably polyadic relation A on a set M is a total (extensional) function on M^{ω} iff for any tuple 〈a_{1},…,a_{n}〉 ∈ M^{ω}, there is a unique b ∈ M such that 〈a_{1},…,a_{n},b〉 ∈ A. An (n+1)-place extensional relation A on a set M is a total (extensional) function on M^{n} iff for any n-tuple 〈a_{1},…,a_{n}〉 ∈ M^{n}, there is a unique b ∈ M such that 〈a_{1},…,a_{n},b〉 ∈ A.
7. These lexical items of L1 are thus being tapped to play a semantic role in our L1-agreeable interpretation. Any objects would do as the elements of R, of course, but using the lexical elements themselves simplifies the construction.
Boole, George (1854) An Investigation into the Laws of Thought, reprinted by Dover Publications, New York.
Frege, Gottlob (1879) Begriffsschrift, English translation in J. van Heijenoort, ed. (1967) From Frege to Gödel, Harvard University Press, Cambridge, MA, pp. 1-82.
Genesereth, Michael R., & Richard Fikes, eds. (1998) Knowledge Interchange Format (KIF), draft of a proposed American National Standard, NCITS.T2/98-004. Available at http://logic.stanford.edu/kif/dpans.html.
Guha, R. V., & Patrick Hayes (2003) LBase: Semantics for Languages of the Semantic Web, W3C Working Group Note 10 October 2003, available at http://www.w3.org/TR/lbase/
Hayes, Patrick, & Chris Menzel (2001) "A semantics for the knowledge interchange format," available at http:reliant.teknowledge.com/IJCAI01/HayesMenzel-SKIF-IJCAI2001.pdf.
Menzel, Chris, & Patrick Hayes (2003) "SCL: A Logic Standard for Semantic Integration," Semantic Integration Workshop, Sanibel Island.
Peano, Giuseppe (1889) Aritmetices principia nova methoda exposita, Bocca, Torino. Excerpt translated as Principles of mathematics presented by a new method in van Heijenoort (1967) pp.83-97.
Peirce, Charles Sanders (1880) "On the algebra of logic," American Journal of Mathematics 3, 15-57.
Peirce, Charles Sanders (1885) "On the algebra of logic," American Journal of Mathematics 7, 180-202.
Roberts, Don D. (1973) The Existential Graphs of Charles S. Peirce, Mouton, The Hague.
Sowa, John F. (1984) Conceptual Structures: Information Processing in Mind and Machine, Addison-Wesley, Reading, MA.
Sowa, John F. (2000) Knowledge Representation: Logical, Philosophical, and Computational Foundations, Brooks/Cole Publishing Co., Pacific Grove, CA.
Sowa, John F. (2001) Conceptual Graphs, draft of a proposed IS standard. Available at http://www.jfsowa.com/cg/cgstand.htm.
Tarski, Alfred (1933) "Pojecie prawdy w jezykach nauk dedukcynych," German trans. as "Der Wahrheitsbegriff in den formalisierten Sprachen," English trans. as "The concept of truth in formalized languages," in Tarski (1982) pp. 152-278.
Tarski, Alfred (1936) "Über den Begriff der logischen Folgerung," translated as "On the concept of logical consequence" in Tarski (1982) pp. 409-420.
Tarski, Alfred (1944)
Tarski, Alfred (1982) Logic, Semantics, Metamathematics, Second edition, Hackett Publishing Co., Indianapolis.