Resultion Method not suitable for non-classical Logics?

[Jan Burse]

Dear All

I am just checking whether there is any chance
of recovering non-classical reasoning from the
resultion refutation method. But I don't see it.

It starts with the refutation approach, which
says instead of trying to proof

G |- A (i)

We add the negation of the conclusion to the
premisses, and try to derive a contradiction:

G, ~A |- f (ii)

But moving from (ii) to (i) looks to me the
same as double negation elimination, and is
for example not valid in intuitionistic logic.

So I would not be able to use refutation
in intuitionistic logic. Rigtht?

Next the resultion rule requires that
everything is brought into clausal form.
Which involves again double negation. For
example the following formula:

~(~~P -> P)

Gives:

~P & P

Finally the resultion rule itself is not
paraconsistent. It says, where A and B
can be empty:

A v X B v ~X
----------------
A v B

This gives for the formula from before:

~P P
-----------
f

This would be still fine in intuitionistic
logic (yielding the already indicated
wrong result due to the clausal form), but
for example for minimal logic this is not ok.

So what would automated proof methods be
for non-classical logic that would owe
something to Robinsons invention?

Extending resultion by modal operators, and
mapping the non classical logic to some
modal translation?

Any other approaches?

Bye

[Jan Burse]

Jan Burse schrieb:

>
> ~P P
> -----------
> f
>
> This would be still fine in intuitionistic
> logic (yielding the already indicated
> wrong result due to the clausal form), but
> for example for minimal logic this is not ok.

Oops, in minimal logic we have:

|- P -> (P -> f) -> f.

So the resolution is fine, at
least in the above case.

Bye

[Alan Smaill]

Jan Burse <janb...@fastmail.fm> writes:

> Dear All
>
> I am just checking whether there is any chance
> of recovering non-classical reasoning from the
> resultion refutation method. But I don't see it.

...

> So what would automated proof methods be
> for non-classical logic that would owe
> something to Robinsons invention?
>
> Extending resultion by modal operators, and
> mapping the non classical logic to some
> modal translation?
>
> Any other approaches?

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'.

> Bye
>
>
>

--
Alan Smaill

[Jan Burse]

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

[Jan Burse]

Jan Burse schrieb:

> 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

I just stepped over the following book chapter:

7.5 Resolution for Ip
Troestlstra, A.S. and Schwichtenberg, H.: Basic Proof Theory,
2nd Edition, 2000, Cambridge University Press

The give show an approach that roughly works
as follows:

First by a method attributed to Zamov, N., namely
to get rid of clausal form and skolem functions.
It is based on adding a variant of the resolution
step, this variant respects also a quantifier.

Then for each subformula positive and negative
clauses are created. Then there are some lemmas
which probably explain some search strategies,
but I don't understand them fully.

Also not clear is combination of the above two.
Anybody knows about systems one can play with?

Bye