Tableaux for Quantified Hybrid Logic

Patrick Blackburn 1 Maarten Marx 2
1 LANGUE ET DIALOGUE - Human-machine dialogue with a significant language component
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present a (sound and complete) tableau calculus for Quantified Hybrid Logic (QHL). QHL is an extension of orthodox quantified modal logic: as well as the usual Box and Diamond modalities it contains names for (and variables over) states, operators @_s for asserting that a formula holds at a named state, and a binder Downarrow that binds a variable to the current state. The first-order component contains equality and rigid and non rigid designators. As far as we are aware, ours is the first tableau system for QHL. Completeness is established via a variant of the standard translation to first order logic. More concretely, a valid QHL-sentence is translated into a valid first order sentence in the correspondence language. As it is valid, there exists a first order tableau proof for it. This tableau proof is then converted into a QHL tableau proof for the original sentence. In this way we recycle a well-known result (completeness of first order logic) instead of a well--known proof. The tableau calculus is highly flexible. We only present it for the constant domain semantics, but slight changes render it complete for varying, expanding or contracting domains. Moreover, completeness with respect to specific frame classes can be obtained simply by adding extra rules or axioms (this can be done for every first-order definable class of frames which is closed under and reflects generated subframes).
Type de document :
Communication dans un congrès
U. Egly, C.G. Fermüller. International Conference on Automated Reasoning with Analytic Tableaux and Related Methods - TABLEAUX 2002, Jul 2002, Copenhagen, Denmark, Springer, 2381, pp.38-52, 2002, Lecture Notes in Artificial Intelligence
Liste complète des métadonnées

https://hal.inria.fr/inria-00100892
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:52:42
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48

Identifiants

  • HAL Id : inria-00100892, version 1

Collections

Citation

Patrick Blackburn, Maarten Marx. Tableaux for Quantified Hybrid Logic. U. Egly, C.G. Fermüller. International Conference on Automated Reasoning with Analytic Tableaux and Related Methods - TABLEAUX 2002, Jul 2002, Copenhagen, Denmark, Springer, 2381, pp.38-52, 2002, Lecture Notes in Artificial Intelligence. 〈inria-00100892〉

Partager

Métriques

Consultations de la notice

52