Open AccessTheorem recycling for Theorem Proving
Author(s) -
Nikolaj Bjørner,
Lev Nachmanson
Publication year - 2018
Publication title -
epic series in computing
Language(s) - English
Resource type - Conference proceedings
ISSN - 2398-7340
DOI - 10.29007/r58f
Subject(s) - projection (relational algebra) , pruning , automated theorem proving , realization (probability) , computer science , dual (grammatical number) , quantifier elimination , quantifier (linguistics) , algebra over a field , projection method , algorithm , theoretical computer science , mathematics , artificial intelligence , dykstra's projection algorithm , pure mathematics , programming language , art , statistics , literature , agronomy , biology
In this paper we examine two cases where solutions to one system of constraints can be used or adapted to solutions to others, for free. We first revisit a method by Bromberger for lifting solutions to systems over linear real arithmetic to solutions over integers. We extend it by identifying several scenarios where solutions over reals can be directly used to establish solutions over integers. Our second case discusses model-based projection, which was introduced in two different places with different, dual, definitions. It turns out that one can typically use the same underlying engines to compute both versions of model based projection and we characterize when this is the case. We extend projection with model- based realization. When used for quantifier reasoning, it serves a complementary purpose than projection. While projection can be used for computing conflict clauses, realizers may be used for forward pruning.