Naslov
Tableaux-Based Prover for Typed Hybrid Multimodal Logic (System Description)

Autori
Rosenzweig, Dean ; Runje, Davor

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Proceedings of the 3rd Methods for Modalities Workshop / Areces C., Blackburn P. - Nancy : LORIA Nancy, 2003, 149-156

Skup
Methods for Modalities 3

Mjesto i datum
Nancy, Francuska, 22.09.2003. - 23.09.2003

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
hybrid modal logic; tableau-based theorem prover

Sažetak
Some potential application domains of hybrid multimodal logic suggest typing of states and imposing type--constraints on modalities. In \cite{;RRS03b}; we have investigated the logical/computational cost of such an extension with a very simple system of types and concluded that there is none: both expressivity and complexity are preserved by the extension. Rewrite rules coping with state equality and state succession have been a major obstacle for efficient implementation of tableaux systems for hybrid modal logic. We handle state equality, state succession and valuation on the metalevel instead, constructing an explicit model--to--be in the process. Handling of types on the metalevel comes naturally in the presence of an explicit model, and it can considerably prune the search space. We present a prototype implementation of a tableaux--based theorem prover built along these lines. The prover handles type--free hybrid modal logic and its subsystems as well.

Izvorni jezik
Engleski

Znanstvena područja
Matematika

POVEZANOST RADA