Geodesic
On symbolic models for Single-Conclusion Logic of Proofs
Sbornik. Mathematics, Tome 202 (2011) no. 5, pp. 683-695 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

In this paper we define symbolic models for Single-Conclusion Logics of Proofs. We prove the soundness and completeness of these logics with respect to the corresponding classes of symbolic models. We apply the semantic methods developed in this paper to justify the use of terms of single-conclusion logic of proofs as notation for derivations in this logic. Bibliography: 17 titles.
Keywords: formal derivation, proof predicate, single-conclusion logic of proofs, Mkrtychev models, internalization property. 
@article{SM_2011_202_5_a3,
     author = {V. N. Krupski},
     title = {On symbolic models for {Single-Conclusion} {Logic} of {Proofs}},
     journal = {Sbornik. Mathematics},
     pages = {683--695},
     year = {2011},
     volume = {202},
     number = {5},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/SM_2011_202_5_a3/}
}
TY  - JOUR
AU  - V. N. Krupski
TI  - On symbolic models for Single-Conclusion Logic of Proofs
JO  - Sbornik. Mathematics
PY  - 2011
SP  - 683
EP  - 695
VL  - 202
IS  - 5
UR  - http://geodesic.mathdoc.fr/item/SM_2011_202_5_a3/
LA  - en
ID  - SM_2011_202_5_a3
ER  - 
%0 Journal Article
%A V. N. Krupski
%T On symbolic models for Single-Conclusion Logic of Proofs
%J Sbornik. Mathematics
%D 2011
%P 683-695
%V 202
%N 5
%U http://geodesic.mathdoc.fr/item/SM_2011_202_5_a3/
%G en
%F SM_2011_202_5_a3
V. N. Krupski. On symbolic models for Single-Conclusion Logic of Proofs. Sbornik. Mathematics, Tome 202 (2011) no. 5, pp. 683-695. http://geodesic.mathdoc.fr/item/SM_2011_202_5_a3/

[1] S. Artemov, L. Beklemishev, “Provability logic”, Handbook of philosophical logic, v. 13, Springer-Verlag, Berlin, 2005, 189–360

[2] S. Artemov, Operational modal logic, Technical report MSI 95–29, Cornell University, Ithaca, NY, 1995

[3] S. Artemov, Logic of proofs: a unified semantics for modality and $\lambda$-terms, Technical report CFIS 98–06, Cornell University, Ithaca, NY, 1998

[4] S. N. Artemov, “Explicit provability and constructive semantics”, Bull. Symbolic Logic, 7:1 (2001), 1–36 | DOI | MR | Zbl

[5] V. N. Krupski, “Operational logic of proofs with functionality condition on proof predicate”, Logical foundations of computer science (Yaroslavl, Russia, 1997), Lecture Notes in Comput. Sci., 1234, Springer-Verlag, Berlin, 1997, 167–177 | MR | Zbl

[6] V. N. Krupski, “The single-conclusion proof logic and inference rules specification”, Ann. Pure Appl. Logic, 113:1–3 (2001), 181–206 | DOI | MR | Zbl

[7] V. N. Krupski, “Reference constructions in the single-conclusion proof logic”, J. Logic Comput., 16:5 (2006), 645–661 | DOI | MR | Zbl

[8] V. N. Krupski, “Referential logic of proofs”, Theoret. Comput. Sci., 357:1–3 (2006), 143–166 | DOI | MR | Zbl

[9] S. Artëmov, V. Krupski, “Data storage interpretation of labeled modal logic”, Ann. Pure Appl. Logic, 78:1–3 (1996), 57–71 | DOI | MR | Zbl

[10] A. Mkrtychev, “Models for the logic of proofs”, Logical foundations of computer science (Yaroslavl, Russia, 1997), Lecture Notes in Comput. Sci., 1234, Springer-Verlag, Berlin, 1997, 266–275 | MR | Zbl

[11] R. Kuznets, “On the complexity of explicit modal logics”, Computer science logic (Fischbachau, Germany, 2000), Lecture Notes in Comput. Sci., 1862, Springer-Verlag, Berlin, 2000, 371–383 | DOI | MR | Zbl

[12] T. Yavorskaya (Sidon), “Negative operations on proofs and labels”, J. Logic Comput., 15:4 (2005), 517–537 | DOI | MR | Zbl

[13] T. Yavorskaya (Sidon), N. Rubtsova, “Operations on proofs and labels”, J. Appl. Non-Classical Logics, 17:3 (2007), 283–316 | DOI | MR | Zbl

[14] N. M. Rubtsova, “Logic of proofs with substitution”, Math. Notes, 82:5–6 (2007), 816–826 | DOI | MR | Zbl

[15] M. Fitting, “The logic of proofs, semantically”, Ann. Pure Appl. Logic, 132:1 (2005), 1–25 | DOI | MR | Zbl

[16] S. Artemov, E. Nogina, “Introducing justification into epistemic logic”, J. Logic Comput., 15:6 (2005), 1059–1073 | DOI | MR | Zbl

[17] N. Rubtsova, “On realization of $S5$-modality by evidence terms”, J. Logic Comput., 16:5 (2006), 671–684 | DOI | MR | Zbl