Search for faster and shorter proofs using machine generated lemmas

Natural Forests in the Temperate Zone of Europe – Values and Utilisation

Petr Pudlák

Others  :  http://CEUR-WS.org/Vol-192/paper03.pdf
PID  :  392

来源: CEUR

【 摘 要 】

When we have a set of conjectures formulated in a common language and proved from a common set of axioms using an automated theorem prover, it is often possible to automatically construct lemmas that can be used to prove the conjectures in a shorter time and/or with shorter proofs. We have implemented a system that repeatedly tries to improve the set of assumptions for proofs of given conjectures using lemmas that it extracts from the proofs constructed by an automated theorem prover. In many cases it can significantly reduce the total time or the overall sum of the lengths of the proofs of the conjectures. We present several examples of such sets of conjectures and show the improvements gained by the system.