1Model Evolution Based Theorem Proving

Abstract—The area of Automated Theorem Proving is char-acterized by the development of numerous calculi and proof procedures, from “general purpose ” to rather specialized ones for specific subsets of first-order logic and logical theories. In this article I highlight two trends that have received considerable attention over the last ten years. The one is the integration of reasoning methods for propositional and for first-order logic, with a best-of-both-worlds motivation. The other is built-in reasoning support modulo background theories, such as equality and inte-ger arithmetic, which are of pivotal importance for, e.g., software verification applications. I will survey the major paradigms in this space from the perspective of our own developments, mainly the model evolution calculus. It is an ongoing quest for the convergence of automated reasoning methods. I. FROM PROPOSITIONAL TO INSTANCE-BASED METHOD