Generation of theory lemmata in SMT-solving

Advisors: David Monniaux

In the DPLL(T) approach of SMT-solving, as implemented in most tools, the dictionary of elementary propositions used in theory lemmata is largely fixed by the vocabulary of the initial formula. For instance, in the linear theory of the reals, such tools never invent any elementary proposition. A consequence is that some theorems that admit short proofs if new elementary propositions are used only have exponentially sized proofs, leading to exponential running time for DPLL(T) solvers.

The goal of this internship is to generate new elementary propositions that can summarize several theory lemmata.

Contact | Site Map | Site powered by SPIP 3.1.13 + AHUNTSIC [CC License]

info visites 1693554