Birkhoff Completeness for Hybrid-Dynamic First-Order Logic

Daniel Găină, Ionuţ Ţuţu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)


Hybrid-dynamic first-order logic is a kind of modal logic obtained by enriching many-sorted first-order logic with features that are common to hybrid and to dynamic logics. This provides us with a logical system with an increased expressive power thanks to a number of distinctive attributes: first, the possible worlds of Kripke structures, as well as the nominals used to identify them, are endowed with an algebraic structure; second, we distinguish between rigid symbols, which have the same interpretation across possible worlds – and thus provide support for the standard rigid quantification in modal logic – and flexible symbols, whose interpretation may vary; third, we use modal operators over dynamic-logic actions, which are defined as regular expressions over binary nominal relations. In this context, we propose a general notion of hybrid-dynamic Horn clause and develop a proof calculus for the Horn-clause fragment of hybrid-dynamic first-order logic. We investigate soundness and compactness properties for the syntactic entailment system that corresponds to this proof calculus, and prove a Birkhoff-completeness result for hybrid-dynamic first-order logic.

Original languageEnglish
Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, Proceedings
EditorsSerenella Cerrito, Andrei Popescu
Number of pages17
ISBN (Print)9783030290252
Publication statusPublished - 2019
Event28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019 - London, United Kingdom
Duration: Sept 3 2019Sept 5 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11714 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019
Country/TerritoryUnited Kingdom

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Birkhoff Completeness for Hybrid-Dynamic First-Order Logic'. Together they form a unique fingerprint.

Cite this