Theorem Prover

The Theorem Prover

AProVE used to be able to automatically create induction proofs for several problems. Nowadays, the theorem prover has neither been used nor has someone looked at the code for it. If you are eager to bring back the old days of AProVE as a theorem prover, then you should have a look at the two packages verification.oldframework.Logic and verification.theoremprover. However, there may be classes all over AProVE that are used within the theorem proving code.

The lemma databases and the proofs are stored somewhere as ZIP compressed XML files having the suffix ldb. To to view them you have the unzip them before using gunzip. (First extend the filename by the suffix gz.)

Disclaimer

• The theorem prover was neither used nor tested during the last decade. It may not be working properly anymore. Enter the realm of theorem proving in AProVE at your own risk!