|Daniel Mircea GAINA||Last modified date：2021.06.22|
Assistant Professor / Australia Branch / Institute of Mathematics for Industry
|1.||Daniel Gaina, Forcing and Calculi for Hybrid Logics, Australasian Logic Group, 2020.12.|
|2.||Daniel Găină, Forcing and Calculi for Hybrid Logics, 31st Seminar on Algebra, Logic and Geometry in Informatics (ALGI), 2020.09, [URL].|
|3.||Daniel Găină, Horn Clauses in Hybrid-Dynamic First-Order Logic, The 15th Theorem Proving and Provers meeting (TPP 2019), 2019.11, [URL], We propose a hybrid-dynamic first-order logic as a formal foundation for specifying and reasoning about reconfigurable systems.As the name suggests, the formalism we develop extends (many-sorted) first-order logic with features that are common to hybrid logics and to dynamic logics.This provides certain key advantages for dealing with reconfigurable systems, such as: (a) a signature of nominals, including operation and relation symbols, that allows references to specific possible worlds / system configurations – as in the case of hybrid logics; (b) distinguished signatures of rigid and flexible symbols, where the rigid symbols are interpreted uniformly across possible worlds; this supports a rigid form of quantification, which ensures that variables have the same interpretation regardless of the possible world where they are evaluated; (c) hybrid terms, which increase the expressive power of the logic in the context of rigid symbols; and (d) modal operators over dynamic-logic actions, which are defined as regular expressions over binary nominal relations. We then study Horn clauses in this hybrid-dynamic logic, and develop a series of results that lead to an initial-semantics theorem for arbitrary sets of clauses.This shows that a significant fragment of hybrid-dynamic first-order logic has good computational properties, and can serve as a basis for defining executable languages for reconfigurable systems..|
|4.||Daniel Găină, Birkhoff Completeness for Hybrid-Dynamic First-Order Logic, The 18th Logic and Computation Seminar, 2019.11, [URL], 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:
(a) first, the possible worlds of Kripke structures, as well as the nominals used to identify them, are endowed with an algebraic structure;
(b) 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;
(c) 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..
|5.||Daniel Găină, Forcing and its applications in hybrid logics, Section of Mathematical Sciences of the Romanian Academy, the Romanian Mathematical Society, the Simion Stoilow Institute of Mathematics of the Romanian Academy, the Faculty of Mathematics and Computer Science of the University of Bucharest, 2019.07, [URL], The definition of institution formalizes the intuitive notion of logic in a category-based setting. Similarly, the concept of stratified institution provides an abstract approach to Kripke semantics. This includes hybrid logics, a type of modal logics expressive enough to allow references to the nodes/states/worlds of the models regarded as relational structures, or multi-graphs. Applications of hybrid logics involve many areas of research such as computational linguistics, transition systems, knowledge representation, artificial intelligence, biomedi- cal informatics, semantic networks and ontologies. The present contribution sets a unified foundation for developing formal verification methodologies to reason about Kripke structures by defining proof calculi for a multitude of hybrid logics in the framework of stratified institutions. In order to prove completeness, we introduce a forcing technique for stratified institutions with nominal and frame extraction and studies a forcing property based on syntactic consistency. The proof calculus is shown to be complete and the significance of the general results is exhibited on a couple of benchmark examples of hybrid logical systems..|
|6.||Daniel Găină, Specification and Verification of Invariant Properties of Transition Systems, 25th Asia-Pacific Software Engineering Conference (APSEC 2018), 2018.12.|
|7.||Daniel Găină, Specification and Verification of Invariant Properties of Transition Systems, Working Formal Methods Symposium (FROM 2017), 2017.07, [URL].|
|8.||Daniel Găină, Mathematical structures for developing reconfigurable systems, La Trobe - Kyushy Joint Seminar on Mathematics for Industry, 2017.05.|