Abstract :
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.
Keywords :
formal logic; model-based reasoning; program verification; theorem proving; automated reasoning method convergence; automated theorem proving; best-of-both-worlds motivation; built-in reasoning support modulo background theories; equality arithmetic; first-order logic subsets; integer arithmetic; logical theories; model evolution calculus; model evolution-based theorem proving; propositional logic; reasoning method integration; software verification; Artificial intelligence; Cognition; Computational modeling; Context awareness; Data structures; Intelligent systems; Knowledge based systems; automated reasoning; automated theorem proving; intelligent systems; knowledge representation;
