Sciweavers

Share
CADE
2007
Springer

Semantic Selection of Premisses for Automated Theorem Proving

11 years 5 months ago
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...
Petr Pudlak
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where CADE
Authors Petr Pudlak
Comments (0)
books