Re: resolution

The motivation for proof objects for mizar isn't to reduce the 
high-levelness of the mizar language, forcing us to work directly with 
raw, totally explicit  deductions, but to provide a "gold standard" so 
that when mizar changes (new language constructs, smarter/faster/better 
checker, etc.), as it frequently (?) does, there is an objective proof 
object that one can refer to.  I certainly wouldn't want to read these 
big proof objects; I'd much rather stick with mizar texts.  But I would 
like to have them around.  Since what is "obvious" is always changing, 
it seems desirable to me to have a format that doesn't change (or at 
least not nearly as often, and not for the same reasons, as mizar 
changes).

Obtaining proof objects as you suggest, using prover9, is what I had in 
mind.  I didn't know about TPTP support for suppositional proofs; 
thanks.

(Proof objects for mizar also would be a fascinating playground for 
proof theorists and automated deduction researcher, too, but that's not 
the main motivation, I'd say.)

Piotr?

On 2011-08-12 21:55:52 +0000, Josef Urban said:

> 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 <[email protected]> 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/


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