Re: Godel's Incompleteness and Nonmonotonic Logic

From: Herman Jurjus (h.jurjus_at_hetnet.nl)
Date: 08/25/04 

Date: Wed, 25 Aug 2004 19:56:41 +0200

Student wrote:
[snip]

>>Maybe you could give a rigorous definition of "answer set style logics"?
>
>
>
> Take classical logic, with one more rule: if "F" is not provable, then
> "not F" is provable, where F is any well formed formula in first-order
> predicate logic, i.e. negation commutes with provability, as is
> seemingly the case in these "Answer Set" logics such as AnsProlog and
> its varients.

Nope, that's not answer set programming. Where did you read that?

Answer set programming defines a number of 'extensions' to a theory
as the fixed points of a certain operator. Based on these extensions, it
is determined whether a formula is inferred or not. Given the way it
works, the inference relation it provides is fundamentally different
from that of first order logic.

It works pretty much like default logic, which also uses fixpoints.
To learn about inference defined via fixpoints, you might try:

David Poole, Default Logic, in D. M. Gabbay et al (eds),
Handbook of Logic in Artificial Intelligence and Logic Programming,
Volume 3, Oxford University Press, 1994.

(It is available via David Poole's homepage, or on:
   http://www.cs.ubc.ca/spider/poole/pubs.html
almost at the bottom of the page, under Books / Chapters.)

A good source for answer set programming is:
   http://www.cs.uni-potsdam.de/~torsten/asp/

> Finally, with regards to your comments on the importance of
> computability... my original question is not of computability, it is
> about consistency. The undecidability (lack of computability) of
> provability is not the same as provability, which is what is referred
> to in the aforementioned extension to classical logic.

For default logic, inconsistency works pretty much the same as for
classical logic: some theories are consistent, others are not.
It's not difficult to find simple default theories that definitely have
extensions. And i'm sure it works the same way for answer set programming.

The Goedel sentence contains a coding of a 'provability' predicate.
For fixpoint systems such as default logic or asp, such a coding is not
available. (The notion of 'provable' there is not the same as classical
provability.) 

-- 
Cheers,
Herman Jurjus

Relevant Pages
Quantcast