Satisfiability modulo bounded checking. (English) Zbl 1494.68283
de Moura, Leonardo (ed.), Automated deduction – CADE 26. 26th international conference on automated deduction, Gothenburg, Sweden, August 6–11, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10395, 114-129 (2017).
Summary: We describe a new approach to find models for a computational higher-order logic with datatypes. The goal is to find counter-examples for conjectures stated in proof assistants. The technique builds on narrowing
but relies on a tight integration with a SAT solver to analyze conflicts precisely, eliminate sets of choices that lead to failures, and sometimes prove unsatisfiability. The architecture is reminiscent of that of an SMT solver. We present the rules of the calculus, an implementation, and some promising experimental results.
For the entire collection see [Zbl 1369.68037].
For the entire collection see [Zbl 1369.68037].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 03B16 | Higher-order logic |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
