Re: [mizar] Re: resolution

[Josef Urban <josef.urban@gmail.com>]

Hi,

Otter/Prover9 proof objects can be used to make the Mizar "by"
statements totally explicit. When used together with the TPTP syntax
for supposition-style proofs
(http://dx.doi.org/10.1007/s11786-008-0053-7), such explicit Mizar
proofs can be fed into simple independent proof verifiers.

The proof object size is not a big issue if syntax for term/formula
sharing is used. I do not think a normal user wants to see the
detailed proof objects. I like Mizar for its emphasis on trying to get
the "human obviousness" level of proofs right - no other ITP has
focused on that (possibly with exceptions like SAD/Forthel and
Naproche). Having detailed proof objects around could indeed help
experimental investigations trying to pin down what is "obviousness".

Best,
Josef

On Mon, Aug 8, 2011 at 11:22 PM, Jesse Alama <jesse.alama@gmail.com> wrote:
> 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/
>
>