Semantic Selection of Premisses for Automated Theorem Proving

We develop and implement a novel algorithm for discovering the optimal sets of premisses for proving and disproving conjectures in first-order logic. The algorithm uses interpretations to semantically analyze the conjectures and the set of premisses of the given theory to find the optimal subsets of the premisses. For each given conjecture the algorithm repeatedly constructs interpretations using an automated model finder, uses the interpretations to compute the optimal subset of premisses (based on the knowledge it has at the point) and tries to prove the conjecture using an automated theorem prover. 1 Importance of selecting appropriate premisses in automated theorem proving A proper set of premisses1 can be essential for proving a conjecture by an automated theorem prover. Clearly, the larger the number of the initial premisses the larger the number of the inferred formulae. And as for the most proving techniques the number of inferred formulae is in general super-exponential in...

• Type: Conference
• Year: 2007
• Where: CADE
• Authors: Petr Pudlak
• Keywords: Automated Reasoning, Automated Theorem Prover, CADE 2007, Conjecture, Premisses