@inproceedings{Korovin2010iProver-Eq,
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.},
address = {Berlin / Heidelberg},
author = {Konstantin Korovin and Christoph Sticksel},
booktitle = {5th International Joint Conference on Automated Reasoning, IJCAR 2010},
isbn = {978-3-642-14202-4},
journal = {Automated Reasoning},
location = {Edinburgh, UK},
pages = {196--202},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {iProver-Eq: An Instantiation-Based Theorem Prover with Equality},
year = {2010}
}