article

Resolution is Cut-Free

Author:

Olivier HermantAuthors Info & Claims

Journal of Automated Reasoning, Volume 44, Issue 3

Pages 245 - 276

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

Published: 01 March 2010 Publication History

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.

References

[1]

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

[2]

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

[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).

[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).

[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).

[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).

[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).

[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).

Digital Library

[10]

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

[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).

[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).

[15]

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

[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).

[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).

[19]

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

[20]

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

Digital Library

[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).

[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).

[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).

[28]

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

[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).

[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).

[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).

[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).

[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).

Digital Library

[37]

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

[38]

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

Digital Library

[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).

[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).

[42]

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

[43]

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

[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).

[45]

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

Cited By

Burel G(2020)Linking Focusing and Resolution with SelectionACM Transactions on Computational Logic10.1145/337327621:3(1-30)Online publication date: 20-Feb-2020
https://dl.acm.org/doi/10.1145/3373276
Burel GBury GCauderlier RDelahaye DHalmagrand PHermant O(2019)First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets PracticeJournal of Automated Reasoning10.1007/s10817-019-09533-z64:6(1001-1050)Online publication date: 23-Sep-2019
https://dl.acm.org/doi/10.1007/s10817-019-09533-z
Bensaid HCaferra RPeltier N(2010)I-terms in ordered resolution and superposition calculiProceedings of the 10th ASIC and 9th MKM international conference, and 17th Calculemus conference on Intelligent computer mathematics10.5555/1894483.1894488(19-33)Online publication date: 5-Jul-2010
https://dl.acm.org/doi/10.5555/1894483.1894488
Show More Cited By

Resolution is Cut-Free

Recommendations

Theorem Proving Modulo
Abstract
Deduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated theorem proving, is of general interest because it permits one to separate ...
Andrews Skolemization May Shorten Resolution Proofs Non-elementarily
Logical Foundations of Computer Science
Abstract
In this paper we construct a sequence of formulas $F_{1}, F_{2}, \dots$ with resolution proofs $π_{1}, π_{2}, \dots$ of these formulas after Andrews Skolemization, such that there is no elementary bound in the complexity of $π_{1}, π_{2}, \dots$ of resolution proofs $π_{1}^{'}, π_{2}^{'}, \dots$ after ... $^{}$
Semantic cut elimination in the intuitionistic sequent calculus
TLCA'05: Proceedings of the 7th international conference on Typed Lambda Calculi and Applications

Cut elimination is a central result of the proof theory. This paper proposes a new approach for proving the theorem for Gentzen's intuitionistic sequent calculus LJ, that relies on completeness of the cut-free calculus with respect to Kripke Models. The ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Automated Reasoning

Journal of Automated Reasoning Volume 44, Issue 3

March 2010

125 pages

ISSN:0168-7433

Issue’s Table of Contents

Copyright © Copyright © 2010 Springer Science+Business Media B.V.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 March 2010

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Burel G(2020)Linking Focusing and Resolution with SelectionACM Transactions on Computational Logic10.1145/337327621:3(1-30)Online publication date: 20-Feb-2020
https://dl.acm.org/doi/10.1145/3373276
Burel GBury GCauderlier RDelahaye DHalmagrand PHermant O(2019)First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets PracticeJournal of Automated Reasoning10.1007/s10817-019-09533-z64:6(1001-1050)Online publication date: 23-Sep-2019
https://dl.acm.org/doi/10.1007/s10817-019-09533-z
Bensaid HCaferra RPeltier N(2010)I-terms in ordered resolution and superposition calculiProceedings of the 10th ASIC and 9th MKM international conference, and 17th Calculemus conference on Intelligent computer mathematics10.5555/1894483.1894488(19-33)Online publication date: 5-Jul-2010
https://dl.acm.org/doi/10.5555/1894483.1894488
Burel G(2010)Embedding deduction modulo into a proverProceedings of the 24th international conference/19th annual conference on Computer science logic10.5555/1887459.1887476(155-169)Online publication date: 23-Aug-2010
https://dl.acm.org/doi/10.5555/1887459.1887476

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents