Model Evolution-Based Theorem Proving

The area of automated theorem proving is characterized 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. This article highlights two trends that have received considerable attention over the last 10 years. 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 integer arithmetic, which are of pivotal importance for, for example, software verification applications. This survey of the major paradigms in this space comes from the perspective of my own developments, mainly the model evolution calculus. This is an ongoing quest for the convergence of automated reasoning methods.