Experiments in Theorem Proving for Topological Hybrid Logic

Dmitry Sustretov*, Guillaume Hoffmann, Carlos Areces, Patrick Blackburn

*Corresponding author

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

Abstract

This paper discusses two experiments in theorem proving for hybrid logic under the topological interpretation. We begin by discussing the topological interpretation of hybrid logic and noting what it adds to the topological interpretation of orthodox modal logic. We then examine two implemented proof methods. The first makes use of HyLoBan, a terminating theorem prover that searches for a winning search strategy in certain topologically motivated games. The second is a translation-based approach that makes use HyLoTab [J. van Eijck. HyLoTab - Tableau-based theorem proving for hybrid logics. Manuscript, CWI, available from http://www.cwi.nl/~jve/hylotab, 2002], a tableaux-based theorem prover for hybrid logic under the standard relational interpretation. We compare the two methods, and note a number of directions for further work.
OriginalsprogEngelsk
TidsskriftElectronic Notes in Theoretical Computer Science
Vol/bind231
Sider (fra-til)309-321
Antal sider13
ISSN1571-0661
DOI
StatusUdgivet - 25 mar. 2009
Udgivet eksterntJa

Emneord

  • hybrid logic
  • theorem proving
  • topological semantics

Citer dette