The single-conclusion proof logic and inference rules specification Original Research Article

The logic of single-conclusion (functional) proofs (View the MathML source) 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 View the MathML source 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 View the MathML source-admissibility testing is considered. We show that the provability in View the MathML source gives the complete admissibility test for the rules which can be specified by schemes in View the MathML source-language. The test is supplied with the ground proof extraction algorithm which eliminates the admissible rules from a View the MathML source-proof by utilizing the information from the corresponding View the MathML source-proofs.