Skip to main content

TS

Proving infinite satisfiability

Authors

Peter Baumgartner and Joshua Bax

NICTA

Abstract

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

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

Download

Served by Apache on Linux on seL4.