Name
Abstract | ||
|---|---|---|
iProver-Eq is an implementation of an instantiation-based calculus Inst-Gen-Eq which is complete for first-order logic with equality. iProver-Eq extends the iProver system with superposition-based equational reasoning and maintains the distinctive features of the Inst-Gen method. In particular, first-order reasoning is combined with efficient ground satisfiability checking where the latter is delegated in a modular way to any state-of-the-art SMT solver. The first-order reasoning employs a saturation algorithm making use of redundancy elimination in form of blocking and simplification inferences. We describe the equational reasoning as it is implemented in iProver-Eq, the main challenges and techniques that are essential for efficiency. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-14203-1_17 | IJCAR |
Keywords | Field | DocType |
instantiation-based calculus inst-gen-eq,distinctive feature,efficient ground satisfiability checking,superposition-based equational reasoning,equational reasoning,inst-gen method,iprover system,first-order reasoning,instantiation-based theorem prover,main challenge,first-order logic,theorem prover,first order logic,first order,satisfiability | Automated reasoning,Discrete mathematics,Computer science,Automated theorem proving,Satisfiability,Algorithm,Theoretical computer science,Redundancy (engineering),Deductive reasoning,Modular design,Reasoning system,Satisfiability modulo theories | Conference |
Volume | ISSN | ISBN |
6173 | 0302-9743 | 3-642-14202-8 |
Citations | PageRank | References |
10 | 0.47 | 8 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Konstantin Korovin | 1 | 288 | 20.64 |
| Christoph Sticksel | 2 | 15 | 1.28 |