Journal article
Proof Checking Technology for Satisfiability Modulo Theories
Electronic notes in theoretical computer science, Vol.228(C), pp.121-133
01/05/2009
DOI: 10.1016/j.entcs.2008.12.121
Abstract
A common proof format for solvers for Satisfiability Modulo Theories (SMT) is proposed, based on the Edinburgh Logical Framework (LF). Two problems arise: checking very large proofs, and keeping proofs compact in the presence of complex side conditions on rules. Incremental checking combines parsing and proof checking in a single step, to avoid building in-memory representations of proof subterms. LF with Side Conditions (LFSC) extends LF to allow side conditions to be expressed using a simple first-order functional programming language. Experimental data with an implementation show very good proof checking times and memory usage on benchmarks including the important example of resolution inferences.
Details
- Title: Subtitle
- Proof Checking Technology for Satisfiability Modulo Theories
- Creators
- Aaron Stump - Washington University in St. Louis
- Resource Type
- Journal article
- Publication Details
- Electronic notes in theoretical computer science, Vol.228(C), pp.121-133
- DOI
- 10.1016/j.entcs.2008.12.121
- ISSN
- 1571-0661
- eISSN
- 1571-0661
- Publisher
- Elsevier B.V
- Grant note
- DOI: 10.13039/100000001, name: National Science Foundation
- Language
- English
- Date published
- 01/05/2009
- Academic Unit
- Computer Science
- Record Identifier
- 9984259425902771
Metrics
6 Record Views