[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Help - using PVS



Hi,

1. Is there any possibility to disable pretty-printing on the
proof(.prf) file ?
   I have to prove some lemmas, in which each of them had a long proof
   sequence (> 300 commands). Because of the preety printing, the proof
file
   exploded. each proof can take > 200K. 
2. Is there any primitive proof command to expand a definition without 
   simplification ?
3. In the middle of my proof, I wanted to expand a definition.
   Somehow, the command (ex: (expand "x")) took a very long time > 10
minutes.
   Is it because of simplification ? Any suggestion on what should I do
?
   (If it's needed, I have a dump file for the lemma. The file size is
    around 1.2 M)
   fyi: My system is running on LINUX - PII 400 - 256M(RAM)

thanks,
-- 
Kong Woei Susanto
Department of Computing Science - University of Glasgow
17 Lilybank Gardens, Glasgow G12 8RZ, Scotland, United Kingdom.
e-mail: susanto@dcs.gla.ac.uk Ph: +44-141-3304454  fax:+44-141-3304913