zbMATH — the first resource for mathematics

Resolution is cut-free. (English) Zbl 1197.03010
The paper proves through syntactic translation that the extension of the resolution proof system to deduction modulo is equivalent to the cut-free fragment of the sequent calculus modulo. The resolution method in deduction modulo, called ENAR, is proved to be sound with respect to the cut-free fragment of sequent calculus. However, in order to prove completeness of ENAR with respect to the original sequent calculus, extra assumptions are needed.
Due to the expressiveness of deduction modulo, the results obtained in this paper can be applied to higher-order resolution, Peano arithmetic and Zermelo set theory.

03B35 Mechanization of proofs and logical operations
Full Text: DOI
[1] Andrews, P.B.: Resolution in type theory. J. Symb. Log. 36(3), 414–432 (1971) · Zbl 0231.02038
[2] Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Log. Comput. 2(3), 297–347 (1992) · Zbl 0764.03020
[3] Bonichon, R., Delahaye, D., Doligez, D.: Zenon: an extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) LPAR. Lecture Notes in Computer Science, vol. 4790, pp. 151–165. Springer, New York (2007) · Zbl 1137.68572
[4] Bonichon, R., Hermant, O.: A semantic completeness proof for TaMeD. In: Hermann, M., Voronkov, A. (eds.) LPAR. Lecture Notes in Computer Science, vol. 4246, pp. 167–181. Springer, New York (2006) · Zbl 1165.68451
[5] Bonichon, R., Hermant, O.: On constructive cut admissibility in deduction modulo. In: Altenkirch, T., McBride, C. (eds.) TYPES for Proofs and Programs. Lecture Notes in Computer Science, vol. 4502, pp. 33–47. Springer, New York (2007) · Zbl 1178.03021
[6] Burel, G., Kirchner, C.: Cut elimination in deduction modulo by abstract completion. In: Artëmov, S.N., Nerode, A. (eds.) LFCS. Lecture Notes in Computer Science, vol. 4514, pp. 115–131. Springer, New York (2007) · Zbl 1132.03315
[7] Bonichon, R.: TaMeD: a tableau method for deduction modulo. In: Automated Reasoning: Second International Joint Conference, IJCAR 2004, 4–8 July 2004 · Zbl 1126.68560
[8] Burel, G.: A first-order representation of pure type systems using superdeduction. In: LICS, pp. 253–263. IEEE Computer Society, Los Alamitos (2008)
[9] Dowek, G., Hardin, T., Kirchner, C.: Hol-lambda-sigma: an intentional first-order expression of higher-order logic. Math. Struct. Comput. Sci. 11, 1–25 (2001) · Zbl 0972.03012
[10] Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reason. 31, 33–72 (2003) · Zbl 1049.03011
[11] Dowek, G., Miquel, A.: Cut Elimination for Zermelo’s Set Theory. Manuscript (2007)
[12] de Nivelle, H.: Ordering refinments of resolution. Ph.D. thesis, Technische Universiteit Delft (1995) · Zbl 1044.03506
[13] de Nivelle, H.: Implementing the Clausal Normal Form Transformation with Proof Generation. University of Liverpool, Liverpool (2003)
[14] Degtyarev, A., Voronkov, A.: The inverse method. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 179–272. Elsevier and MIT, New York (2001) · Zbl 0992.03016
[15] Dowek, G., Werner, B.: Proof normalization modulo. J. Symb. Log. 68(4), 1289–1316 (2003) · Zbl 1059.03062
[16] Dowek, G., Werner, B.: Arithmetic as a theory modulo. In: Giesl, J. (ed.) RTA. Lecture Notes in Computer Science, vol. 3467, pp. 423–437. Springer, New York (2005) · Zbl 1078.03046
[17] Dowek, G., Werner, B.: A Constructive Proof of Skolem Theorem for Constructive Logic. Manuscript (2005)
[18] Fitting, M.: First Order Logic and Automated Theorem Proving, 2nd edn. Springer, New York (1996) · Zbl 0848.68101
[19] Gentzen, G.: Untersuchungen über das logische Schliessen. Math. Z. 39, 176–210, 405–431 (1934) · Zbl 0010.14501
[20] Girard, J.-Y.: Linear logic. Theor. Comp. Sci. 50, 1–102 (1987) · Zbl 0625.03037
[21] Herbelin, H.: Séquents qu’on calcule. Ph.D. thesis, Université Paris VII, Janvier (1995)
[22] Hermant, O.: Méthodes sémantiques en déduction modulo. Ph.D. thesis, Université Paris 7 – Denis Diderot (2005)
[23] Hermant, O.: Semantic cut elimination in the intuitionistic sequent calculus. In: Urzyczyn, P. (ed.) Typed Lambda-Calculi and Applications. LNCS, vol. 3461, pp. 221–233. Nara, Japan. Springer, New York (2005) · Zbl 1114.03044
[24] Hermant, O.: Skolemization in various intuitionistic logics. Arch. Math. Log. (2009, in press)
[25] Howe, J.M.: Proof search issues in some non-classical logics. Ph.D. thesis, University of St Andrews (1998). Available as University of St Andrews Research Report CS/99/1
[26] Kleene, S.C.: Permutability of inferences in Gentzen’s calculi LK and LJ. Two papers on the predicate calculus. Mem. Am. Math. Soc. 10, 1–26 (1952) · Zbl 0047.25002
[27] Liang, C., Miller, D.: Focusing and polarization in intuitionistic logic. In: Duparc, J., Henzinger, T.A. (eds.) CSL. Lecture Notes in Computer Science, vol. 4646, pp. 451–465. Springer, New York (2007) · Zbl 1179.03057
[28] Maehara, S.: The predicate calculus with {\(\epsilon\)} symbol. J. Math. Soc. Jpn. 7(4), 323–344 (1955) · Zbl 0067.25003
[29] Maslov, S.Ju.: An inverse method of establishing deducibilities in the classical predicate calculus. Dokl. Akad. Nauk SSSR 159, 17–20 (1964). Reprinted in Siekmann, Wrightson: Automation of reasoning 1: Classical papers on computational logic 1957–1966 (1983)
[30] Mints, G.E.: Skolem’s method of elimination of positive quantifiers in sequential calculi. Sov. Math. Dokl. 7, 861–864 (1966) · Zbl 0186.00501
[31] Mints, G.: Gentzen-type systems and resolution rules, part I: propositional logic. In: Martin-Löf, P., Mints, G. (eds.) Conference on Computer Logic. Lecture Notes in Computer Science, vol. 417, pp. 198–231. Springer, New York (1988) · Zbl 0739.03011
[32] Mints, G.: Gentzen-type systems and resolution rule, part II: predicate logic. In: Oikkonen, J., Väänänen, J. (eds.) Proc. of ASL Summer Meeting, Logic Colloquium ’90, Helsinki, Finland, 15–22 July 1990. Lecture Notes in Logic, vol. 2, pp. 163–190. Springer, New York (1993)
[33] Nerode, A., Shore, R.A.: Logic for Applications. Springer, New York (1993) · Zbl 0842.03003
[34] Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 335–367. Elsevier and MIT, New York (2001) · Zbl 0992.03018
[35] Pfenning, F.: Automated Theorem Proving. Lecture Notes (2004)
[36] Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965) · Zbl 0139.12303
[37] Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT, New York (2001) · Zbl 0964.00020
[38] Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Commun. 15(2), 91–110 (2002) · Zbl 1021.68082
[39] Skolem, T.: Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Verënderlichen mit unendlichem Ausdehnungsbereich. In: Videnskapsselskapets skrifter, I. Matematisk-naturvidenskabelig klasse, vol. 6 (1923) English translation by van Heijenoort in From Frege to Gödel
[40] Schwichtenberg, H., Troelstra, A.S.: Basic Proof Theory. Cambridge University Press, Cambridge (1996) · Zbl 0868.03024
[41] Stuber, J.: A model-based completeness proof of extended narrowing and resolution. In: First International Joint Conference on Automated Reasoning (IJCAR-2001). LNCS, vol. 2083, pp. 195–210. Springer, New York (2001) · Zbl 0988.03016
[42] Szabo, M.E. (ed.): Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundation of Mathematics. North Holland, Amsterdam (1969) · Zbl 0209.30001
[43] Takeuti, G.: Proof Theory, 2nd edn. North Holland, Amsterdam (1987) · Zbl 0609.03019
[44] Tammet, T.: Resolution, inverse method and the sequent calculus. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) Kurt Gödel Colloquium. Lecture Notes in Computer Science, vol. 1289, pp. 65–83. Springer, New York (1997) · Zbl 0888.03004
[45] Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics, An Introduction. North-Holland, Amsterdam (1988) · Zbl 0653.03040
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.