Logic of proofs. (English) Zbl 0796.03029
Summary: Individual proofs are integrated into provability logic. Systems of axioms for a logic with operators “\(A\) is provable” and “\(p\) is a proof of \(A\)” are introduced, provided with Kripke semantics and decision procedure. Completeness theorems with respect to the arithmetical interpretation are proved.
Keywords:
completeness with respect to the arithmetical interpretation; provability logic; Kripke semantics; decision procedureReferences:
| [1] | Artëmov, S., Logic of Proofs, (Rapport de Recherche R.R. LIRMM No. 92-078 (Dec. 1992), CNRS-Laboratoire d’Informatique, de Robotique et de Microelectronique de Montpellier) · Zbl 1133.03038 |
| [2] | Artëmov, S., Logic of functional proofs, (Tech. Rep. 93-47 (July 1993), Mathematical Sciences Institute, Cornell University) · Zbl 1079.03053 |
| [3] | Artëmov, S.; Straβen, T., The basic logic of proofs, (Börger, E.; Jäger, G.; Kleine Büning, H.; Richter, M., Computer Science Logic. Computer Science Logic, 6th Workshop, CSL’92, San Miniato, Italy, Oct. 1992. Computer Science Logic. Computer Science Logic, 6th Workshop, CSL’92, San Miniato, Italy, Oct. 1992, Lecture Notes in Computer Science, 702 (1993), Springer: Springer Berlin), 14-28 · Zbl 0802.03012 |
| [4] | Artëmov, S.; Straβen, T., Functionality in the basic logic of proofs, (Tech. Rep. IAM 92-004 (Jan. 1993), Department for Computer Science, University of Berne: Department for Computer Science, University of Berne Switzerland) |
| [5] | Boolos, G., The Unprovability of Consistency: An Essay in Modal Logic (1979), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0409.03009 |
| [6] | Guaspary, D.; Solovay, R. M., Rosser sentences, Ann. Math. Logic, 16, 81-99 (1979) · Zbl 0426.03062 |
| [7] | Hughes, G. E.; Cresswell, M. J., A Companion to Modal Logic (1984), Methuen: Methuen London · Zbl 0625.03005 |
| [8] | Lassez, J.; Maher, M.; Marriott, K., Unification revisited, (Minker, J., Foundations of Deductive Databases and Logic Programming (1987), Morgan Kaufmann: Morgan Kaufmann Los Altos, CA), 587-625, Ch. 15 · Zbl 0645.68046 |
| [9] | Smoryński, C., Self-reference and Modal Logic (1985), Springer: Springer New York · Zbl 0596.03001 |
| [10] | Solovay, R. M., Provability interpretations of modal logic, Israel J. Math., 25, 287-304 (1976) · Zbl 0352.02019 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
