Paper Info
Title
iProver --- An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
Abstract
iProver is an instantiation-based theorem prover which is based on Inst-Gen calculus, complete for first-order logic. One of the distinctive features of iProver is a modular combination of instantiation and propositional reasoning. In particular, any state-of-the art SAT solver can be integrated into our framework. iProver incorporates state-of-the-art implementation techniques such as indexing, redundancy elimination, semantic selection and saturation algorithms. Redundancy elimination implemented in iProver include: dismatching constraints, blocking non-proper instantiations and propositional-based simplifications. In addition to instantiation, iProver implements ordered resolution calculus and a combination of instantiation and ordered resolution. In this paper we discuss the design of iProver and related implementation issues.
Year
DOI
Venue
2008
10.1007/978-3-540-71070-7_24
IJCAR
Keywords
Field
DocType
redundancy elimination,modular combination,related implementation issue,distinctive feature,system description,inst-gen calculus,resolution calculus,first-order logic,dismatching constraint,state-of-the-art implementation technique,sat solver,instantiation-based theorem prover,indexation,theorem prover,first order logic
Discrete mathematics,Programming language,Computer science,Automated theorem proving,Boolean satisfiability problem,Search engine indexing,Algorithm,Theoretical computer science,First-order logic,Redundancy (engineering),Modular design
Conference
Citations 
PageRank 
References 
58
1.96
9
Authors
1
Name
Order
Citations
PageRank
Konstantin Korovin128820.64