iProver-Eq: An Instantiation-Based Theorem Prover with Equality

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, firstorder 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.

• Type: Conference
• Year: 2010
• Where: CADE
• Authors: Konstantin Korovin, Christoph Sticksel
• Keywords: CADE 2010, Equational Reasoning, First-order Reasoning, Logical Reasoning, Superposition-based Equational Reasoning