CODEWITHSUNDEEP
prolog
atx
atx

Reputation: 5069

Finitely failed derivations in logic

What are finitely failed derivations? Are refutations the same as contradictions in the mathematical sense? What's the difference between general logic programs and definite logic programs?

Upvotes: 0

Views: 241

Answers (1)

user502187
user502187

Reputation:

There are no finitely failed derivations. Only failed derivations and finitely failed derivations trees. A failed derivations is a derivation that ends in failure. For example:

p :- q.
p :- p.
q :- fail.

The derivation that consists of the first rule of p and then the only rule of q is a failed derivation. Derivations might not only fail because an undefined predicate such as fail, but also because some head unification does not completely succeed.

Now what is a finitely failed derivation tree. Well if you look at all the derivations you get a tree. In a finitely failed derivation tree, the tree is finite and each derivation is failed. Finitely failed derivation trees have the following nice property:

- The interpreter terminates.
- The interpreter does not produce any answer substitution.

In practical Prolog systems this means that after posing your question you will get a No after a while (in some Prolog systems a false is displayed). Interestingly the above program will not terminate for the query p. It is an instance of a infinite derivation tree where each derivation is failed. The derivations are:

p - q - fail
p - p - q - fail
p - p - p - q - fail
Etc..

The notion of finitely failed derivation trees is defined for definite Prolog programs. One can now extend the notion of a Prolog program into general Prolog programs. In a general Prolog program the body might contain negative literals. And the idea is that the interpreter regresses into checking for finitely failed derivation trees for these literals.

One important question is how finitely failed derivation trees relate to mathematical derivations. Under what mathematical semantic should a goal fail? And how could we build an interpreter that implements this semantic? A particular class of semantics is based on the refutation method. Here we explain a derivation as establishing a contradiction:

   P, ~G |= f => P |- G

This more or less implies double negation elimination and thus classical logic. But also other logics can be instrumental. As a start you might want to lookup the following book:

Logic for Applications
Anil Nerode, Richard A. Shore
2nd. Edition, 1997, Springer

Bye

Upvotes: 4

Related Questions