Abstract
Deduction modulo is a way to express a theory using computation rules instead of axioms.We present in this paper an extension of deduction modulo, called Polarized deduction modulo, where some rules can only be used at positive occurrences, while others can only be used at negative ones.We show that all theories in propositional calculus can be expressed in this framework and that cuts can always be eliminated with such theories.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
S.C. Bailin.A normalization theorem for set theory. The Journal of Symbolic Logic, 53, 3, 1988, pp.673–695.
M. Crabbé.Non-normalisation de la théorie de Zermelo. Manuscript, 1974.
M. Crabbé.Stratification and cut-elimination. The Journal of Symbolic Logic, 56, 1991, pp.213–226.
G. Do wek. Axioms vs. rewrite rules: from completeness to cut elimination. H. Kirchner and Ch. Ringeissen (Eds.), Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence 1794, Springer-Verlag, 2000, pp.62–72.
G.Do wek.About folding-unfolding cuts and cuts modulo. Journal of Logic and Computation 11, 3, 2001, pp.419–429.
G.Do wek.Confluence as a cut elimination property. Workshop on Logic, Language, Information and Computation, 2001.
G.Do wek, Th. Hardin, and C. Kirchner.Theorem proving modulo. Journal of Automated Reasoning (to appear). Rapport de Recherche INRIA 3400, 1998.
G. Dowek and B. Werner.Proof normalization modulo. Types for proofs and programs, T. Altenkirch, W. Naraschewski, and B. Rues (Eds.), Lecture Notes in Computer Science 1657, Springer-Verlag, 1999, pp.62–77. Rapport de Recherche 3542, INRIA, 1998.
J. Ekman. Normal proofs in set theory. Doctoral thesis, Chalmers University of Technology and University of Göteborg, 1994.
L. Hallnäs. On normalization of proofs in set theory. Doctoral thesis, University of Stockholm, 1983.
L. Hallnäs and P. Schroeder-Heister.A proof-theoretic approach to logic programming. I. Clauses as rules. Journal of Logic and Computation 1, 2, 1990, pp.261–283. II. Programs as definitions. Journal of Logic and Computation 1, 5, 1991, pp.635–660.
D.E. Knuth and P.B. Bendix.Simple word problems in universal algebras. J. Leech (Ed.), Computational Problems in Abstract Algebra, Pergamon Press, 1970, pp.263–297.
R. McDowell and D. Miller.Cut-Elimination for a logic with definitions and induction. Theoretical Computer Science 232, 2000, pp.91–119.
S. Negri and J. Von Plato.Cut elimination in the presence of axioms. The Bulletin of Symbolic Logic, 4, 4, 1998, pp.418–435.
D. Prawitz. Natural deduction, a proof-theoretical study. Almqvist & Wiksell, 1965.
P. Schroeder-Heister. Cut elimination in logics with definitional reflection. D. Pearce and H. Wansing (Eds.), Nonclassical Logics and Information Processing, Lecture Notes in Computer Science 619, Springer-Verlag, 1992, pp.146–171.
P. Schroeder-Heister.Rules of definitional reflection. Logic in Computer Science, 1993, pp.222–232.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dowek, G. (2002). What Is a Theory?. In: Alt, H., Ferreira, A. (eds) STACS 2002. STACS 2002. Lecture Notes in Computer Science, vol 2285. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45841-7_3
Download citation
DOI: https://doi.org/10.1007/3-540-45841-7_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43283-8
Online ISBN: 978-3-540-45841-8
eBook Packages: Springer Book Archive