Logic Journal of IGPL

Logic Journal of IGPL Advance Access originally published online on October 17, 2007
Logic Journal of IGPL 2007 15(5-6):553-575; doi:10.1093/jigpal/jzm040

This Article Abstract Full Text (PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Alert me to new issues of the journal Add to My Personal Archive Download to citation manager Request Permissions Google Scholar Articles by Finger, M. Articles by Gabbay, D. Search for Related Content Social Bookmarking          What's this?

© The Author, 2007. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs

Marcelo Finger

University of Sao Paulo, Brazil. E-mail: mfinger{at}ime.usp.br

Dov Gabbay

King's College, London. E-mail: dg{at}dcs.kcl.ac.uk

This work studies the structure of proofs containing non-analytic cuts in the cut-based system, a sequent inference system in which the cut rule is not eliminable and the only branching rule is the cut. Such sequent system is invertible, leading to the KE-tableau decision method. We study the structure of such proofs, proving the existence of a normal form for them in the form of a comb-tree proof.

We then concentrate on the problem of efficiently computing non-analytic cuts. For that, we study the generalisation of techniques present in many modern theorem provers, namely the techniques of conflict-driven formula learning.

Key Words: Proof Theory • non-analytic cuts • sequent calculus • tableaux.

References

Bachmair L, Ganzinger H. Resolution theorem proving. Handbook of Automated Reasoning—Robinson A, Voronkov A, eds. (2001) volume I. Elsevier Science. 19–99. chapter 2.

Bayardo RJ, Miranker DP. A complexity analysis of space-bounded learning algorithms fofr the constraint satisfaction problem. (1996) In Proceedings of the Thirteenth National Conference on Artificial Intelligence. 508–522.

Boolos George. Don't eliminate cut. Journal of Philosophical Logic (1984) 13:373–378.

Curry HB, Feys R. Combinatory Logics, volume 1. (1958) North Holland.

Carbone Alessandra, Semmes Stephen. A Graphic Apology for Symmetry and Implicitness. In: Oxford Mathematical Monographs. (2000) Oxford University Press.

D'Agostino Marcello. Investigations into the complexity of some propositional calculi. In: Technical Report PRG Technical Monograph 88 (1990) Oxford University Computing Laboratory.

D'Agostino Marcello. Are tableaux an improvement on truth-tables? — Cut-free proofs and bivalence. Journal of Logic, Language and Information (1992) 1:235–252.[CrossRef]

D'Agostino Marcello. Tableau methods for classical propositional logic. In: Handbook of Tableau Methods—D'Agostino Marcello, Gabbay Dov, Haehnle Rainer, Posegga Joachim, eds. (1999) Kluwer. 45–124.

Dechter Rina. Enhancement schemes for constraint processing: Backjumping, learning, and cutset decomposition. Artificial Intelligence (1990) January;41(3):273–312.[CrossRef][ISI]

Davis M, Longemann G, Loveland D. A machine program for theorem proving. Communications of the ACM (1962) 5:394–397.[CrossRef][ISI]

D'Agostino Marcello, Mondadori Marco. The taming of the cut.Classical refutations with analytic cut. Journal of Logic and Computation (1994) 4:285–319.[Abstract/Free Full Text]

Finger Marcelo, Gabbay Dov. Cut and pay. Journal of Logic, Language and Information (2006) October;15(3):195–218.[CrossRef]

Fitting Melvin. Proof Methods for Modal and Intuitionistic Logic. (1983) Reidel.

Goldberg E, Novikov Y. Berkmin: A Fast and Robust SAT Solver. In: In Design Automation and Test in Europe (DATE2002) (2002) 142–149.

Howard W. The formulae-as-types notion of constructuion. In: To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism—Hinchley JR, Seldin JP, eds. (1980) Academic Press. 479–490.

Kleene Stephen C. Mathematical Logic. (1967) John Wiley & Sons.

Massacci Fabio. Single step tableaux for modal logics: Methodology, computations, algorithms. Journal of Automated Reasoning (2000) 24(3):319–364.[CrossRef][ISI]

Martin P-L. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science (1979) volume VI. North Holland. 153–175.

Moskewicz Matthew W, Madigan Conor F, Zhao Ying, Zhang Lintao, Malik Sharad. Chaff: Engineering an Efficient SAT Solver. (2001) In Proceedings of the 38th Design Automation Conference (DAC'01). 530–535.

Marques-Silva JP, Sakallah KA. Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers (1999) 48:506–521.[CrossRef][ISI]

Nieuwenhuis Robert, Oliveras Albert, Tinelli Cesare. Abstract DPLL and abstract DPLL modulo theories. In: volume 3452 of Lecture Notes in Computer Science—Baader F, Voronkov A, eds. (2005) Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'04), Montevideo. Uruguay: Springer. 36–50.

Smullyan Raymond M. Analytic Cut. Journal of Symbolic Logic (1968) 33:560–564.[CrossRef][ISI]

Smullyan Raymond M. First-Order Logic. (1968) Springer-Verlag.

Szabo ME, ed. Collected papers of Gerhard Gentzen. In: Studies in Logic (1969) Amsterdam.

Zhang L, Madigan CF, Moskewitz MH, Malik S. Efficient conflict driven learning in a boolean satisfiability solver. (2001) In International Conference on Computer-Aided Design (ICCAD2001).

CiteULike    Connotea    Del.icio.us    What's this?

This Article Abstract Full Text (PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Alert me to new issues of the journal Add to My Personal Archive Download to citation manager Request Permissions Google Scholar Articles by Finger, M. Articles by Gabbay, D. Search for Related Content Social Bookmarking          What's this?