Encoding first order proofs in SMT. (English) Zbl 1277.03006
Krstić, Sava (ed.) et al., Proceedings of the 5th international workshop on satisfiability modulo theories (SMT 2007), Berlin, Germany, July 1–2, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 198, No. 2, 71-84 (2008).
Summary: We present a method for encoding first-order proofs in SMT. Our implementation, called ChewTPTP-SMT, transforms a set of first-order clauses into a propositional encoding (modulo theories) of the existence of a rigid first-order connection tableau and the satisfiability of unification constraints, which is then fed to Yices. For the unification constraints, terms are represented as recursive datatypes, and unification constraints are equations on terms. The finiteness of the tableau is encoded by linear real arithmetic inequalities.{
}We compare our implementation with our previous implementation ChewTPTP-SAT, encoding rigid connection tableau in SAT, and show that for Horn clauses many fewer propositional clauses are generated by ChewTPTP-SMT, and ChewTPTP-SMT is much faster than ChewTPTP-SAT. This is not the case for our non-Horn clause encoding. We explain this, and we conjecture a rule of thumb on when to use theories in encoding a problem.
For the entire collection see [Zbl 1276.68020].
For the entire collection see [Zbl 1276.68020].
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
References:
| [1] | Andrews, P. B., Theorem Proving via General Matings, Journal of the Association for Computing Machinery, 28, 2, 193-214 (1981) · Zbl 0456.68119 |
| [2] | Bell, J. L.; Slomson, A. B., Models and Ultraproducts, An Introduction (1969), Dover · Zbl 0179.31402 |
| [3] | Chang, C.; Lee, C. R., Symbolic Logic and Mechanical Theorem Proving (1973), Academic Press: Academic Press New York and London · Zbl 0263.68046 |
| [4] | Davis, M.; Logemann, D.; Loveland, D., A Machine Program For Theorem Proving, Communications of the ACM, 5, 7, 394-397 (1962) · Zbl 0217.54002 |
| [5] | Delaune S., Lin H. and Lynch C. [2007], Protocol Verification Via Rigid/Flexible Resolution, submitted; Delaune S., Lin H. and Lynch C. [2007], Protocol Verification Via Rigid/Flexible Resolution, submitted · Zbl 1137.94342 |
| [6] | Deshane, T.; Hu, W.; Jablonski, P.; Lin, H.; Lynch, C.; McGregor, R. E., (CADE. CADE, Lecture Notes in Computer Science, Vol. 4603 (2007), Springer), 476-491 · Zbl 1213.68569 |
| [7] | Dutertre, B.; deMoura, L., Yices |
| [8] | Eén N. and Sörensson N. [2003], An Extensible Sat-Solver, In SAT, pp. 502-518; Eén N. and Sörensson N. [2003], An Extensible Sat-Solver, In SAT, pp. 502-518 |
| [9] | Goubault, J., The Complexity of Resource-Bounded First-Order Classical Logic, (Proceedings of the 11th Annual Symposium on Theoretical Aspects of Computer Science. Proceedings of the 11th Annual Symposium on Theoretical Aspects of Computer Science, Lecture Notes In Computer Science, Vol. 775 (1994), Springer-Verlag), 59-70 · Zbl 0941.03547 |
| [10] | Hähnle, R., Tableaux and Related Methods, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning, Vol. 1 (2001), Elsevier Science), 101-177, chapter 3 · Zbl 1011.68125 |
| [11] | Letz, R.; Gernot, S., Model Elimination and Connection Tableau Procedures, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning, Vol. 2 (2001), Elsevier Science), 2015-2113, chapter 28 · Zbl 1011.68130 |
| [12] | Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T), Journal of the ACM, 53, 6, 937-977 (2006), November 2006 · Zbl 1326.68164 |
| [13] | Sutcliffe, G.; Suttner, C. B., The TPTP Problem Library: CNF Release v1.2.1, Journal of Automated Reasoning, 21, 2, 177-203 (1998) · Zbl 0910.68197 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
