Conference proceeding
(LIA) - Model Evolution with Linear Integer Arithmetic Constraints
Logic for Programming, Artificial Intelligence, and Reasoning, pp.258-273
Lecture Notes in Computer Science, vol 5330
2008
DOI: 10.1007/978-3-540-89439-1_19
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 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.
Details
- Title: Subtitle
- (LIA) - Model Evolution with Linear Integer Arithmetic Constraints
- Creators
- Peter Baumgartner - Data61Alexander Fuchs - University of IowaCesare Tinelli - University of Iowa
- Resource Type
- Conference proceeding
- Publication Details
- Logic for Programming, Artificial Intelligence, and Reasoning, pp.258-273
- Publisher
- Springer Berlin Heidelberg; Berlin, Heidelberg
- Series
- Lecture Notes in Computer Science; vol 5330
- DOI
- 10.1007/978-3-540-89439-1_19
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 2008
- Academic Unit
- Computer Science
- Record Identifier
- 9984259478902771
Metrics
23 Record Views