Resolution is Cut-Free | Journal of Automated Reasoning Skip to main content
Springer Nature Link
Log in

Resolution is Cut-Free

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

In this article, we show that the extension of the resolution proof system to deduction modulo is equivalent to the cut-free fragment of the sequent calculus modulo. The result is obtained through a syntactic translation, without using any cut-elimination procedure. Additionally, we show Skolem theorem and inversion/focusing results. Thanks to the expressiveness of deduction modulo, all these results also apply to the cases of higher-order resolution, Peano’s arithmetic and Gentzen’s LK.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Andrews, P.B.: Resolution in type theory. J. Symb. Log. 36(3), 414–432 (1971)

    Article  MATH  Google Scholar 

  2. Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Log. Comput. 2(3), 297–347 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Google Scholar 

  7. Bonichon, R.: TaMeD: a tableau method for deduction modulo. In: Automated Reasoning: Second International Joint Conference, IJCAR 2004, 4–8 July 2004

  8. Burel, G.: A first-order representation of pure type systems using superdeduction. In: LICS, pp. 253–263. IEEE Computer Society, Los Alamitos (2008)

    Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  10. Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reason. 31, 33–72 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  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)

  13. de Nivelle, H.: Implementing the Clausal Normal Form Transformation with Proof Generation. University of Liverpool, Liverpool (2003)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  15. Dowek, G., Werner, B.: Proof normalization modulo. J. Symb. Log. 68(4), 1289–1316 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  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)

    Google Scholar 

  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)

    MATH  Google Scholar 

  19. Gentzen, G.: Untersuchungen über das logische Schliessen. Math. Z. 39, 176–210, 405–431 (1934)

    Article  MathSciNet  Google Scholar 

  20. Girard, J.-Y.: Linear logic. Theor. Comp. Sci. 50, 1–102 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  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)

    Google Scholar 

  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)

    MATH  MathSciNet  Google Scholar 

  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)

    Google Scholar 

  28. Maehara, S.: The predicate calculus with ε symbol. J. Math. Soc. Jpn. 7(4), 323–344 (1955)

    Article  MATH  MathSciNet  Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  33. Nerode, A., Shore, R.A.: Logic for Applications. Springer, New York (1993)

    MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  37. Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT, New York (2001)

    Google Scholar 

  38. Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Commun. 15(2), 91–110 (2002)

    MATH  Google Scholar 

  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)

    MATH  Google Scholar 

  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)

    Google Scholar 

  42. Szabo, M.E. (ed.): Collected Papers of Gerhard Gentzen. Studies in Logic and the Foundation of Mathematics. North Holland, Amsterdam (1969)

    Google Scholar 

  43. Takeuti, G.: Proof Theory, 2nd edn. North Holland, Amsterdam (1987)

    MATH  Google Scholar 

  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)

    Google Scholar 

  45. Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics, An Introduction. North-Holland, Amsterdam (1988)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. Sistemas Informáticos y Computación, Univ. Complutense de Madrid, C/ Prof. José G. Santesmases, s/n, Ciudad Universitaria, 28040, Madrid, Spain

    Olivier Hermant

  2. ISEP, 28 rue N.-D. des Champs, 75006, Paris, France

    Olivier Hermant

Authors
  1. Olivier Hermant
    View author publications

    You can also search for this author inPubMed Google Scholar

Corresponding author

Correspondence to Olivier Hermant.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Hermant, O. Resolution is Cut-Free. J Autom Reasoning 44, 245–276 (2010). https://doi.org/10.1007/s10817-009-9153-6

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-009-9153-6

Keywords