1996 | ReviewPaper | Buchkapitel
Efficient loop-check for backward proof search in some non-classical propositional logics
verfasst von : Alain Heuerding, Michael Seyfried, Heinrich Zimmermann
Erschienen in: Theorem Proving with Analytic Tableaux and Related Methods
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We consider the modal logics KT and S4, the tense logic Kt, and the fragment IPC(∧,→) of intuitionistic logic.For these logics backward proof search in the standard sequent or tableau calculi does not terminate in general. In terms of the respective Kripke semantics, there are several kinds of non-termination: loops inside a world (KT), infinite resp. looping branches (S4, IPC(∧,→)), and infinite branching degree (Kt).We give uniform sequent-based calculi that contain specifically tailored loop-checks such that the efficiency of proof search is not deteriorated. Moreover all these loop-checks are easy to implement and can be combined with optimizations.Note that our calculus for S4 is not a pure contraction-free sequent calculus, but this (theoretical) defect does not hinder its application in practice.