Kyushu University Academic Staff Educational and Research Activities Database
List of Papers
Daniel Mircea GAINA Last modified date:2021.06.22

Assistant Professor / Australia Branch / Institute of Mathematics for Industry

1. Daniel Găină, Tomasz Kowalski, Fraïssé-Hintikka Theorem in institutions, Journal of Logic and Computation, 10.1093/logcom/exaa042, 30, 7, 1377-1399, 2020.10, [URL], We generalize the characterization of elementary equivalence by Ehrenfeucht–Fraïssé games to arbitrary institutions whose sentences are finitary. These include many-sorted first-order logic, higher-order logic with types, as well as a number of other logics arising in connection to specification languages. The gain for the classical case is that the characterization is proved directly for all signatures, including infinite ones..
2. Daniel Găină, Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi, Stability of termination and sufficient-completeness under pushouts via amalgamation, Theoretical Computer Science, 10.1016/j.tcs.2020.09.024, 2020.09, [URL], In the present study, we provide conditions for the existence of pushouts of signature morphisms in constructor-based order-sorted algebra, and then we prove that reducibility and termination of term rewriting systems are closed under pushouts. Under the termination assumption, reducibility is equivalent to sufficient-completeness, which is crucial for proving several important properties in computing for constructor-based logics such as completeness, existence of initial models and interpolation. In logic frameworks that are not based on constructors, sufficient-completeness is essential to establish the soundness of the induction schemes which are based on some methodological constructor operators. We discuss the application of our results to the instantiation of parameterized specifications..
3. Daniel Găină, Forcing and Calculi for Hybrid Logics, Journal of the Association for Computing Machinery, 10.1145/3400294, 67, 4, 1-55, 2020.06, [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, the paper introduces 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..
4. Daniel Găină, Ţuţu Ionuţ, Birkhoff Completeness for Hybrid-Dynamic First-Order Logic, 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019 Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, Proceedings, 10.1007/978-3-030-29026-9_16, 277-293, 2019.08, 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..
5. Daniel Gaina, Ionut Tutu, Adrian Riesco, Specification and Verification of Invariant Properties of Transition Systems, 25th Asia-Pacific Software Engineering Conference, APSEC 2018 Proceedings - 25th Asia-Pacific Software Engineering Conference, APSEC 2018, 10.1109/APSEC.2018.00024, 99-108, 2018.07, Transition systems provide a natural way to specify and reason about the behaviour of discrete systems, and in particular about the computations that they may perform. This paper advances a verification method for transition systems whose reachable states are described explicitly by membership axioms. The proof technique is implemented in the Constructor-based Inductive Theorem Prover (CITP), a proof management tool built on top of a variation of conditional equational logic enhanced with many modern features. This approach complements the so-called OTS method, a verification procedure for observational transition systems that is already implemented in CITP..
6. Daniel Găină, Birkhoff style calculi for hybrid logics, Formal Aspects of Computing, 10.1007/s00165-016-0414-y, 29, 5, 805-832, 2017.09, We develop an abstract proof calculus for hybrid logics whose sentences are (hybrid) Horn clauses, and we prove a Birkhoff completeness theorem for hybrid logics in the general setting provided by the institution theory. This result is then applied to particular cases of hybrid logics with user-defined sharing, where the first-order variables in quantified sentences are interpreted uniformly across worlds..
7. Daniel Găină, Downward Löwenheim-Skolem Theorem and interpolation in logics with constructors, Journal of Logic and Computation, 10.1093/logcom/exv018, 27, 6, 1717-1752, 2017.09, The present article describes a method for proving Downward Löwenheim-Skolem Theorem within an arbitrary institution satisfying certain logic properties. In order to demonstrate the applicability of the present approach, the abstract results are instantiated to many-sorted first-order logic and preorder algebra. In addition to the first technique for proving Downward Löwenheim-Skolem Theorem, another one is developed, in the spirit of institution-independent model theory, which consists of borrowing the result from a simpler institution across an institution comorphism. As a result, the Downward Löwenheim- Skolem Property is exported from first-order logic to partial algebras, and from higher-order logic with intensional Henkin semantics to higher-order logic with extensional Henkin semantics. The second method successfully extends the domain of application of Downward Löwenheim-Skolem Theorem to other non-conventional logical systems for which the first technique may fail. One major application of Downward Löwenheim-Skolem Theorem is interpolation in constructor-based logics with universally quantified sentences. The interpolation property is established by borrowing it from a base institution for its constructor-based variant across an institution morphism. This result is important as interpolation for constructor-based first-order logics is still an open problem..
8. Daniel Găină, Foundations of logic programming in hybrid logics with user-defined sharing, Theoretical Computer Science, 10.1016/j.tcs.2017.04.009, 686, 1-24, 2017.07, The present contribution advances an abstract notion of hybrid logic by supplementing the definition of institution with an additional structure to extract frames. The foundation of logic programming is set in the general framework proposed by defining the basic concepts such as Horn clause, query and solution, and proving fundamental results such as the existence of initial model of Horn clauses and Herbrand's theorem. The abstract results are then applied to hybrid logics with user-defined sharing, where the possible worlds share a common domain and the variables used for quantification are interpreted uniformly across the worlds..
9. Daniel Găină, Kokichi Futatsugi, Initial semantics in logics with constructors, Journal of Logic and Computation, 10.1093/logcom/exs044, 25, 1, 95-116, 2015.09, The constructor-based logics constitute the logical foundation of the so-called OTS/CafeOBJ method, a modelling, specification and verification method of the observational transition systems. The important role played in algebraic specifications by the initial algebras semantics is well known. Free models along presentation morphisms provide semantics for the modules with initial denotation in structured specification languages. Following Goguen and Burstall, the notion of logical system over which we build specifications is formalized as an institution. The present work is an institution-independent study of the existence of free models along sufficient complete presentation morphisms in logics with constructors in the signatures..
10. Daniel Găină, Foundations of logic programming in hybridised logics, 22nd International Workshop on Recent Trends in Algebraic Development Techniques, WADT 2014 Recent Trends in Algebraic Development Techniques - 22nd International Workshop, WADT 2014, Revised Selected Papers, 10.1007/978-3-319-28114-8_5, 69-89, 2015.01, The present paper sets the foundation of logic programming in hybridised logics. The basic logic programming semantic concepts such as query and solutions, and the fundamental results such as the existence of initial models and Herbrand’s theorem, are developed over a very general hybrid logical system.We employ the hybridisation process proposed by Diaconescu over an arbitrary logical system captured as an institution to define the logic programming framework..
11. Masaki Nakamura, Daniel Gaina, Kazuhiro Ogata, Kokichi Futatsugi, Proving sufficient completeness of constructor-based algebraic specifications, Lecture Notes in Electrical Engineering, 10.1007/978-981-10-0281-6_3, 373, 15-21, 2015.01, OBJ algebraic specification languages, for example, OBJ3, CafeOBJ and Maude, are formal specification languages which support several sophisticated functions to describe and verify large and complex specifications. Recently, the proof score method, which is an interactive formal verification method for OBJ languages, based on constructor-based algebras has been developed and several practical case studies have been reported. Sufficient completeness is one of the most important properties of constructor-based specifications, which guarantees the existence of initial models. In this study, we give a sufficient condition for sufficient completeness of constructor-based specifications based on the theory of term rewriting..
12. Daniel Mircea Gaina, Forcing, Downward Löwenheim-Skolem and Omitting Types Theorems, Institutionally, Logica Universalis, 10.1007/s11787-013-0090-0, 8, 3-4, 469-498, 2014.12, In the context of proliferation of many logical systems in the area of mathematical logic and computer science, we present a generalization of forcing in institution-independent model theory which is used to prove two abstract results: Downward Löwenheim-Skolem Theorem (DLST) and Omitting Types Theorem (OTT). We instantiate these general results to many first-order logics, which are, roughly speaking, logics whose sentences can be constructed from atomic formulas by means of Boolean connectives and classical first-order quantifiers. These include first-order logic (FOL), logic of order-sorted algebras (OSA), preorder algebras (POA), as well as their infinitary variants FOL ω1, ω, OSA ω1, ω, POA ω1, ω. In addition to the first technique for proving OTT, we develop another one, in the spirit of institution-independent model theory, which consists of borrowing the Omitting Types Property (OTP) from a simpler institution across an institution comorphism. As a result we export the OTP from FOL to partial algebras (PA) and higher-order logic with Henkin semantics (HNK), and from the institution of FOLω1, ω to PAω1, ω and HNKω1, ω. The second technique successfully extends the domain of application of OTT to non conventional logical systems for which the standard methods may fail..
13. Daniel Gǎinǎ, Dorel Lucanu, Kazuhiro Ogata, Kokichi Futatsugi, On automation of OTS/CafeOBJ method, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10.1007/978-3-642-54624-2_29, 8373, 578-602, 2014.01, The proof scores method is an interactive verification method in algebraic specification that combines manual proof planning and reduction (automatic inference by rewriting). The proof score approach to software verification coordinates efficiently human intuition and machine automation. We are interested in applying these ideas to transition systems, more concretely, in developing the so-called OTS/CafeOBJ method, a modelling, specification, and verification method of observational transition systems. In this paper we propose a methodology that aims at developing automatically proof scores according to the rules of an entailment system. The proposed deduction rules include a set of generic rules, which can be found in other proof systems as well, together with a set of rules specific to our working context. The methodology is exhibited on the example of the alternating bit protocol, where the unreliability of channels is faithfully specified..
14. Daniel Gǎinǎ, Min Zhang, Yuki Chiba, Yasuhito Arimoto, Constructor-based inductive theorem prover, 5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013 Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings, 10.1007/978-3-642-40206-7-26, 328-333, 2013.10, Constructor-based Theorem Prover (CITP) is a tool for proving inductive properties of software systems specified with constructor-based logics. CITP is equipped with a default proof strategy for the automated verification of Observational Transitional Systems (OTS), but the area of applications is not restricted to OTS. The proof strategy can be customised by the user, or the basic tactics can be applied step-by-step. The tool features are exhibited on concrete examples, showing how to perform verification with CITP..
15. Daniel Gǎinǎ, Interpolation in logics with constructors, Theoretical Computer Science, 10.1016/j.tcs.2012.12.002, 474, 46-59, 2013.02, We present a generic method for establishing the interpolation property by borrowing it across the logical systems from a base institution to prove it for its constructor-based variant. The framework used is that of the so-called institution theory invented by Goguen and Burstall which is a categorical-based formulation of the informal concept of logical system sufficiently abstract to capture many examples of logics used in computer science and mathematical logic, and expressive enough to elaborate our general results. We illustrate the applicability of the present work by instantiating the abstract results to constructor-based Horn clause logic and constructor-based Horn preorder algebra but applications are also expected for many other logical systems..
16. Kokichi Futatsugi, Daniel Găină, Kazuhiro Ogata, Principles of proof scores in CafeOBJ, Theoretical Computer Science, 10.1016/j.tcs.2012.07.041, 464, 90-112, 2012.12, This paper describes the theoretical principles of a verification method with proof scores in the CafeOBJ algebraic specification language. The verification method focuses on specifications with conditional equations and realizes systematic theorem proving (or interactive verification). The method is explained using a simple but instructive example, and the necessary theoretical foundations, which justify every step of the verification, are described with precise mathematical definitions. Some important theorems that result from the definitions are also presented..
17. Daniel Gǎinǎ, Kokichi Futatsugi, Kazuhiro Ogata, Constructor-based logics, Journal of Universal Computer Science, 18, 16, 2204-2233, 2012.12, Many computer science applications concern properties that are true for a restricted class of models. In this paper, a couple of constructor-based institutions are presented. These institutions are defined on top of some base institutions, roughly speaking, by enhancing the syntax with constructor symbols and restricting the semantics to models with elements that are reachable by constructors. The proof rules for the constructor-based Horn logics, formalized as institutions, are defined in this paper, and a proof of completeness is provided in the abstract framework of institutions..
18. Daniel Găină, Marius Petria, Completeness by forcing, Journal of Logic and Computation, 10.1093/logcom/exq012, 20, 6, 1165-1186, 2010.12, The completeness of the infinitary language ℒ ω1,ω was proved by Carol Karp in 1964.We express and prove the completeness of infinitary first-order logics in the institution-independent setting by using forcing, a powerful method for constructing models. As a consequence of this abstraction, the completeness theorem becomes available for the infinitary versions of many 'first order' logical systems that appear in the area of logic or computer science..
19. Daniel Gǎinǎ, Kokichi Futatsugi, Kazuhiro Ogata, Constructor-based institutions, 3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2009 Algebra and Coalgebra in Computer Science - Third International Conference, CALCO 2009, Proceedings, 10.1007/978-3-642-03741-2_27, 398-412, 2009.11, Many computer science applications concern properties which are true of a restricted class of models. We present a couple of constructor-based institutions defined on top of some base institutions by restricting the class of models. We define the proof rules for these logics formalized as institutions, and prove their completeness in the abstract framework of institutions..
20. Mihai Codescu, Daniel Găină, Birkhoff completeness in institutions, Logica Universalis, 10.1007/s11787-008-0035-1, 2, 2, 277-309, 2008.09, We develop an abstract proof calculus for logics whose sentences are 'Horn sentences' of the form: (∀X)H ⇒ c and prove an institutional generalization of Birkhoff completeness theorem. This result is then applied to the particular cases of Horn clauses logic, the 'Horn fragment' of preorder algebras, order-sorted algebras and partial algebras and their infinitary variants..
21. Daniel Gǎinǎ, Andrei Popescu, Erratum
An institution-independent generalization of tarski's elementary chain theorem (Journal of Logic and Computation (2006) 16 (713-735) DOI: 10.1093/logcom/exl006), Journal of Logic and Computation, 10.1093/logcom/exm022, 17, 3, 2007.06.
22. Daniel Găină, Andrei Popescu, An institution-independent proof of the Robinson Consistency Theorem, Studia Logica, 10.1007/s11225-007-9022-4, 85, 1, 41-73, 2007.02, We prove an institutional version of A. Robinson's Consistency Theorem. This result is then appliedto the institution of many-sorted first-order predicate logic and to two of its variations, infinitary and partial, obtaining very general syntactic criteria sufficient for a signature square in order to satisfy the Robinson consistency and Craig interpolation properties..
23. Daniel Gǎinǎ, Andrei Popescu, An institution-independent generalization of Tarski's elementary chain theorem, Journal of Logic and Computation, 10.1093/logcom/exl006, 16, 6, 2006.12, We prove an institutional version of Tarski's elementary chain theorem applicable to a whole plethora of 'first-orderaccessible' logics, which are, roughly speaking, logics whose sentences can be constructed from atomic formulae by means of classical first-order connectives and quantifiers. These include the unconditional equational, positive, (π ∪ ∑)n 0 and full first-order logics, as well as less conventional logics, used in computer science, such as hidden or rewriting logic..