Schema Complexity in Propositional-Based Logics

The essential structure of derivations is used as a tool for measuring the complexity of schema consequences in propositional-based logics. Our schema derivations allow the use of schema lemmas and this is reflected on the schema complexity. In particular, the number of times a schema lemma is used...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Jaime Ramos, João Rasga, Cristina Sernadas
Formato: article
Lenguaje:EN
Publicado: MDPI AG 2021
Materias:
Acceso en línea:https://doaj.org/article/19bd520978e34bb287db101bb426fa05
Etiquetas: Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
Descripción
Sumario:The essential structure of derivations is used as a tool for measuring the complexity of schema consequences in propositional-based logics. Our schema derivations allow the use of schema lemmas and this is reflected on the schema complexity. In particular, the number of times a schema lemma is used in a derivation is not relevant. We also address the application of metatheorems and compare the complexity of a schema derivation after eliminating the metatheorem and before doing so. As illustrations, we consider a propositional modal logic presented by a Hilbert calculus and an intuitionist propositional logic presented by a Gentzen calculus. For the former, we discuss the use of the metatheorem of deduction and its elimination, and for the latter, we analyze the cut and its elimination. Furthermore, we capitalize on the result for the cut elimination for intuitionistic logic, to obtain a similar result for Nelson’s logic via a language translation.