Book chapter
Foundations of Satisfiability Modulo Theories
Logic, Language, Information and Computation, pp.58-58
Lecture Notes in Computer Science, Springer Berlin Heidelberg
01/01/2010
DOI: 10.1007/978-3-642-13824-9_6
Abstract
Satisfiability Modulo Theories (SMT) studies methods for checking the (un)- satisfiability of first-order formulas with respect to a given logical theory T . Distinguishing features of SMT, as opposed to traditional theorem proving, are that the background theory T need not be finitely or even first-order axiomatizable, and that specialized inference methods are used for each theory of interest. By being theory-specific and restricting their language to certain classes of formulas (such as, typically but not exclusively, quantifier-free formulas), these methods can be implemented into solvers that are more efficient in practice than general-purpose theorem provers.
Details
- Title: Subtitle
- Foundations of Satisfiability Modulo Theories
- Creators
- Cesare Tinelli - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Logic, Language, Information and Computation, pp.58-58
- Publisher
- Springer Berlin Heidelberg; Berlin, Heidelberg
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-642-13824-9_6
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 01/01/2010
- Academic Unit
- Computer Science
- Record Identifier
- 9984410847902771
Metrics
3 Record Views