×

zbMATH — the first resource for mathematics

Complexity of translations from resolution to sequent calculus. (English) Zbl 07114850
Summary: Resolution and sequent calculus are two well-known formal proof systems. Their differences make them suitable for distinct tasks. Resolution and its variants are very efficient for automated reasoning and are in fact the theoretical basis of many theorem provers. However, being intentionally machine oriented, the resolution calculus is not as natural for human beings and the input problem needs to be pre-processed to clause normal form. Sequent calculus, on the other hand, is a modular formalism that is useful for analysing meta-properties of various logics and is, therefore, popular among proof theorists. The input problem does not need to be pre-processed, and proofs are more detailed. However, proofs also tend to be larger and more verbose. When the worlds of proof theory and automated theorem proving meet, translations between resolution and sequent calculus are often necessary. In this paper, we compare three translation methods and analyse their complexity.
MSC:
03F07 Structure of proofs
03B35 Mechanization of proofs and logical operations
03F20 Complexity of proofs
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baaz, M. and Leitsch, A. (2011). Methods of Cut-Elimination, Trends in Logic, Springer. · Zbl 1225.03075
[2] Ben-Sasson, E. and Wigderson, A. (2001). Short proofs are narrow – resolution made simple. Journal of ACM48 (2) 149-169. · Zbl 1089.03507
[3] Benzmüller, C., Sultana, N., Paulson, L.C. and Theiß, F. (2015). The higher-order prover Leo-II. Journal of Automated Reasoning55 (4) 389-404.
[4] Bouton, T., De Oliveira, D.C.B., Déharbe, D. and Fontaine, P. (2009). veriT: An open, trustable and efficient SMT-solver. In: Proceedings of the 22nd International Conference on Automated Deduction, Springer-Verlag, 151-156.
[5] Chihani, Z., Miller, D. and Renaud, F. (2017). A semantic framework for proof evidence. Journal of Automated Reasoning59 (3) 287-330. · Zbl 1425.68371
[6] Cook, S. and Reckhow, R. (1974). On the lengths of proofs in the propositional calculus (preliminary version). In: Proceedings of the 6th Annual ACM Symposium on Theory of Computing, ACM, 135-148. · Zbl 0375.02004
[7] Degtyarev, A. and Voronkov, A. (2001). The inverse method. In: Robinson, J. A. and Voronkov, A. (eds.) Handbook of Automated Reasoning, Elsevier and MIT Press, 179-272. · Zbl 0992.03016
[8] Dunchev, T., Leitsch, A., Libal, T., Weller, D. and Woltzenlogel Paleo, B. (2010). System description: The proof transformation system CERES. In: Giesl, J. and Hähnle, R. (eds.) Automated Reasoning, Springer, Berlin, Heidelberg, 427-433. · Zbl 1291.68338
[9] Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S. and Zivota, S. (2016). System description: GAPT 2.0. In: Proceedings of the 8th International Joint Conference on Automated Reasoning, vol. 9706, Springer-Verlag, New York, Inc., New York, NY, USA, 293-301. · Zbl 06623268
[10] Gentzen, G. (1969). Investigations into logical deductions. In: Szabo, M. E. (ed.) The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam, 68-131.
[11] Hermant, O., Resolution is cut-free, Journal of Automated Reasoning, 44, 3, 245-276, (2010) · Zbl 1197.03010
[12] Hetzl, S., Leitsch, A., Reis, G. and Weller, D. (2014). Algorithmic introduction of quantified cuts. Theoretical Computer Science549, 1-16. · Zbl 1393.03050
[13] Hetzl, S., Leitsch, A., Weller, D. and Woltzenlogel Paleo, B. (2008). Herbrand sequent extraction. In: Proceedings of the 9th AISC International Conference, 15th Calculemas Symposium, and 7th International MKM Conference on Intelligent Computer Mathematics 462-477. · Zbl 1166.68347
[14] Hetzl, S., Libal, T., Riener, M. and Rukhaia, M. (2013). Understanding resolution proofs through Herbrand’s theorem. In: Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods: 22nd International Conference, TABLEAUX 2013, Springer, 157-171. · Zbl 1401.03038
[15] Itegulov, D., Slaney, J. and Woltzenlogel Paleo, B. (2017). Scavenger 0.1: A theorem prover based on conflict resolution. In: De Moura, L. (ed.) Automated Deduction - CADE 26, Springer International Publishing, Cham, 344-356. · Zbl 06778413
[16] Korovin, K. (2008). iProver - An instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P. and Dowek, G. (eds.) Automated Reasoning, Springer, Berlin, Heidelberg, 292-298. · Zbl 1165.68462
[17] Kovács, L. and Voronkov, A. (2013). First-order theorem proving and vampire, In: Sharygina, N. and Veith, H. (eds.) Computer Aided Verification, Springer, Berlin, Heidelberg, 1-35.
[18] Maslov, S.J. (1964). An Inverse Method of Establishing Deducibilities in the Classical Predicate Calculus, Reprinted in Siekmann, Wrightson: Automation of reasoning 1: classical papers on computational logic 1957-1966, 1983, pp. 17-20.
[19] Mccune, W. (2005-2010). Prover9 and Mace4. Available at: http://www.cs.unm.edu/mccune/prover9/.
[20] Miller, D. (2013). Foundational proof certificates: Making proof universal and permanent. In: Proceedings of the 8th ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice 1-2.
[21] Miller, D. (2017a). Expansion proofs. In: Woltzenlogel Paleo, B. (ed.) Towards an Encyclopaedia of Proof Systems, 1st edn., College Publications, London, UK, 18.
[22] Miller, D. (2017b). Focused LK. In: Woltzenlogel Paleo, B. (ed.) Towards an Encyclopaedia of Proof Systems, 1st edn., College Publications, London, UK, 75-76.
[23] Mints, G. (1990). Gentzen-type systems and resolution rules part I propositional logic, In: Martin-Löf, P. and Mints, G. (eds.) Proceedings of the International Conference on Computer Logic Tallinn, USSR, December 12-16, 1988, Springer, Berlin, Heidelberg, 198-231. · Zbl 0739.03011
[24] Mints, G. (1993). Gentzen-type systems and resolution rule, part II: Predicate logic, In: Oikkonen, J. and Väänänen, J. (eds.) Proceedings of ASL Summer Meeting, Logic Colloquium, Helsinki, Finland, 15-22 July 1990, Lecture Notes in Logic, vol. 2, Springer-Verlag, 163-190.
[25] Orevkov, V. P., Lower bounds for increasing complexity of derivations after cut elimination, Journal of Mathematical Sciences, 20, 4, 2337-2350, (1982) · Zbl 0492.03023
[26] Reis, G. (2015). Importing SMT and Connection proofs as expansion trees, In: Proceedings 4th Workshop Proof eXchange for Theorem Proving, 3-10.
[27] Robinson, J. A., A machine-oriented logic based on the resolution principle, Journal of the ACM, 12, 1, 23-41, (1965) · Zbl 0139.12303
[28] Schulz, S. (2013). System description: E 1.8, In: Mcmillan, K., Middeldorp, A. and Voronkov, A. (eds.) Proceedings of the 19th Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science, vol. 8312, Springer, 735-743. · Zbl 1407.68442
[29] Statman, R. (1979). Lower bounds on Herbrand’s theorem. In: Proceedings of the American Mathematical Society 104-107. · Zbl 0411.03048
[30] Urquhart, A., The complexity of propositional proofs, Bulletin of Symbolic Logic, 1, 4, 425-467, (1995) · Zbl 0845.03025
[31] Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M. and Wischnewski, P. (2009). SPASS version 3.5, In: Schmidt, R. A. (ed.) Automated Deduction - CADE-22, Springer, Berlin, Heidelberg, 140-145.
[32] Woltzenlogel Paleo, B. (2008). Herbrand Sequent Extraction, M.Sc. Thesis, VDM-Verlag, Saarbrücken, Germany.
[33] Woltzenlogel Paleo, B. (2010). Atomic cut introduction by resolution: Proof structuring and compression. In: Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Revised Selected Papers, 463-480. · Zbl 1253.03085
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.