Geodesic
Normalization of terms in exact models of the logic of evidence LP
Vestnik Moskovskogo universiteta. Matematika, mehanika, no. 6 (2023), pp. 52-55 
V. N. Krupski. Normalization of terms in exact models of the logic of evidence LP. Vestnik Moskovskogo universiteta. Matematika, mehanika, no. 6 (2023), pp. 52-55. http://geodesic.mathdoc.fr/item/VMUMM_2023_6_a7/
@article{VMUMM_2023_6_a7,
     author = {V. N. Krupski},
     title = {Normalization of terms in exact models of the logic of evidence {LP}},
     journal = {Vestnik Moskovskogo universiteta. Matematika, mehanika},
     pages = {52--55},
     year = {2023},
     number = {6},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/VMUMM_2023_6_a7/}
}
TY  - JOUR
AU  - V. N. Krupski
TI  - Normalization of terms in exact models of the logic of evidence LP
JO  - Vestnik Moskovskogo universiteta. Matematika, mehanika
PY  - 2023
SP  - 52
EP  - 55
IS  - 6
UR  - http://geodesic.mathdoc.fr/item/VMUMM_2023_6_a7/
LA  - ru
ID  - VMUMM_2023_6_a7
ER  - 
%0 Journal Article
%A V. N. Krupski
%T Normalization of terms in exact models of the logic of evidence LP
%J Vestnik Moskovskogo universiteta. Matematika, mehanika
%D 2023
%P 52-55
%N 6
%U http://geodesic.mathdoc.fr/item/VMUMM_2023_6_a7/
%G ru
%F VMUMM_2023_6_a7

Voir la notice de l'article provenant de la source Math-Net.Ru

A basic justification model is sharp when the evidence term constructors $\cdot, +, !$ in it mean exactly the application of modus ponens rule, the union and the verification of evidences. We construct an example of a sharp model for the logic of proofs LP and establish that in any sharp model of LP every proof term is equivalent to some proof polynomial.

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

[2] Mkrtychev A., “Models for the logic of proofs”, Logical Foundations of Computer Science, Int. Symp. LFCS'97, Lect. Notes Comput. Sci. Vol., 1234, eds. S. Adyan, A. Nerode, Springer, Cham, 1997, 266–275 | DOI | MR | Zbl

[3] Artemov S., Fitting M., Justification logic: Reasoning with reasons, Cambridge University Press, Cambridge, 2019 | MR | Zbl

[4] Artemov S., “Justification awareness models”, Logical Foundations of Computer Science, Int. Symp. LFCS 2018, Lect. Notes Comput. Sci., 10703, eds. S. Artemov, A. Nerode, Springer, Cham, 2018, 22–36 | DOI | MR | Zbl

[5] Krupski N., “On the complexity of the reflected logic of proofs”, Theor. Comput. Sci., 357:1–3 (2006), 136–142 | DOI | MR | Zbl