[FOM] shocked?
Rob Arthan
rda at lemma-one.com
Wed Oct 29 05:37:41 EST 2003
> Message: 8
> Date: Tue, 28 Oct 2003 13:12:54 -0500
> From: Harvey Friedman <friedman at math.ohio-state.edu>
> Subject: [FOM] shocked?
> To: fom <fom at cs.nyu.edu>
> Message-ID: <BBC41BD6.6F33%friedman at math.ohio-state.edu>
> Content-Type: text/plain; charset="US-ASCII"
>
> I seem to be somewhat shocked that the recent thread concerning "what is a
> proof" does not seem to be taking into account the rather massive
> literature concerning Proof Assistants, where actual human beings actually
> interact with actual computers to get humanly created proofs checked. No
> line by line Hilbert style system is even remotely used in such systems.
> Instead, they are based on variants of natural deduction, with an emphasis
> on lemma refinement, just like most ordinary proofs humans like.
This is not strictly true. Many practical mechanized theorem-proving systems
follow Milner's LCF paradigm (e.g., the several variants of Mike Gordon's
HOL, ProofPower, Isabelle, NuPrl etc.). These systems do, in effect, check
line-by-line primitive inferences at the lowest level of their operation.
However, this is analogous to the machine code level in programming and, as
in programming, not many users work at this level.
Typical users constructs proofs using higher-level tools. The higher level
tools are analogous to (fairly intelligent) interpreters or compilers that
can generate a string of primitive inferences to prove goals in a given
class. Very commonly, the higher-level tools include a framework for
goal-oriented proof, based on Larry Paulson's ideas, which provides a natural
deduction-like look and feel. However in a useful system, the higher-level
tools will also include automatic decision procedures and heuristics for
equational reasoning, first order reasoning, arithmetic etc. etc.
The existence of good automation does change your strategy a little compared
with "ordinary proofs humans like": a common technique is to transform a
given problem, ideally via an equivalence, into a domain where there is a
decision procedure (e.g., use induction to reduce a diophantine problem into
linear arithmetic) and then throw the decision procedure at the result
(without much caring whether the transformed problem is easy for a human to
understand, since the decision procedure is better at that kind of thing than
a human is).
Regards,
Rob Arthan.
More information about the FOM
mailing list