The scripts for the ProofPower mathematical case studies have a little tool 
called "check_thms" which does a quality assurance check on the the theorems in 
a theory. It checks against:

a) Theorems with free variables. Typically this means you forgot an outer 
universal quantifier. Later on you will be puzzled when tools like the 
rewriting tools think you don't want the free variables to be instantiated.

b) Theorems with variables bound by logical quantifiers (universal, existential 
and unique existential) that are not used in the body of the abstraction. This 
happens for various reasons (often hand in hand with (a)). It is misleading for 
the reader and can be confusing when you try to use the theorem.

It outputs a little report on any problems it finds.

I am considering putting a bug-fixed and documented version of check_thms in 
the next working release of ProofPower. Any comments or suggestions for other 
things to check for would be welcome. This is currently just for HOL, but I 
could do something similar for Z too.

Regards,

Rob.
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to