Skip to main content
CSIRO Logo Data 61 logo

ME(LIA) — model evolution with linear integer arithmetic constraints

Authors

Peter Baumgartner, Alexander Fuchs and Cesare Tinelli

NICTA

The University of Iowa
USA

Abstract

Many applications of automated deduction require reasoning modulo some form of integer arithmetic. Unfortunately, theory reasoning support for the integers in current theorem provers is sometimes too weak for practical purposes. In this paper we propose a novel calculus for a large fragment of first-order logic modulo Linear Integer Arithmetic (LIA) that overcomes several limitations of existing theory reasoning approaches. The new calculus --- based on the \emph{Model Evolution} calculus, a first-order logic version of the propositional DPLL procedure --- supports restricted quantifiers, requires only a decision procedure for LIA-validity instead of a complete LIA-unification procedure, and is amenable to strong redundancy criteria. We present a basic version of the calculus and prove it sound and (refutationally) complete.

BibTeX Entry

  @inproceedings{Baumgartner_FT_08,
    month            = nov,
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/1102.pdf},
    publisher        = {Springer},
    booktitle        = {Proceedings of the 15thInternational Conference on Logic for Programming, Artificial Intelligence
                        and Reasoning},
    editor           = {{Iliano Cervesato, Helmut Veith, Andrei Voronkov}},
    author           = {Baumgartner, Peter and Fuchs, Alexander and Tinelli, Cesare},
    year             = {2008},
    pages            = {258--273},
    title            = {{ME}({LIA}) --- Model Evolution With Linear Integer Arithmetic Constraints},
    address          = {Doha, Qatar}
  }

Download