@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}
}