Lightweight hybrid tableaux
type: Item
instance of: scholarly article
title: Lightweight hybrid tableaux
zbMATH Open document ID: 1228.03004
author: Guillaume Hoffmann
published in: Journal of Applied Logic
publication date: 2011-03-22T00:00:00Z
review text: The paper presents a decision procedure for some fragments of the hybrid logic. The main difference between hybrid logic and modal logic is the presence of nominals, which are propositional symbols true at exactly one world in a model. The decision procedure is based on a prefixed tableau calculus. The general idea of the termination proof of this system is that, on the one hand, the quasi-subformula property guarantees that a given prefix can only make true finitely many formulas and, on the other hand, there can only be finitely many prefixes in a branch of the tableau.
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 5869149
zbMATH Keywords: hybrid logic
zbMATH Keywords: modal logic
zbMATH Keywords: tableau calculus
zbMATH Keywords: decision procedure
zbMATH Keywords: loop-check
zbMATH Keywords: difference modality
zbMATH Keywords: converse modality
zbMATH Keywords: nominals
reviewed by: Nail Zamov
describes a project that uses: KL-ONE
MaRDI profile type: Publication
full work available at URL: j.jal.2010.08.003
OpenAlex ID: W2035819327
cites work: An overview of tableau algorithms for description logics
cites work: Termination for Hybrid Tableaus
cites work: Introduction to algorithms
cites work: A description logic with transitive and inverse roles and role hierarchies
cites work: Hybrid Tableaux for the Difference Modality
cites work: Terminating tableau systems for hybrid logic with difference and converse
cites work: Optimizing terminological reasoning for expressive description logics
DOI: 10.1016/J.JAL.2010.08.003
description: scientific article; zbMATH DE number 5869149