Hi Simon,
You wrote: With prolog, the biggest problem is that, by requiring all possible proof trees to be explored,...
Actually, Prolog finds one proof and pauses. The user can then ask it to backtrack for another (which may turn out to be an alternative proof for the same answer).
However the original Prolog engine is very old, and there are better engines these days for executing Prolog syntax, e.g. [1].
Cheers,  Adrian
[1] Backchain Iteration: Towards a Practical Inference Method that is Simple Enough to be Proved Terminating, Sound and Complete. Journal of Automated Reasoning, 11:122
Internet Business Logic A Wiki and SOA Endpoint for Executable Open Vocabulary English Q/A over SQL and RDF Online at www.reengineeringllc.com Shared use is free, and there are no advertisements
Adrian Walker Reengineering
[1]
On Sat, Mar 24, 2012 at 3:35 PM, Simon Spero <ses@xxxxxxx> wrote:
Sent from wrong address.
 Forwarded message  From: Simon Spero <sesuncedu@xxxxxxxxx>
Date: Fri, Mar 23, 2012 at 1:58 PM In the case of prolog, we're never in P to begin with...
With prolog, the biggest problem is that, by requiring all possible proof trees to be explored, any infinite search trees that might not be explored in a successful positive query will lead to nontermination in what should be a successful negative query.
Since Prolog is not complete anyway, this does not add a new problem :)
See the original semantics for NAF, available online at
http://www.doc.ic.ac.uk/~klc/neg.html
There are lots of issues of this kind in general nonmonotonic reasoning; fortunately there are also lots of special cases where reasoning is tractable see, for example, any objectoriented programming language that offers inheritance with overriding.
See also: Morgenstern, Leora (1998). Inheritance Comes of Age: Applying Nonmonotonic Techniques to Problems in Industry. Available at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.8316
Simon
On Mar 23, 2012 1:19 PM, "Adrian Walker" < adriandwalker@xxxxxxxxx> wrote:
Hi John,
Nice summary of the issues.
It seems that 1. takes us outside first order logic into second order. What are the computational complexity consequences? Moving from P to NP perhaps?
Cheers,  Adrian
Internet Business Logic A Wiki and SOA Endpoint for Executable Open Vocabulary English Q/A over SQL and RDF Online at www.reengineeringllc.com
Shared use is free, and there are no advertisements
Adrian Walker Reengineering
On Fri, Mar 23, 2012 at 11:59 AM, John F. Sowa <sowa@xxxxxxxxxxx> wrote:
The topic of nonmonotonic reasoning has come up in many threads on
this list. I'd like to make a few comments about it and cite some
references.
First, the term 'nonmonotonic reasoning' is broader than the term
'nonmonotonic logic'. It includes methods of belief revision (or
theory revision). Those methods keep the usual classical logic,
but they revise a classical theory by adding or deleting axioms
to create a new classical theory.
Second, the semantics of every version of nonmonotonic reasoning is
based on the semantics of a related classical logic. For example,
query languages like SQL and rulebased languages like Prolog use
a nonmonotonic logic called *negation as failure* (NAF). Proofs
in NAF systems can be defined in several ways:
1. As nonmonotonic logic, add a new rule of inference to the rules
for the corresponding classical logic: if an attempted proof
of a statement p fails, assume that p is false.
2. As belief revision, use the Closed World Assumption (CWA) to
revise the theory (axioms + facts) by adding the negation of
every statement that uses the same ontology, but is not provable.
Then you can use the classical rules of inference, but with a
much larger set of axioms.
3. Method #2 makes a huge revision to the axioms in one step.
But it's possible to achieve the same effect by incrementally
adding axioms one at a time as needed: whenever a NAF step is
used in a proof, add the new negated assumption to the set of
axioms for the current theory. As a result, the same proof can
be carried out from the enlarged set of axioms, but with just
classical inference rules.
Method #3 is an incremental method of belief revision that can use
exactly the same inference engine as the corresponding nonmonotonic
logic. The only difference is that it saves each negated statement
and adds it to the list of axioms. It shows that the difference
between nonmonotonic logic and belief revision can just be considered
a difference in terminology (at least for NAF logics).
For a general discussion of these issues, see the following book
on belief revision, which emphasizes the relationships among
nonmonotonic logics, classical logics, and belief revision:
Makinson, David (2005) Bridges from Classical to Nomonotonic Logic,
King's College Publications, London.
Makinson also happens to be the M in the AGM axioms for belief
revision. The following review of his book summarizes some of
the issues:
http://www.maths.manchester.ac.uk/~hykel/work/bridgesreview/
See the end of this note for a few excerpts from the review.
For related information, see the first page of Makinson's own
web site, which has comments about his other articles:
http://sites.google.com/site/davidcmakinson/
For a good review article with 110 references to the literature
on belief revision, see
Peppas, Pavlos (2008) Belief revision, in F. van Harmelen,
V. Lifschitz, & B. Porter, Handbook of Knowledge Representation,
Elsevier, Amsterdam, pp. 317359.
Note the last paragraph in the following excerpts from the review
of Makinson's book. The cases for which the "unwelcome assumption"
can be avoided can be found by walking through the lattice of all
possible theories that can be stated in the given classical logic.
John
_____________________________________________________________________
Source: http://www.maths.manchester.ac.uk/~hykel/work/bridgesreview/
The book [develops] the logicomathematical apparatus required to
construct nonmonotonic inference operations out of the classical,
monotonic one...
Its key message is that nonmonotonic logics, as in fact many other
socalled nonstandard logics, are not to be taken as alternatives to
the classical one, in the way, that is, in which intuitionistic logic is
regarded as opposed to classical logic. Both at the object and at the
meta level the importance of classical logic is beyond dispute in
nonmonotonic logics. Engaging in nonmonotonic logics means aiming at
extending classical logic, rather than replacing it tout court...
Chapters 24 constitute the core of the book in which the author
presents three canonical constructions to obtain nonmonotonic
consequence relations out of monotonic ones. The author follows a
general pattern for introducing such constructions. The starting point
is always the mathematical machinery provided by classical consequence.
It is fundamental to notice that the nonmonotonic consequence relations
discussed in the book all rest on the very same language as classical
propositional logic. The second step consists in introducing a bridge
consequence relation. Such a (monotonic) bridge is then used to
construct a nonmonotonic consequence relation...
The main idea of Chapter 2  Using additional background assumptions 
is simple and powerful: distinguishing among local and background
assumptions. It is reasonable to believe that when making inferences we,
intelligent reasoners, do not consider all the information available to
us, that is the premisses of our logical argument, as "equally
conspicuous". In particular it seems appropriate to distinguish between
the information embodying "the current premises" of our argument  the
set of local assumptions  from the set of assumptions which we commit
to somehow tacitly  the set of background assumptions (or expectations)...
Allowing the set of background assumptions to vary  essentially in a
consistency preserving way  with the set of local assumption amounts to
enabling nonmonotonic reasoning, as captured by the default assumption
consequence relation, fully investigated in Section 2.2...
However, when considering default assumption consequence we face, in the
author's terminology, a basic Dilemma. Makinson proves, in fact, that if
the set of background assumptions is not closed under classical
consequence, then it is not language invariant...
As to the latter unwelcome consequence, a number of solutions are
discussed... All these variations allow the set of background
assumptions to be closed under classical consequence yet avoiding the
collapse of default assumption consequence into the classical one.
Section 2.3 (and the corresponding exercises and problems) illustrates
this at length...
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontologforum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgibin/wiki.pl?WikiHomePage#nid1J
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontologforum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgibin/wiki.pl?WikiHomePage#nid1J
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontologforum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgibin/wiki.pl?WikiHomePage#nid1J
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontologforum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgibin/wiki.pl?WikiHomePage#nid1J (01)
