@inproceedings{1c78b6a69ff9459a8b112449335ea358,
title = "iProver-Eq: An instantiation-based theorem prover with equality",
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. {\textcopyright} 2010 Springer-Verlag.",
keywords = "automated reasoning, instantiation-based methods, implementation techniques",
author = "Konstantin Korovin and Christoph Sticksel",
year = "2010",
doi = "10.1007/978-3-642-14203-1\_17",
language = "English",
isbn = "3642142028",
volume = "6173",
series = "Lecture Notes in Computer Science",
publisher = "Springer Nature",
pages = "196--202",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",
address = "United States",
note = "5th International Joint Conference on Automated Reasoning, IJCAR 2010 ; Conference date: 01-07-2010",
}