Birkhoff Completeness for Hybrid-Dynamic First-Order Logic

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

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

2 Citations (Scopus)

Abstract

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
PublisherSpringer
Pages277-293
Number of pages17
ISBN (Print)9783030290252
DOIs
Publication statusPublished - Jan 1 2019
Event28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019 - London, United Kingdom
Duration: Sep 3 2019Sep 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

Conference

Conference28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019
CountryUnited Kingdom
CityLondon
Period9/3/199/5/19

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

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

Cite this