Instantiation-based automated reasoning: From theory to practice

Instantiation-based automated reasoning aims at combining the efficiency of propositional SAT and SMT technologies with the expressiveness of first-order logic. Propositional SAT and SMT solvers are probably the most successful reasoners applied to real-world problems, due to extremely efficient propositional methods and optimized implementations. However, the expressiveness of first-order logic is essential in many applications ranging from formal verification of software and hardware to knowledge representation and querying. Therefore, there is a growing demand to integrate efficient propositional and more generally ground reasoning modulo theories into first-order reasoning. © 2009 Springer Berlin Heidelberg.