Switch to: References

Add citations

You must login to add citations.
  1. Operations on proofs and labels.Tatiana Yavorskaya & Natalia Rubtsova - 2007 - Journal of Applied Non-Classical Logics 17 (3):283-316.
    Logic of proofs LP was introduced by S. Artemov in. It describes properties of the proof predicate “t is a proof of F” formalized by the formula ⟦t⟧ F. Proofs are represented by terms constructed by three elementary recursive operations on proofs. In this paper we extend the language of the logic of proofs by the additional storage predicate x ∋ F with the intended interpretation “x is a label for F”. The storage predicate can play the role of syntax (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • The single-conclusion proof logic and inference rules specification.Vladimir N. Krupski - 2001 - Annals of Pure and Applied Logic 113 (1-3):181-206.
    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 (...)
    Download  
     
    Export citation  
     
    Bookmark   6 citations