Book chapter
Model Evolution with Equality Modulo Built-in Theories
Automated Deduction – CADE-23, pp.85-100
Lecture Notes in Computer Science, Springer Berlin Heidelberg
2011
DOI: 10.1007/978-3-642-22438-6_9
Abstract
Many applications of automated deduction require reasoning modulo background theories, in particular some form of integer arithmetic. Developing corresponding automated reasoning systems that are also able to deal with quantified formulas has recently been an active area of research. We contribute to this line of research and propose a novel instantiation-based method for a large fragment of first-order logic with equality modulo a given complete background theory, such as linear integer arithmetic. The new calculus is an extension of the Model Evolution Calculus with Equality, a first-order logic version of the propositional DPLL procedure, including its ordering-based redundancy criteria. We present a basic version of the calculus and prove it sound and (refutationally) complete under certain conditions.
Details
- Title: Subtitle
- Model Evolution with Equality Modulo Built-in Theories
- Creators
- Peter Baumgartner - Australian National UniversityCesare Tinelli - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Automated Deduction – CADE-23, pp.85-100
- Publisher
- Springer Berlin Heidelberg; Berlin, Heidelberg
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-642-22438-6_9
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 2011
- Academic Unit
- Computer Science
- Record Identifier
- 9984259482702771
Metrics
5 Record Views