SUO: Re: CG: Re: Ontology
Jean-Luc,
There was no "ontology war". Jay was merely repeating
the same old BS he was taught in school, and I was
pointing out that the people who know better know better.
In any case, I have been busy working on writing the
specifications for CLCE (Common Logic Controlled English).
See the abstract below and the pointer to the (still
unfinished) report.
Re "What is mathematics": That's a fairly decent
summary of math. Nothing controversial.
John
________________________________________________________
Source: http://www.jfsowa.com/logic/clce.htm
Common Logic Controlled English
Incomplete Draft, 31 January 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, parentheses to delimit lists, single
quotes to delimit names that contain nonalphabetic characters, 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, well-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, 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.
Since CLCE has the full expressive power of first-order logic, it is
possible to translate any FOL statement in predicate calculus, CGIF, or
many other notations into CLCE. The 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 statement.
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.