Re: resolution

Below is a fragment of a discussion about the power of the mizar checker
between me and Artur Kornilowicz.  Perhaps others on the mizar-forum
might be interested in these issues.

================================================================================

Hi Artur,

Artur Kornilowicz wrote:

> in Wroclaw we were talking about resolution. I've mentioned an example
> in XBOOLE_1. The story is: in XBOOLE_1 there is a theorem
>
> theorem
> X c= Y implies X c= Z \/ Y
>
> with its original proof
>
> proof
> assume X c= Y;
> then A1: Z \/ X c= Z \/ Y by Th9;
> X c= Z \/ X by Th7;
> hence X c= Z \/ Y by A1,Th1;
> end;
>
> where Th1, Th7 are:
>
> theorem Th1:
> X c= Y & Y c= Z implies X c= Z
>
> theorem Th7:
> X c= X \/ Y
>
> After implementation of resolution (2 general premisses in one
> inference) TRIVDEMO and RELPREM found a proof
>
> theorem
> X c= Y implies X c= Z \/ Y by Th1,Th7;
>
> But further experiments with some parameters of resolution made its
> weaker, and I rewritten the proof as:
>
> theorem
> X c= Y implies X c= Z \/ Y
> proof
> Y c= Z \/ Y by Th7;
> hence thesis by Th1;
> end;
>
> which is much nicer than the original one. :-)

Thanks for reminding me of our discussion about resolution. I am
fascinated by the attempts to make the checker stronger, and to see the
tradeoffs of doing so (shorter proofs, but which might be more difficult
to understand). I am on the fence about whether the straightforward
justification of

X c= Y implies X c= Z \/ Y

is such a case. I admit that I did have to look twice at the statement
to make sure that it was valid. But on the other hand, once I saw that
it was valid, I was content to accept the straightforward justification.
I did some experiments myself in XBOOLE_1 and found some interesting
cases like the one you mention. I'm fascinated by seeing how a machine
(that checker) can justify the statements given to it, sometimes in
unexpected ways.

I'd be curious to know how to do my own tuning and experimentation with
resolution. For example, can one enable checking for three universal
premises? Four?

I think Piotr's idea of having a uniform notation for proofs that is
"utterly formal" -- e.g., a raw natural deduction proof or a sequent
calculus proof, possibly even a Hilbert-style deduction, in unsorted or
possibly many-sorted first-order logic -- makes sense. It might not even
be so hard to cook up some initial experiments for this. Following the
proof skeleton, it should be trivial to find a skeleton for a natural
deduction proof or sequent calculus proof. The real challenge is to
replace each by/from with such a deduction. We could use Josef's ATP
tools to find a sufficient set of premises for each by/from statement,
and then try to do proof search in a natural deduction calculus or
sequent calculus using exactly these premises. There has been some work
on proof search in natural deduction (by Wilfried Sieg, e.g.), and there
are even some systems out there (Sieg's, for example), but I'm not sure
how flexible they are and whether they could handle the non-trivial
search problems that we'd give. Geoff Sutcliffe might even have a
suitable system available for our purposes on SystemOnTPTP.

Getting one's hands on a "raw" representation of a non-trivial theorem
would be great, though I remain somewhat skeptical about time and space
issues. I am open to being convinced, though, and would be willing to do
the experiments to prove myself right/wrong. I wonder if we'd have a
similar experience as the Coq people in Nijmegen who, having given a
formal proof of the fundamental theorem of algebra in the calculus of
inductive constructions, tried to actually use the giant proof object
they had constructed to find a root of some very simple polynomial,
thereby crashing their Coq instance. A formalist can dream of actually
getting Herbrand terms for theorems of interest, but I wonder if these
things are going to be at all manageable. I think we might need to
investigate working not in raw unsorted or many-sorted first-order
logic, but have instead a mechanism not unlike mizar's own for
conservatively extending the theory with new functions and predicates.

Best,

Jesse

-- Jesse Alama
http://centria.di.fct.unl.pt/~alama/