3532 articles – 5253 Notices  [english version]

inria-00187303, version 1

Experiments in Theorem Proving for Topological Hybrid Logic

Dmitry Sustretov 1, Guillaume Hoffmann () 1, Carlos Areces () 1, Patrick Blackburn () 1

Methods for Modalities 5 (2007)

Résumé : 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, 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.

  • 1 :  TALARIS (INRIA Nancy - Grand Est / LORIA)
  • CNRS : UMR7503 – INRIA – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
  • Domaine : Informatique/Logique en informatique
  • Mots-clés : hybrid logic – topological semantics – theorem proving
 
  • inria-00187303, version 1
  • http://hal.inria.fr/inria-00187303
  • oai:hal.inria.fr:inria-00187303
  • Contributeur : Guillaume Hoffmann <>
  • Soumis le : Mercredi 14 Novembre 2007, 11:47:32
  • Dernière modification le : Mercredi 14 Novembre 2007, 14:12:51