TY - GEN
T1 - ME(LIA) - Model evolution with linear integer arithmetic constraints
AU - Baumgartner, Peter
AU - Fuchs, Alexander
AU - Tinelli, Cesare
PY - 2008
Y1 - 2008
N2 - 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 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.
AB - 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 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.
UR - http://www.scopus.com/inward/record.url?scp=58049114884&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-89439-1_19
DO - 10.1007/978-3-540-89439-1_19
M3 - Conference contribution
SN - 3540894381
SN - 9783540894384
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 258
EP - 273
BT - Logic for Programming, Artificial Intelligence, and Reasoning - 15th International Conference, LPAR 2008, Proceedings
T2 - 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2008
Y2 - 22 November 2008 through 27 November 2008
ER -