Adrian, (01)
I'm still not exactly clear about what you are advocating.
I believe that there is a considerable overlap in our
positions, but the layers you mention aren't clear. (02)
Also, please don't make assumptions about what I advocate.
If you have a question, I'd be happy to answer. But please
don't make claims about my position. I'd rather explain my
own position than have anyone else try to do it for me. (03)
> Unfortunately, classical logic assigns a meaning to negation
> that differs from the way databases are actually used. (04)
That is true. There are four widely used options: (05)
1. The closed-world assumption (CWA) in which any ground clause
(n-tuple of constants) not asserted to be true is assumed
to be false. This is typical of airline reservations: if
your reservation is not in the DB, you don't have one. (06)
2. The open-world assumption (OWA) in which any ground clause
not asserted to be true has an unknown truth value. This
is typical of most databases generated from observations.
Anything not observed is not known to be true or false. (07)
3. Three-valued logic (TVL) in which some ground clauses are
asserted to be true, others are asserted to be false, and
any others have an unknown truth value. (08)
4. The whatever assumption (WA) in which anything not asserted
to be true may be false, unknown, or whatever. This is the
widely used method of code-and-debug until you get tired
or the deadline has passed. (09)
First observation: all four of these methods agree on those
ground clauses (n-tuples) that have been asserted to be true.
Therefore, programs or proofs that fetch data and draw
positive inferences without making any assumptions about
what's not present will work correctly under all four. (010)
Second, any notation for logic, any logic-related notation
such as SQL, Datalog, etc., and any natural language or
any controlled or executable variant, can be used to make
statements under all four of the above alternatives.
Different reasoning methods are necessary to avoid making
false or nonsensical statements in each of those methods,
and the methods for avoiding the problems are independent
of the notation. (011)
> Unfortunately, classical logic assigns a meaning to negation
> that differs from the way databases are actually used. (012)
Classical negation corresponds to the CWA. That is one of
the ways that databases are used. (013)
> I believe that where you and I agree is that it's crucial to have
> an executable English layer between end author-users and the logic.
> Such a layer captures the intention of an author, so that a user
> can see what the intention is. Calling this a "semantic layer"
> would seem to be justifiable. (014)
I really am not sure what you mean. I can say what I mean:
The semantic layer I have in mind is the abstract syntax of
Common Logic, as defined in ISO/IEC 24707 -- or some subset or
superset thereof. The CL standard was designed in such a way
that no concrete notation is privileged over any other. The
three annexes of the standard define three concrete syntaxes
(CLIF, CGIF, and XCL), but the standard also specifies how
anybody who wishes to define some other concrete syntax as
a dialect of CL can do so. (015)
If you wish to define executable English as a dialect of CL or
some subset of CL, by all means do so. The standard encourages
you and others who have defined logical notations to map them
to the CL abstract syntax. That mapping automatically gives
them a formal model theory. For specific examples of how to
do the definitions, look at the three annexes -- each of which
maps a very different kind of dialect to the same abstract syntax.
Download a copy of the ISO standard and do it. (016)
> Your point about avoiding lock-in by supporting a broad version
> of logic is well taken, so long as the model theoretic semantics
> is a relevant one. (017)
Relevant to what? The CL model theory is a superset of the one
used by Datalog or SQL with the closed-world assumption. So it
is definitely relevant to that one. (018)
Furthermore, every proof that uses negation as failure (NAF) can
be converted to a proof that conforms to the CL model theory. (019)
1. Start with a set of formal axioms A stated in any CL dialect,
a set of ground-level clauses C, and a goal G (e.g. an SQL
query or Prolog goal). (020)
2. Carry out a proof of the G using NAF, and make a note of
every application of NAF to assume not-p if some n-tuple p
is not in the database. (021)
3. Then the resulting proof is *identical* to a classical proof
of G from the set consisting of the axioms A, the ground
clauses C, and the set of negated clauses p1,...,pN that
correspond to each use of NAF. (022)
This illustrates how the CL model theory is relevant to the
use of negation as failure, if you choose to use the open-world
assumption. (023)
It is possible to define an extension of this approach to show
how the CL model theory can be used in a way that is relevant
to three-valued logic. (024)
So I claim that CL model theory can be used and interpreted in
ways that are relevant to the CWA, OWA, and TVL assumptions. (025)
I won't bother with the whatever assumption. (026)
John (027)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (028)
|