The single-conclusion proof logic and inference rules specificationстатья
Информация о цитировании статьи получена из
Web of Science
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 27 мая 2015 г.
Аннотация:The {\em Logic of Single-Conclusion (functional) Proofs} (${\cal FLP}$) 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
${\cal FLP}$ 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 ${\cal PA}$-admissibility
testing is considered. We show that the provability in ${\cal FLP}$ gives
the complete admissibility test for the rules which can be specified by
schemes in ${\cal FLP}$-language. The test is supplied with the ground proof
extraction algorithm which eliminates the admissible rules from a
${\cal PA}$-proof by utilizing the information from the corresponding
${\cal FLP}$-proofs.