Abstract
We present the CoRe calculus for contextual reasoning which supports reasoning directly at the assertion level, where proof steps are justified in terms of applications of definitions, lemmas, theorems, or hypotheses (collectively called “assertions”) and which is an established basis to generate proof presentations in natural language. The calculus comprises a uniform notion of a logical context of subformulas as well as replacement rules available in a logical context. Replacement rules operationalize assertion level proof steps and technically are generalized resolution and paramodulation rules, which in turn should suit the implementation of automatic reasoning procedures.
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
Andreoli, J.-M.: Focusing and proof construction. Annals of Pure and Applied Logic 107(1), 131–163 (2000)
Andrews, P.B.: General models, descriptions, and choice in type theory. The Journal of Symbolic Logic 37(2), 385–397 (1972)
Autexier, S.: Hierarchical Contextual Reasoning. PhD thesis, Computer Science Department, Saarland University, Saarbrücken, Germany (2003)
Barendregt, H.: The λ-Calculus - Its Syntax and Semantics. North-Holland, Amsterdam (1984)
Benzmüller, C., Brown, C.E., Kohlhase, M.: Semantic Techniques for Higher-Order Cut-Elimination. SEKI Tech. Report SR-2004-07, Saarland University (2004)
Brünnler, K.: Deep Inference and Symmetry in Classical Proofs. Logos (2004)
Bundy, A.: The use of explicit plans to guide inductive proofs. DAI Research Report 349, Department of Artificial Intelligence, University of Edinburgh (1987)
Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Rapport de Recherche 3400, INRIA (April 1998)
Fitting, M.: Tableau methods of proof for modal logics. Notre Dame Journal of Formal Logic, XIII, 237–247 (1972)
Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 335–349. Springer, Heidelberg (2003)
Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF – A mechanised logic of computation. LNCS, vol. 78. Springer, Heidelberg (1979)
Henkin, L.: Completeness in the theory of types. The Journal of Symbolic Logic 15, 81–91 (1950)
Huang, X.: Human Oriented Proof Presentation: A Reconstructive Approach. In: Augustin, S. (ed.) DISKI. Infix, Germany, vol. 112 (1996)
Murray, N.V., Rosenthal, E.: Inference with path resolution and semantic graphs. Journal of the Association of Computing Machinery 34(2), 225–254 (1987)
Pfenning, F.: Proof Transformation in Higher-Order Logic. Phd thesis, Carnegie Mellon University (1987)
Schütte, K.: Proof Theory (Originaltitel: Beweistheorie). In: Die Grundlehren der mathematischen Wissenschaften, vol. 255, Springer, Heidelberg (1977)
Smullyan, R.M.: First-Order Logic. In: Ergebnisse der Mathematik, vol. 43, Springer, Berlin (1968)
Wallen, L.: Automated proof search in non-classical logics: efficient matrix proof methods for modal and intuitionistic logics. series in AI. MIT Press, Cambridge (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Autexier, S. (2005). The CoRe Calculus. In: Nieuwenhuis, R. (eds) Automated Deduction – CADE-20. CADE 2005. Lecture Notes in Computer Science(), vol 3632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11532231_7
Download citation
DOI: https://doi.org/10.1007/11532231_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28005-7
Online ISBN: 978-3-540-31864-4
eBook Packages: Computer ScienceComputer Science (R0)