Back to Search
Start Over
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs
- Source :
- Journal of Automated Reasoning. 66:43-91
- Publication Year :
- 2021
- Publisher :
- Springer Science and Business Media LLC, 2021.
-
Abstract
- Search-based satisfiability procedures try to build a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. Conflict-driven procedures perform non-trivial inferences only when resolving conflicts between formulæ and assignments representing the candidate model. CDSAT (Conflict-Driven SATisfiability) is a method for conflict-driven reasoning in unions of theories. It combines inference systems for individual theories as theory modules within a solver for the union of the theories. This article augments CDSAT with a more general lemma learning capability and with proof generation. Furthermore, theory modules for several theories of practical interest are shown to fulfill the requirements for completeness and termination of CDSAT. Proof generation is accomplished by a proof-carrying version of the CDSAT transition system that produces proof objects in memory accommodating multiple proof formats. Alternatively, one can apply to CDSAT the LCF approach to proofs from interactive theorem proving, by defining a kernel of reasoning primitives that guarantees the correctness by construction of CDSAT proofs.
- Subjects :
- Computer science
Satisfiability modulo assignment
020207 software engineering
Lemma learning
0102 computer and information sciences
02 engineering and technology
Proof generation
Mathematical proof
01 natural sciences
Lemma learning, Proof generation, Satisfiability modulo theories, Satisfiability modulo assignment
Satisfiability
Algebra
Computational Theory and Mathematics
010201 computation theory & mathematics
Artificial Intelligence
Satisfiability modulo theories
0202 electrical engineering, electronic engineering, information engineering
Software
Subjects
Details
- ISSN :
- 15730670 and 01687433
- Volume :
- 66
- Database :
- OpenAIRE
- Journal :
- Journal of Automated Reasoning
- Accession number :
- edsair.doi.dedup.....e35bdc75085c114ab1650207775fff92