## 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 □ and ◊ modalities it contains names for (and variables over)
states, operators @_{s} for asserting that a formula holds at a
named state, and a binder ↓ 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).

Original language | English |
---|---|

Title of host publication | Automated Reasoning with Analytic Tableaux and Related Methods : International Conference, TABLEAUX 2002, Proceedings |

Editors | Uwe Egly, Christian G. Fermuller |

Number of pages | 15 |

Publisher | Springer |

Publication date | 2002 |

Pages | 38-52 |

ISBN (Print) | 3540439293, 9783540439295 |

ISBN (Electronic) | 978-3-540-45616-2 |

DOIs | |

Publication status | Published - 2002 |

Externally published | Yes |

Event | International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2002 - Copenhagen, Denmark Duration: 30 Jul 2002 → 1 Aug 2002 |

### Conference

Conference | International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2002 |
---|---|

Country/Territory | Denmark |

City | Copenhagen |

Period | 30/07/2002 → 01/08/2002 |

Sponsor | Kurt Godel Society, Vienna University of Technoloy |

Series | Lecture Notes in Computer Science |
---|---|

Volume | 2381 |

ISSN | 0302-9743 |

## Keywords

- Modal Logic
- Hybrid Logic
- Replacement Rule
- Predicate Abstraction
- Conjunctive Rule