Re: Resultion Method not suitable for non-classical Logics?

Alan Smaill schrieb:

Historically Prolog owed something to the resolution provers around
then. But by taking all input clauses to be definite clauses, and
queries as negated atoms, you get a sublogic of the original set-up
where queries (not double negation) are derivable iff they are
intuitionistic consequence of the original definite clauses (understood
as 'A1 & ... & An -> B'.


Yes, it can be seen in the DEC10 Prolog manual. They say
a fact is a unit-clause, and a rule is a non-unit-clause.
And the resolution that Prolog usually uses is input
resolution, that is one of the two resolvents has to come
from the logic program.

And I agree it can be interpreted for example in minimal
logic, you even don't need conjunction, a definite
clause can be cast as:

A1 -> (... (An -> B) ...)

But still I having more in mind, something that would
go beyond prolog. Question is not whether Prolog can
be viewed as non classical. But question is whether a
non classical logic in full bloom could be dealt with
with methods found in resolution refutation.

Prolog is somehow ruled out, because when refering to
the resolution refutation method, I am refering to
the method use in automated theorem proving. Thus when
the input is an arbitrary set of premisses, not
necessarily leading to definite clauses.

For example the following rule that is also found in
intuitionism when cast as natural deduction:

G, A |- B
-----------
G |- A -> B

It doesn't work for Prolog and resolution refutation method.
Because refutation method requires to add the negation
of A -> B to G, and then check for derivation of f.

But classicaly when I add the negation of A -> B to G,
I get the theory G, A, ~B, which is only on first sight
horn. It is not horn because A and B might have variables
that communicate, and thus taking the clausal approach,
where each clause is automatically unversally quantified,
would not be valid.

So any ideas to fix resolution?

Bye
.

Relevant Pages

  • Re: Out of local stack? (SWI)
    ... that your clauses go from the most spécific case to the most général ... all the lines 'Ontimer" and see wich one is always choosen..... ... >>and standard Prolog is pretty simple minded. ...
    (comp.lang.prolog)
  • question about last call optimization
    ... I have a question about last call optimization using euclids algorithm ... Okay the prolog literature gives the procedure as: ... Now will prolog "last call optimize" this. ... What about if we switch the order of the clauses as such: ...
    (comp.lang.prolog)
  • Re: Simple propositional calculus with prolog
    ... Now horn clauses are a subset of clauses. ... represent your problem in Prolog, ... Transformation into clauses works easiest when the problem is ...
    (comp.lang.prolog)
  • Re: The Da Vinci Code.
    ... Prolog language which just don't stand up in practice. ... get experienced, you realize that most clauses *are*, in fact, ...
    (alt.usage.english)