Annals of Pure and Applied Logic 113 (1-3):181-206 (2001)

The logic of single-conclusion proofs () is introduced. It combines the verification property of proofs with the single valuedness of proof predicate and describes the operations on proofs induced by modus ponens rule and proof checking. It is proved that is decidable, sound and complete with respect to arithmetical proof interpretations based on single-valued proof predicates. The application to arithmetical inference rules specification and -admissibility testing is considered. We show that the provability in gives the complete admissibility test for the rules which can be specified by schemes in -language. The test is supplied with the ground proof extraction algorithm which eliminates the admissible rules from a -proof by utilizing the information from the corresponding -proofs
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/s0168-0072(01)00058-6
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 56,999
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Explicit Provability and Constructive Semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.
Logic of Proofs.Sergei Artëmov - 1994 - Annals of Pure and Applied Logic 67 (1-3):29-59.
Data Storage Interpretation of Labeled Modal Logic.Sergei Artëmov & Vladimir Krupski - 1996 - Annals of Pure and Applied Logic 78 (1-3):57-71.

Add more references

Citations of this work BETA

Explicit Provability and Constructive Semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.
The Logic of Justification.Sergei Artemov - 2008 - Review of Symbolic Logic 1 (4):477-513.
Tracking Reasons with Extensions of Relevant Logics.Shawn Standefer - 2019 - Logic Journal of the IGPL 27 (4):543-569.
Operations on Proofs and Labels.Tatiana Yavorskaya & Natalia Rubtsova - 2007 - Journal of Applied Non-Classical Logics 17 (3):283-316.

View all 6 citations / Add more citations

Similar books and articles


Added to PP index

Total views
13 ( #716,554 of 2,410,273 )

Recent downloads (6 months)
1 ( #540,207 of 2,410,273 )

How can I increase my downloads?


My notes