SUO: Common Logic Controlled English (CLCE)
Folks,
I have been writing a program for translating
a subset of English to CGIF, which I plan to
release under the GPL license. I'll also include
the option of generating predicate calculus or
a KIF-like version of the proposed standard for
Common Logic. I expect to have it finished this
spring, and I'll discuss the issues involved at
the ICCS conference in July. Following is a draft
of the CLCE specifications and grammar:
http://www.jfsowa.com/logic/clce.htm
Common Logic Controlled English
I'd like to solicit any comments, suggestions,
or complaints.
For those who don't want to take the trouble to
click on the above URL, I'm including the abstract
and an excerpt from each of the 9 sections below.
John Sowa
____________________________________________________________
COMMON LOGIC CONTROLLED ENGLISH
Draft, 6 February 2004
John F. Sowa
Abstract: Common Logic Controlled English (CLCE) is a formal language
with an English-like syntax. Anyone who can read ordinary English
can read sentences in CLCE with little or no training. Writing CLCE,
however, requires practice in learning to stay within its syntactic and
semantic limitations. Formally, CLCE supports full first-order logic
with equality supplemented with an ontology for sets, sequences, and
integers. The fundamental semantic limitation of CLCE is that the
meaning of every CLCE sentence is defined by its translation to FOL;
none of the flexibility of ordinary English and none of its metaphorical
or metonymic extensions are supported. The primary syntactic
restrictions are the use of present tense verbs and singular nouns,
variables instead of pronouns, and only a small subset of the many
syntactic options permitted in English. Despite these limitations,
CLCE can express the kind of English used in software specifications,
textbooks of mathematics, and the definitions and axioms of formal
ontology.
1 OVERVIEW
The design goal for Common Logic Controlled English (CLCE) is to stay as
close as possible to precise, carefully written English while supporting
automated translation to first-order logic (FOL). The syntax of CLCE
is similar to the kind of English used in software documentation and
textbooks of mathematics. Anyone who can read English can read CLCE
without special training. The hardest part of learning to write CLCE is
staying within the semantic restrictions of FOL. Those restrictions are
familiar to anyone who has used languages for database query, software
design, or formal specification, such as SQL, UML, OWL, Express, and Z.
Since those languages can be automatically translated to and from FOL,
they can also be translated to and from CLCE. Therefore, CLCE can be
used as a readable documentation language that can be compiled to
an implementation language. In that regard, CLCE is similar to other
controlled languages such as Attempto Controlled English (Fuchs et al.
1998), which is compiled to Prolog.
Despite its generality, CLCE is not intended to be an official standard;
the standard is first-order logic, and CLCE is just a convenient
notation for making FOL easier to read and write. Since CLCE has the
full expressive power of FOL, it is possible to translate any FOL
statement in predicate calculus, CGIF, or many other notations into
CLCE. The reverse translation from FOL to CLCE can be automated, but
with certain qualifications:
1. If the FOL statement had originally been generated from CLCE, then
the declarations of names and other words used to translate CLCE
to FOL could also be used to translate the FOL back to CLCE.
2. If the FOL statement had not be derived from CLCE, the translation
into CLCE could only be done if the mappings of the symbols used
in FOL to the words used in CLCE were specified by the same kind
of information given in CLCE declarations.
3. Since both CLCE and FOL provide many alternative ways of stating
the same proposition, the reverse translation might not be identical
to the original CLCE statement, but it should be logically
equivalent.
4. Conceptual graphs (CGs) have been designed to support a direct
translation to and from natural languages. Therefore, the reverse
translation from CGs to CLCE tends to be closer to the original
CLCE form than the translations from other versions of FOL.
5. As examples of reverse translations, consider the following three
CLCE sentences, which are logically equivalent:
Every prime number less than 3 is even.
For every number x, if x is prime, and x is less than 3,
then x is even.
For every x, if x is a number, x is prime, and x is less than 3,
then x is even.
If the first sentence were translated to CGs, the reverse
translation would produce the original. The second sentence
would result from translating the first to typed predicate calculus
and back to CLCE. The third sentence would result from translating
to untyped predicate calculus and back to CLCE.
6. The proof that the reverse translation is equivalent to the original
can always be done efficiently. In fact, the number of interchanges
and substitutions required for the proof is linearly proportional
to the length of the CLCE sentence.
The ability to do translations in both directions enables CLCE to be
used as a documentation language that is always synchronized with
the implementation: any changes to either the documentation or the
implementation can always be translated to the other. Errors and typos
that may be hard to detect in unfamiliar notations are often easier to
see in CLCE, and they can be found even by people who have never studied
CLCE....
2 RELATING CLCE TO OTHER REPRESENTATIONS
CLCE is not intended to be a standardized language. FOL is the
standard, and CLCE is a highly readable supplement to FOL and related
languages, such as SQL and UML. Similar techniques can be used to
design other controlled languages, such as CLCF, CLCG, or CLCJ for
French, German, or Japanese. For all those languages, FOL is the common
semantic form, which can be translated to and from any syntax the user
may prefer. To see how CLCE can be used to relate natural languages to
logic, it is important to consider some examples. Figure 2 shows two
structures of blocks and pyramids and their representation in database
tables named Objects and Supports. The first step is to declare the
syntax of suitable CLCE words and relate them to the two database
tables. Then the two structures can be described by CLCE sentences
that can be automatically translated to logic, SQL, UML, or other
notations....
3 ELIMINATING AMBIGUITIES
Unlike English, for which background knowledge is required to resolve
many ambiguities, CLCE has a syntax that allows every ambiguity to be
resolved when a sentence is parsed. The declarations that are necessary
for translating CLCE to FOL can also be used at parse time in order to
select the correct sense for each word and generate the translation to
other notations....
4 SENTENCES
The sentences of CLCE resemble a subset of the sentences of ordinary
English. Like English sentences, each CLCE sentence has one or more
clauses, and each clause has one verb. A sentence can be classified in
two ways: according to its structure, a sentence may be simple,
complex, or compound; according to its use, a sentence may be
declarative, interrogative, or imperative....
5 WORDS
CLCE words are divided into a small number of reserved words and an
open-ended number of declared words. All reserved words are spelled
like English words, but their meanings are restricted to just one word
sense or to a small number of senses that can be distinguished by the
syntax....
6 SCOPE OF QUANTIFIERS
The problem of determining the referents of pronouns and other
referential noun phrases is intimately connected with the question of
the scope of quantifiers in first-order logic. As examples, consider
the following CLCE sentences...
Bob sees a car; the car is red.
Bob does not see a car; the car is red.
In the first line, the phrase, a car, is represented by an existential
quantifier, (?x:Car), in the sentence before the semicolon. In the
sentence after the semicolon, the referential noun phrase, the car,
which is represented by the variable x, is associated with the car that
is assumed to exist. But the car that Bob does not see is represented
by an existential quantifier within the scope of a negation. Therefore,
it is not possible to refer to the car after the semicolon because its
identity and even its existence are in doubt. That example illustrates
two fundamental principles:
1. If the only logical operators were the existential quantifier and
conjunction, any entity that was mentioned in a text could be
referenced at any point after its first introduction.
2. Any negation, explicit or implicit, blocks the assumption that an
entity introduced inside the context of the negation exists outside
that context.
These two principles are equally valid for FOL, CLCE, English, and every
other natural language. For CLCE, all the questions about scope are
determined by the interaction of these two principles with the explicit
or implicit negations in a CLCE text. The CLCE rules, which follow from
these principles, are a subset of the more complex rules of discourse
representation theory (Kamp & Reyle 1993) for unrestricted natural
language....
7 GRAMMAR
CLCE grammar rules are written in Extended Backus-Naur Form (EBNF),
as specifed by International Standard ISO/IEC 14977. Each EBNF rule
is preceded by an informal English paraphrase. In any question of
interpretation, the EBNF rule takes precedence over the English
statement. This section uses EBNF to define three kinds of grammar
rules for CLCE: lexical rules, which define the categories of words
that occur in CLCE sentences; syntactic rules, which define the
combinations of words in phrases and sentences; and declaration rules,
which define the statements that declare CLCE words and their mapping
to FOL or other notations....
8 GENERATING FOL FROM CLCE
Translation from CLCE to first-order logic in any notation is based on
the same general principles. The translation is somewhat simpler for
conceptual graphs, which have been designed to map to and from natural
languages as directly as possible, but the initial stages of generating
any other notation for FOL are the same. The only difference is that a
few extra steps are needed in the final stages for generating predicate
calculus and other notations....
9 BEYOND FIRST-ORDER LOGIC
First-order logic is sufficiently expressive to specify a Turing
machine, any digital computer, or any software that could be implemented
on a digital computer. It is also sufficiently expressive to specify a
Petri net or any system of times, events, and causal sequences that may
be modeled by a Petri net. A specification that is limited to nothing
but pure FOL, however, can become encrusted with so much detail that
no amount of "syntactic sugar" can make it understandable. For that
reason, many extensions beyond classical FOL are necessary to make such
specifications not only possible, but readable and understandable....