Foundations for Natural Proofs and Quantifier Instantiation

Опубликовано 29 сентября 2017, 17:26

The logics required to support program verification go much beyond the class of decidable logics available today, and beyond the quantifier-free logics supported by SMT solvers today. In particular, when dealing with unbounded structures such as arrays or dynamically manipulated heaps, the current support for automated reasoning falls short of what we desire. The typical ways of dealing with such logics have been through heuristics, and in particular quantifier instantiation heuristics to deal with quantified logics and the so-called natural proof heuristics that employ recursion-unfolding tactics to deal with recursively defined datatypes. We give foundational results that explain the efficacy of heuristics used for dealing with quantified formulas and recursive definitions. We develop a framework for first order logic (FOL) over an uninterpreted combination of background theories. Our central technical result is that systematic term instantiation is *complete* for a fragment of FOL that we call safe. Coupled with the fact that unfolding recursive definitions is essentially term instantiation and with the observation that heap verification engines generate verification conditions in the safe fragment explains the efficacy of verification engines like natural proofs that resort to such heuristics. Furthermore, we study FOL with recursive definitions that have least fix point semantics and show that though they are not amenable to complete procedures, we can systematically introduce induction principles that in practice bridge the divide between FOL and FOL with recursive definitions. 

See more on this video at microsoft.com/en-us/research/v...