Conference proceeding
Towards an SMT proof format
Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on bit-precise reasoning, pp.27-32
SMT '08/BPR '08
07/07/2008
DOI: 10.1145/1512464.1512470
Abstract
The Edinburgh Logical Framework (LF) extended to support side condition code (LFSC) is advocated as a foundation for a proof format for SMT. The flexibility of the framework is demonstrated by example encoded inference rules, notably propositional resolution. Preliminary empirical results obtained with a SAT solver producing proofs in LFSC format are presented.
Details
- Title: Subtitle
- Towards an SMT proof format
- Creators
- Aaron Stump - Washington University in St. LouisDuckki Oe - Washington University in St. Louis
- Resource Type
- Conference proceeding
- Publication Details
- Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on bit-precise reasoning, pp.27-32
- Series
- SMT '08/BPR '08
- DOI
- 10.1145/1512464.1512470
- Publisher
- ACM
- Grant note
- DOI: 10.13039/100000001, name: National Science Foundation, award: 551697
- Language
- English
- Date published
- 07/07/2008
- Academic Unit
- Computer Science
- Record Identifier
- 9984259490202771
Metrics
14 Record Views