Trustworthy Systems

Proving infinite satisfiability


Peter Baumgartner and Joshua Bax



We consider the problem of automatically disproving invalid conjectures over data structures such as lists and arrays over integers, in the presence of additional hypotheses over these data structures. Unfortunately, current theorem provers are rather weak when it comes to computing counter-models in these cases (absence of finite models, incompleteness of provers due to quantifiers and arithmetics). As an alternative, we investigate a simple approach based on refutational theorem proving. We assume that the data structure axioms are satisfiable and provide a template language for additional hypotheses such that satisfiability is preserved. Then, disproving is done by proving that the negated conjecture follows. By means of examples, we demonstrate that our template language is reasonably expressive and that our approach works well with current theorem provers (Z3, SPASS+T and Beagle).

BibTeX Entry

    publisher        = {Springer},
    doi              = {10.1007/978-3-642-40537-2_5},
    month            = dec,
    booktitle        = {International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
    paperurl         = {},
    year             = {2013},
    editor           = {{Ken McMillan, Aart Middeldorp and Andrei Voronkov}},
    keywords         = {automated deduction, theorem proving, disproving, verification},
    title            = {Proving Infinite Satisfiability},
    pages            = {86--95},
    author           = {Baumgartner, Peter and Bax, Joshua},
    address          = {Stellenbosch, South Africa}