Evolving model evolution

摘要: Automated theorem proving is a method to establish or disprove logical theorems. While these can be theorems in the classical mathematical sense, we are more concerned with encodings of properties algorithms, hardware and software. Especially area verification, propositional logic used widely industry. Satisfiability Module Theories (SMT) set logics which extend theories relevant for specific application domains. In particular, software verification has received much attention, efficient algorithms have been devised reasoning over arithmetic data types. Built-in support by decision procedures often significantly than reductions (SAT). Most SAT solvers based on DPLL architecture, also basis most SMT solvers. The main shortcoming both kinds weak non-ground reasoning, noticeably limits applicability real world systems. Model Evolution Calculus (ME) was as lifting architecture from setting full first-order logic. previous work, created solver Darwin an implementation ME, showed how adapt improvements setting. first half this thesis ME Darwin. First, lift further crucial ingredient solvers, lemma-learning, evaluate its benefits. Then, show use finite model finding, benefits lemma-learning.