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

Proof systems for hybrid logic typically use    @   -operators to access information hidden behind modalities; this labelling approach lies at the heart of the best known hybrid resolution, natural deduction and tableau systems. But there is another approach, which we have come to believe is conceptually clearer. We call this Seligman-style inference, as it was first introduced and explored by Jerry Seligman in natural deduction and sequent calculus in the 1990s. The purpose of this article is to introduce a Seligman-style tableau system, to prove its completeness, and to show how it can be made to terminate. The most obvious feature of Seligman-style systems is that they work with arbitrary formulas, not just statements prefixed by    @   -operators. They do so by introducing machinery for switching to other proof contexts. We capture this idea in the setting of tableaus by introducing a rule called  GoTo , which allows us to ‘jump to a named world’ on a tableau branch. We first develop a Seligman-style tableau system for basic hybrid logic and prove its completeness. We then prove termination of a restricted version of the system without resorting to loop checking, and show that the restrictions do not effect completeness. Both completeness and termination results are proved by explicit translations that transform tableaus in a standard labelled system into Seligman-style tableaus and vice-versa.

Completeness and termination for a Seligman-style tableau system