Experiments in Theorem Proving for Topological Hybrid Logic

D. Sustretov, G. Hoffmann, C. Areces, and P. Blackburn. Experiments in Theorem Proving for Topological Hybrid Logic. In Proceedings of Methods for Modalities 5, 2007.

Download

[pdf] 

Abstract

This paper discusses two experiments in theorem proving for hybrid logic under the topological interpre- tation. 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 of HyLoTab [17], 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.

BibTeX

@InProceedings{Sustretov2007,
  author =       "D. Sustretov and G. Hoffmann and C. Areces and P.
                 Blackburn",
  booktitle =    "Proceedings of Methods for Modalities 5",
  title =        "Experiments in Theorem Proving for Topological Hybrid
                 Logic",
  year =         "2007",
  abstract =     "This paper discusses two experiments in theorem
                 proving for hybrid logic under the topological
                 interpre- tation. 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 of HyLoTab [17], 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.",
  owner =        "areces",
  timestamp =    "2007.10.25",
}