Abstract
Symbolic semantics for logics of proofs based on Mkrtychev models covers the the case of multi-conclusion proof logics. We propose symbolic models for single-conclusion proof logics (FLP and its extensions). The corresponding soundness and completeness theorems are proven. The developed symbolic model technique is used to establish the consistency of contexts required for proof internalization. In particular, we construct an extension of FLP that enjoys the strong proof internalization property with empty context. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Krupski, V. N. (2010). Symbolic models for single-conclusion proof logics. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6072 LNCS, pp. 276–287). https://doi.org/10.1007/978-3-642-13182-0_26
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
