engleski

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

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.

hybrid modal logic; tableau-based theorem prover

nije evidentirano