Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Tue, 28 Feb 95 12:15:26 EST
From: reetz <reetz@ira.uka.de>
To: David <des@inmos.co.uk>
Cc: info-hol@cs.uidaho.edu
Subject: HOL versus BM (provers with heuristics for chooesing inductions)
Message-Id: <"i80fs2.ira.547:28.02.95.11.15.28"@ira.uka.de>

David Sheperd wrote:

>Since then HOL has improved a lot ... I suspect that things like the
>recursive type definition stuff has appeared since then +  all the
>libraries. While BM may still seem initially more approachable (after
>all, when you start you do simple problems where the BM heuristics can
>probably do everything automatically), I would suspect that HOL would
>rate a lot higher now.

I agree that HOL has improved a lot the last two years. However,
heuristics for choosing induction schemes are STILL missing and that
is really useful. I myself have `played' with RRL [KaZh88] (roughly spoken:
a prover
for many-sorted first order logic plus induction plus knuth-bendix plus
a whole sack of heuristics for choosing induction schemes) for proving
expressions over integers and I found it very useful im comparison
with HOL, where, besides case distinctions on integers in combination
with ARITH_CONV, you have to do even the trivial things manually.
That is the point: I DO NOT want to deal with `simple problems', HOL
should solve them automatically, I want to concentrate on the `real' problems.
But in my >personal< experience, missing things like these heuristics keeps
you proving on a level of UNDISCH, MP, ... almost all the time.

To summarize, I don't think you can say, 'hey, HOL is better than RLL/BM!' or
vice versa. It depends on what kind of proofs you want to perform. So,
IMHO a HOL2000 should merge these two things together...

@inproceedings{KaZh88,
  author      ={{D. Kapur} and {H. Zhang}},
  title       ={{RRL}: a rewrite rule laboratory},
  booktitle   ={9th International Conference on Automated Deduction},
  year        ={1988},
  editor      ={{Lusk} and {Overbeek}},
  pages       ={768--769},
  organization={},
  volume      ={},
  series      ={},
  publisher   ={Springer Verlag},
  address     ={},
  month       ={},
  note        ={},
  key         ={KaZh88},
  keyword     ={Rewrite},
  remark      ={},
  owner       ={}
}