English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

Hybrid logics are a principled generalization of both modal logics and description logics. It is well known that various hybrid logics without binders are decidable, but decision procedures are usually not based on tableau systems, a kind of formal proof procedure that lends itself to computer implementation. In this article, we give four different tableau-based decision procedures for a very expressive hybrid logic including the universal modality; three of the procedures are based on different tableau systems, and one procedure is based on a Gentzen system. The decision procedures make use of so-called loop-checks, which is a standard technique used in connection with tableau systems for other logics, namely, prefixed tableau systems for transitive modal logics as well as for certain description logics. The loop-checks used in our four decision procedures are similar, but the four proof systems on which the procedures are based constitute a spectrum of different systems: prefixed and internalized systems, tableau and Gentzen systems.

Tableau-based Decision Procedures for Hybrid Logic