Re: Boyers Hypothesis

• Mail folder: QED
• Next message: Alan Bundy: "Re: Document -- What's Done and What's to be Done"
• Previous message: jt@linus.mitre.org: "Re: Analytica and Boyer's Hypothesis "

Via: uk.ac.edinburgh.aifh; Mon, 26 Apr 1993 13:39:42 +0100
Date: Mon, 26 Apr 93 13:39:34 BST
Message-id: <28659.9304261239@etive.aisb.ed.ac.uk>
From: Alan Bundy <bundy@aisb.ed.ac.uk>
Subject: Re: Boyers Hypothesis
To: jt@linus.mitre.org
In-Reply-To: jt@org.mitre.linus's message of Sun, 25 Apr 93 10:44:30 -0400
Phone: 44-31-650-2716
Fax: 44-31-650-6516
Fcc: +qed.mai
Cc: qed@aisb.ed.ac.uk
Sender: qed-owner
Precedence: bulk

Javier

>                       BOYER's HYPOTHESIS
> 
>   For any theorem the length l_c of its computer proof is not significantly
>   larger than the length l_i of its rigourous (but possibly informal)
>   proof.

	There seems to be an implict assumption behind your and
other's uses of the Boyer hypothesis that a computer proof has a
unique Boyer number. But this is not true of tactic based
provers. The whole proof may be generated by a single tactic.
This big tactic may break down into smaller ones and so on until
eventually it is unpacked into into applications of rules of
inference of the base logic. It may be possible to read the proof
at many different levels, eg a 1 step proof at the top level, a
20,000 step proof at the bottom level. If the tactics are
well-designed then the most congenial level to read it may be at
some intermediate tactic level and this may correspond well with
the rigorous proof, or with some higher level informal proof.

	It may also be possible to input the proof at this higher
level as well as read it there.


			Alan