Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <9502250706.AA09027@maui.cs.ucla.edu>
To: info-hol@leopard.cs.byu.edu
Subject: FWD: Recent proofs with nqthm?
Date: Fri, 24 Feb 95 23:06:36 PST
From: chou@cs.ucla.edu


I wonder what HOL hackers have to say about the conclusions
of the following message.

Cheers,
- Ching Tsun


Begin forwarded message:

Date: Fri, 24 Feb 95 18:35:04 GMT
From: laurence@gyptis.univ-mrs.fr (Laurence Pierre)
To: nqthm-users@cli.com
Subject: RE: Recent proofs with nqthm?


>> Hello to all!
>>
>> I will be giving a talk end of next week here in Germany on nqthm for  
some
>> hardware oriented people. I have a slide with "proofs done with NQTHM"
>> and a bibliography, I believe I have pretty much everything up until
>> the summer of 94. Any newer TechReports/Journal articles/Whatever
>> on proofs that have been done? Please mail me at weberwu@tfh-berlin.de
>>
>> We will be discussing the usefulness of nqthm as a proof tool, any
>> comments such as Matt Kaufmann's from last week much appreciated, both
>> positive and negative. Please indicate if I can use your comment in a
>> summary, or if you would rather it remain anonymous.
>>
>> Thanks!
>> Debora Weber-Wulff
>> TFH Berlin

At the end of March, I will also be giving a lecture on Nqthm, to French
PhD students. I intend to mention the current state-of-the-art of
developments with Nqthm (in particular in the field of hardware  
verification).
So, if you have a complete reference list, I will be interested in
getting it. Could you please send me this information ?

A summary of my comments about the usefulness of Nqthm for hardware
verification is the following :
I have been using Nqthm since 1988 (it was not called Nqthm at that
time, as far as I know !). My work is aiming at :
   - using Nqthm for verifying the observational equivalence of digital
     devices (I did not investigate the verification of temporal properties,
     for instance),
   - defining everything that is needed for reasoning with Nqthm on
     circuit descriptions preliminary given in a Hardware Description
     Language (VHDL for instance) : methods for tranlating from the HDL
     to Nqthm, and specialized methods (in particular for generalization) 

     for "adapting" the obtained Nqthm events before starting the proof
     process.
In our team, we have been comparing Nqthm with other provers, with respect
to these 2 aspects, in particular with OBJ3 and the Larch Prover. My own 

conclusion about this comparison is that Nqthm gives more satisfying
results than the others :
   - induction is fully mechanized (this aspect is very useful for us,
     either for reasoning on synchronous devices - induction on time -
     or for reasoning on replicated architectures - induction on the
     structure - ), and the induction mechanism did not exist in OBJ3 

     (when we experimented with it, I don't know if it exists now), and 

     is less elaborate in LP than in Nqthm.
   - as far as I know, it is also the only prover which implements a
     generalization heuristics (which is also very useful for us).
   - it is not too difficult to express structural or behavioural
     circuit descriptions in the Boyer-Moore logic (in particular, it
     was less easy in OBJ3, at least for us !!).
   - and finally, using Nqthm requires less expertise than for instance
     HOL or COQ.
Those are my main conclusions, but many other things can be said about
the advantages of Nqthm !

Kind regards,

Laurence PIERRE
CMI/Universite de Provence
39 rue Joliot-Curie
13453 Marseille cedex 13
FRANCE
e-mail : laurence@gyptis.univ-mrs.fr