Abstract
Deduction modulo consists in applying the inference rules of a deductive system modulo a rewrite system over terms and formulæ. This is equivalent to proving within a so-called compatible theory. Conversely, given a first-order theory, one may want to internalize it into a rewrite system that can be used in deduction modulo, in order to get an analytic deductive system for that theory. In a recent paper, we have shown how this can be done in classical logic. In intuitionistic logic, however, we show here not only that this may be impossible, but also that the set of theories that can be transformed into a rewrite system with an analytic sequent calculus modulo is not co-recursively enumerable. We nonetheless propose a procedure to transform a large class of theories into compatible rewrite systems. We then extend this class by working in conservative extensions, in particular using Skolemization.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baader, F., Nipkow, T.: Term Rewriting and all That. Cambridge University Press, Cambridge (1998)
Baaz, M., Iemhoff, R.: On Skolemization in constructive theories. The Journal of Symbolic Logic 73, 969–998 (2008)
Bachmair, L., Dershowitz, N.: Completion for rewriting modulo a congruence. In: Lescanne, P. (ed.) RTA 1987. LNCS, vol. 256, pp. 192–203. Springer, Heidelberg (1987)
Barwise, J. (ed.): Handbook of Mathematical Logic, 4th edn. Elsevier Science Publishers B. V., North-Holland (1985)
Bonichon, R., Hermant, O.: On constructive cut admissibility in deduction modulo. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 33–47. Springer, Heidelberg (2007)
Burel, G.: A first-order representation of pure type systems using superdeduction. In: Pfenning, F. (ed.) LICS, pp. 253–263. IEEE Computer Society, Los Alamitos (2008)
Burel, G.: Automating theories in intuitionistic logic (2009), http://hal.inria.fr/inria-00395934/
Burel, G., Kirchner, C.: Regaining cut admissibility in deduction modulo using abstract completion (2008) (submitted)
Dowek, G.: What is a theory? In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 50–64. Springer, Heidelberg (2002)
Dowek, G.: Confluence as a cut elimination property. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 2–13. Springer, Heidelberg (2003)
Dowek, G., Hardin, T., Kirchner, C.: HOL-λσ an intentional first-order expression of higher-order logic. Mathematical Structures in Computer Science 11, 1–25 (2001)
Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning 31, 33–72 (2003)
Dowek, G., Miquel, A.: Cut elimination for Zermelo’s set theory. Available on authors’ web page (2006)
Dowek, G., Werner, B.: Arithmetic as a theory modulo. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 423–437. Springer, Heidelberg (2005)
Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Computer Science and Technology Series, vol. 5. Harper & Row, New York (1986), http://www.cis.upenn.edu/~jean/gbooks/logic.html , Revised On-Line Version (2003)
Gentzen, G.: Untersuchungen über das logische Schliessen. Mathematische Zeitschrift 39, 176–210, 405–431 (1934)
Girard, J.Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1989)
Hermant, O.: Semantic cut elimination in the intuitionistic sequent calculus. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 221–233. Springer, Heidelberg (2005)
Kirchner, F.: A finite first-order theory of classes. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 188–202. Springer, Heidelberg (2007)
Kleene, S.C.: Mathematical Logic. John Wiley, New York (1967)
Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)
Maehara, S.: Eine Darstellung der intuitionistischen Logik in der klassischen. Nagoya Mathematical Journal 7, 45–64 (1954)
Mints, G.: The Skolem method in intuitionistic calculi. Proc. Steklov Inst. Math. 121, 73–109 (1974)
Mints, G.: A Short Introduction to Intuitionistic Logic. The University series in mathematics. Kluwer Academic Publishers, Dordrecht (2000)
Raths, T., Otten, J., Kreitz, C.: The ILTP problem library for intuitionistic logic, release v1.1. Journal of Automated Reasoning 38, 261–271 (2007), http://www.iltp.de/
von Plato, J.: The axioms of constructive geometry. Annals of Pure and Applied Logic 76, 169–200 (1995)
Waaler, A., Wallen, L.: Tableaux for Intutionistic Logics. In: Handbook of Tableau Methods. Kluwer Academic Publishers, Boston (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Burel, G. (2009). Automating Theories in Intuitionistic Logic. In: Ghilardi, S., Sebastiani, R. (eds) Frontiers of Combining Systems. FroCoS 2009. Lecture Notes in Computer Science(), vol 5749. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04222-5_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-04222-5_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04221-8
Online ISBN: 978-3-642-04222-5
eBook Packages: Computer ScienceComputer Science (R0)