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, 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.
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: inference system and completeness (2017)
- Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
- Plaisted, David A.: History and prospects for first-order automated deduction (2015)
- Saghafi, Salman; Danas, Ryan; Dougherty, Daniel J.: Exploring theories with a model-finding assistant (2015)
- Brown, Chad E.: Reducing higher-order theorem proving to a sequence of SAT problems (2013)
- Korovin, Konstantin: Inst-Gen -- a modular approach to instantiation-based automated reasoning (2013)
- Plaisted, David A.; Miller, Swaha: The relative power of semantics and unification (2013)
- Korovin, Konstantin; Sticksel, Christoph: iProver-Eq: an instantiation-based theorem prover with equality (2010)