Labelled tableaux for interpretability logics

2016/05/18 by Tuomas Hakoniemi, Tuomas A. Hakoniemi, Joost J. Joosten +2
Computer Science · Mathematics · #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies #math.LO

paper · pdf · doi:10.48550/arxiv.1605.05612

Dedicated to Albert Visser on the occasion of his retirement. In: Liber Amicorum Alberti, A Tribute to Albert Visser, Eds. Jan van Eijck, Rosalie Iemhoff and Joost J. Joosten, p. 141-154, Tributes Series Vol. 30, College Publications, London. ISBN 978-1-84890-204-6, 2016

arxiv created 2016/05/18 · openalex publication_date 2016/05/18 · arxiv updated 2016/05/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

In is paper we present a labelled tableau proof system that serves a wide class of interpretability logics. The system is proved sound and complete for any interpretability logic characterised by a frame condition given by a set of universal strict first order Horn sentences. As such, the current paper adds to a better proof-theoretical understanding of interpretability logics.

Citations

• Two series of formalized interpretability principles for weak systems of arithmetic
• Provability interpretations of modal logic

Related

• Analytic Tableaux for Justification Logics
• Tableau methodology for propositional logics
• Tableaux for First Order Logic of Proofs
• Data-Aware Hybrid Tableaux
• Two series of formalized interpretability principles for weak systems of arithmetic