Proving infinite satisfiability

Peter Baumgartner; Joshua Bax

doi:10.1007/978-3-642-45221-5_6

Proving infinite satisfiability

Peter Baumgartner, Joshua Bax

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Citation (Scopus)

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. 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).

Original language	English
Title of host publication	Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR 2013, Proceedings
Pages	86-95
Number of pages	10
DOIs	https://doi.org/10.1007/978-3-642-45221-5_6
Publication status	Published - 2013
Event	19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2013 - Stellenbosch, South Africa Duration: 14 Dec 2013 → 19 Dec 2013

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8312 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2013
Country/Territory	South Africa
City	Stellenbosch
Period	14/12/13 → 19/12/13

Access to Document

10.1007/978-3-642-45221-5_6

Cite this

Baumgartner, P., & Bax, J. (2013). Proving infinite satisfiability. In Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR 2013, Proceedings (pp. 86-95). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8312 LNCS). https://doi.org/10.1007/978-3-642-45221-5_6

@inproceedings{599292ddca3e4aeca8c9243dd5e415b6,

title = "Proving infinite satisfiability",

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. 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).",

author = "Peter Baumgartner and Joshua Bax",

year = "2013",

doi = "10.1007/978-3-642-45221-5_6",

language = "English",

isbn = "9783642452208",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "86--95",

booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR 2013, Proceedings",

note = "19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2013 ; Conference date: 14-12-2013 Through 19-12-2013",

}

Baumgartner, P & Bax, J 2013, Proving infinite satisfiability. in Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR 2013, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8312 LNCS, pp. 86-95, 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2013, Stellenbosch, South Africa, 14/12/13. https://doi.org/10.1007/978-3-642-45221-5_6

Proving infinite satisfiability. / Baumgartner, Peter; Bax, Joshua.
Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR 2013, Proceedings. 2013. p. 86-95 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8312 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Proving infinite satisfiability

AU - Baumgartner, Peter

AU - Bax, Joshua

PY - 2013

Y1 - 2013

N2 - 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. 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).

AB - 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. 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).

UR - http://www.scopus.com/inward/record.url?scp=84893909265&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-45221-5_6

DO - 10.1007/978-3-642-45221-5_6

M3 - Conference contribution

SN - 9783642452208

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 86

EP - 95

BT - Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR 2013, Proceedings

T2 - 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2013

Y2 - 14 December 2013 through 19 December 2013

ER -

Proving infinite satisfiability

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this