Abstract
We establish a connection between the geometric methods developed in the combinatorial theory of small cancellation and the propositional resolution calculus. We define a precise correspondence between resolution proofs in logic and diagrams in small cancellation theory, and as a consequence, we derive that a resolution proof is a 2-dimensional process. The isoperimetric function defined on diagrams corresponds to the length of resolution proofs.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Blake, A., Canonical Expressions in Boolean Algebra, PhD thesis, University of Chicago, 1937.
Buss, S. R., and G. Turan, ‘Resolution proofs of generalized pigeon-hole principles’, Theoretical Computer Science, 62: 311–317, 1988.
Carbone, A., ‘Streams and strings of formal proofs’, Theoretical Computer Science. To appear.
Carbone, A., and S. Semmes, A Graphic Apology for Symmetry and Implicitness. Mathematical Monographs, Oxford University Press, 2000.
Colmerauer, A., H. KANOUI, P. Roussel, and R. Pasero, Un système de communication homme-machine en français, Groupe de Recherche en Intelligence Artiflcielle, Université d'Aix-Marseille, 1973.
Davis, M., and H. Putnam, ‘A computing procedure for quantification theory’, Journal of ACM, 7: 201–215, 1960.
Epstein, D.B.A, J.W.Cannon, D.F.Holt, S.V.F. Levy, M.S.Paterson, and W.P.Thurston, Word Processing in Groups. Jones and Bartlett Publishers, Boston and London, 1992.
Gilmore, P.C., ‘A proof method for quantification theory’, IBM Journal Res. Develop., 4: 28–35, 1960.
Guba, V., and M. Sapir, Diagram Groups, Memoirs of the American Mathematical Society, number 620, volume 130, 1996.
Haken, A., ‘The intractability of resolution’, Theoretical Computer Science, 39: 297–308, 1985.
Herbrand, J., Logical Writings, W.D. Goldfarb (ed.), Harvard University Press, 1971.
Van Kampen, E.R., ‘On some lemmas in the theory of groups’, American Journal of Mathematics, 55: 268–273, 1933.
Kowalski, R.A., ‘Predicate logic as a programming language’, IFIP 74, 569–574, 1974.
Krajicek, J., Bounded Arithmetic, Propositional Logic, and Complexity Theory. Encyclopedia of Mathematics and its Applications 60, Cambridge University Press, Cambridge, 1995.
Krajicek, J., ‘Dehn functions and length of proofs’, Internatinal Journal of Algebra and Computation, 13: 527–542, 2001.
Leitsch, A., The Resolution Calculus. Texts in Theoretical Computer Science, Springer, 1997.
Lyndon, R.C., ‘On Dehn's algorithm’, Math. Annalen, 166: 208–228, 1966.
Lyndon, R.C., and P.E. Schupp, Combinatorial Group Theory. Ergebnisse der Mathematik und iher Grenzgebiete 89, A Series of Modern Surveys in Mathematics, Springer- Verlag, 1977.
Prawitz, D., ‘An improved proof procedure’, Theoria, 26: 102–139, 1960.
Robinson, J.A., ‘A machine-oriented logic based on the resolution principle’, Journal of ACM, 1: 23–41, 1965.
Strebel, R., ‘Small cancellation groups’, in Sur les groupes hyperbolique d'apres Mikhael Gromov, E. Ghys and P. de la Harpe (eds.), Progress in Mathematics, volume 83, Birkhauser, Boston, 1990.
Tseitin, G.S., ‘Complexity of a derivation in the Propositional calculus’, Zap. Nauchn. Sem. Leningrad Otd. Mat. Inst. Akad. Nauk SSSR, 8: 234–259, 1968. Also appeared in Studies in Mathematics and Mathematical Logic, Part II, A.O. Slissenko, (ed.,) 115–125.
Urquhart, A., ‘Hard examples for resolution’, Journal of the Association for Computing Machinery, 34(1):209–219, 1987.
Weinbaum, C.M., ‘Visualizing the word problem with an application to sixth group’, Pacific Journal of Mathematics, 16: 557–578, 1966.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Carbone, A. Group Cancellation and Resolution. Stud Logica 82, 73–93 (2006). https://doi.org/10.1007/s11225-006-6606-3
Issue Date:
DOI: https://doi.org/10.1007/s11225-006-6606-3