Experiments in Theorem Proving for Topological Hybrid Logic

Dmitry Sustretov 1 Guillaume Hoffmann 1 Carlos Areces 1 Patrick Blackburn 1
1 TALARIS - Natural Language Processing: representation, inference and semantics
Inria Nancy - Grand Est, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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, 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.
Type de document :
Communication dans un congrès
Methods for Modalities 5, Nov 2007, Cachan, France. 2007
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00187303
Contributeur : Guillaume Hoffmann <>
Soumis le : mercredi 14 novembre 2007 - 11:47:32
Dernière modification le : jeudi 11 janvier 2018 - 06:21:35
Document(s) archivé(s) le : lundi 24 septembre 2012 - 15:25:47

Fichier

m4m-topo.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00187303, version 1

Collections

Citation

Dmitry Sustretov, Guillaume Hoffmann, Carlos Areces, Patrick Blackburn. Experiments in Theorem Proving for Topological Hybrid Logic. Methods for Modalities 5, Nov 2007, Cachan, France. 2007. 〈inria-00187303〉

Partager

Métriques

Consultations de la notice

233

Téléchargements de fichiers

140