Trustworthy Systems

Model evolution based theorem proving


Peter Baumgartner



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. 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 integer 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.

BibTeX Entry

    doi              = {10.1109/MIS.2013.124},
    month            = feb,
    paperurl         = {},
    journal          = {IEEE Intelligent Systems Magazine (IEEE ISM)},
    year             = {2014},
    keywords         = {autamated theorem proving},
    volume           = {29},
    title            = {Model Evolution Based Theorem Proving},
    number           = {1},
    author           = {Baumgartner, Peter},
    pages            = {4--10}