2024/07/28 更新

お知らせ

 

写真a

ガイナ ダニエル ミルチヤ
GAINA DANIEL MIRCEA
GAINA MIRCEA DANIEL
所属
マス・フォア・インダストリ研究所 准教授
理学部 数学科(併任)
数理学府 数理学専攻(併任)
マス・フォア・イノベーション連係学府 (併任)
職名
准教授
連絡先
メールアドレス
電話番号
0928024425
プロフィール
My research is focused on algebraic specification, one of the most promising aproach to formal methods assisting the developing of software systems at several stages such as design, specification and formal verification. Algebraic specification and programming languages are rigorously based on logic, which amounts to the existence of a logical system underlying the language such that each language feature and construction can be expressed as a mathematical entity of the underlying logic.

学位

  • BSc in informatics from University of Bucharest

  • MSc in fundamentals of informatics from University of Bucharest

  • MSc in algebraic specification from Normal Superior School of Bucharest

  • PhD in information science from Japan Advanced Institute of Science and Technology

経歴

  • October 2004 - October 2006: research assistant at University of Bucharest October 2009 - July 2010: postdoctoral researcher at Japan Advanced Institute of Science and Technology August 2010 - March 2013: research assistant professor at Japan Advanced Institute of Science and Technology April 2013 - March 2017: assistant professor at Japan Advanced Institute of Science and Technology April 2017 - March 2022: assistant professor at Kyushu University April 2022 - present: associate professor at Kyushu University   

研究テーマ・研究キーワード

  • 研究テーマ: Reconfigurable systems are found everywhere: software-driven medical devices (such as infusion pumps, pacemakers, imaging machines and pill cameras), intelligent transportation systems, cars, or mobile robots. They all interact with their users and the environment in which they operate. Reconfigurable systems are often used in safety-critical areas where any malfunction may cause serious injuries to human beings. The safety requirements can be fulfilled only by applying formal methods. The objective is to develop a software tool for the formal specification and verification of reconfigurable systems.

    研究キーワード: theorem proving, reconfiguration paradigm, hybrid systems, verification methodology

    研究期間: 2023年4月 - 2026年4月

  • 研究テーマ: Recent developments of computer systems have triggered a paradigm shift from standard applications with fixed resources to reconfigurable systems, i.e. applications that work in different operation modes, called configurations, and react flexibly to internal and external stimuli for optimizing their performance. Very often the operation of reconfigurable systems is safety-critical: any malfunction may result in the serious injury to people. The safety requirements can be fulfilled only by applying formal methods. The purpose is to provide a solid logic-based foundation for developing a formal method to describe reconfigurable systems and to reason formally about their properties.

    研究キーワード: reconfigurable systems, formal methods, hybrid-dynamic logics

    研究期間: 2020年4月 - 2023年4月

論文

  • Forcing and Calculi for Hybrid Logics 査読 国際誌

    Daniel Găină

    Journal of the Association for Computing Machinery   67 ( 4 )   1 - 55   2020年6月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    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.

    DOI: https://doi.org/10.1145/3400294

    その他リンク: https://dl.acm.org/doi/10.1145/3400294

    リポジトリ公開URL: https://hdl.handle.net/2324/7172111

  • Forcing, Transition Algebras, and Calculi 査読 国際誌

    #Go Hashimoto, Daniel Găină, Ionuţ Ţuţu

    51st EATCS International Colloquium on Automata, Languages and Programming, ICALP 2024   2024年5月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    We bring forward a logical system of transition algebras that enhances many-sorted first-order logic using features from dynamic logics. The sentences we consider include compositions, unions, and transitive closures of transition relations, which are treated similarly to the actions used in dynamic logics in order to define necessity and possibility operators. This leads to a higher degree of expressivity than that of many-sorted first-order logic. For example, one can finitely axiomatize both the finiteness and the reachability of models, neither of which are ordinarily possible in many-sorted first-order logic. We introduce syntactic entailment and study basic properties such as compactness and completeness, showing that the latter does not hold when standard finitary proof rules are used. Consequently, we define proof rules having both finite and countably infinite premises, and we provide conditions under which completeness can be proved. To that end, we generalize the forcing method introduced in model theory by Robinson from a single signature to a category of signatures, and we apply it to obtain a completeness result for signatures that are at most countable.

  • Omitting Types Theorem in hybrid dynamic first-order logic with rigid symbols 査読 国際誌

    Daniel Găină, Guillermo Badia, Tomasz Kowalski

    Annals of Pure and Applied Logic   174 ( 3 )   2023年3月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    In the the present contribution, we prove an Omitting Types Theorem (OTT) for an arbitrary fragment of hybrid dynamic first-order logic with rigid symbols (i.e. symbols with fixed interpretations across worlds) closed under negation and retrieve. The logical framework can be regarded as a parameter and it is instantiated by some well-known hybrid and/or dynamic logics from the literature. We develop a forcing technique and then we study a forcing property based on local satisfiability, which lead to a refined proof of the OTT. For uncountable signatures, the result requires compactness, while for countable signatures, compactness is not necessary. We apply the OTT to obtain upwards and downwards Lowenheim-Skolem theorems for our logic, as well as a completeness theorem for its constructor-based variant.

    DOI: https://doi.org/10.1016/j.apal.2022.103212

  • Robinson consistency in many-sorted hybrid first-order logics 査読 国際誌

    Daniel Găină, Guillermo Badia, Tomasz Kowalski

    Advances in Modal Logic 2022, AiML 2022, Rennes, August 22-25   2022年8月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    In this paper we prove a Robinson consistency theorem for a class of many-sorted hybrid logics as a consequence of an Omitting Types Theorem. An important corollary of this result is an interpolation theorem.

  • Lindström’s theorem, both syntax and semantics free 査読 国際誌

    Daniel Găină, Tomasz Kowalski

    Journal of Logic and Computation   32 ( 5 )   942 - 975   2022年7月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    Lindström’s theorem characterizes first-order logic in terms of its essential model theoretic properties. One cannot gain expressive power extending first-order logic without losing at least one of compactness or downward Löwenheim–Skolem property. We cast this result in an abstract framework of institution theory, which does not assume any internal structure either for sentences or for models, so it is more general than the notion of abstract logic usually used in proofs of Lindström’s theorem; indeed, it can be said that institutional model theory is both syntax and semantics free. Our approach takes advantage of the methods of institutional model theory to provide a structured proof of Lindström’s theorem at a level of abstraction applicable to any logical system that is strong enough to describe its own concept of isomorphism and its own concept of elementary equivalence. We apply our results to some logical systems formalized as institutions and widely used in computer science practice.

    DOI: https://doi.org/10.1093/logcom/exab073

  • Fraïssé-Hintikka Theorem in institutions 査読 国際誌

    Daniel Găină, Tomasz Kowalski

    Journal of Logic and Computation   30 ( 7 )   1377 - 1399   2020年10月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    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.

    DOI: https://doi.org/10.1093/logcom/exaa042

    その他リンク: https://academic.oup.com/logcom/article-abstract/30/7/1377/5900766

  • Stability of termination and sufficient-completeness under pushouts via amalgamation 査読 国際誌

    Daniel Găină, Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi

    Theoretical Computer Science   848   82 - 105   2020年9月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    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.

    DOI: https://doi.org/10.1016/j.tcs.2020.09.024

    その他リンク: https://www.sciencedirect.com/science/article/pii/S0304397520305235?via%3Dihub

  • Birkhoff Completeness for Hybrid-Dynamic First-Order Logic

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

    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   277 - 293   2019年8月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(その他学術会議資料等)  

    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.

    DOI: 10.1007/978-3-030-29026-9_16

  • Specification and Verification of Invariant Properties of Transition Systems

    Daniel Gaina, Ionut Tutu, Adrian Riesco

    25th Asia-Pacific Software Engineering Conference, APSEC 2018 Proceedings - 25th Asia-Pacific Software Engineering Conference, APSEC 2018   99 - 108   2018年7月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(その他学術会議資料等)  

    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.

    DOI: 10.1109/APSEC.2018.00024

  • Birkhoff style calculi for hybrid logics 査読 国際誌

    Daniel Găină

    Formal Aspects of Computing   29 ( 5 )   805 - 832   2017年9月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    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.

    DOI: 10.1007/s00165-016-0414-y

  • Downward Löwenheim-Skolem Theorem and interpolation in logics with constructors 招待 査読 国際誌

    Daniel Găină

    Journal of Logic and Computation   27 ( 6 )   1717 - 1752   2017年9月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    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.

    DOI: 10.1093/logcom/exv018

  • Foundations of logic programming in hybrid logics with user-defined sharing 査読 国際誌

    Daniel Găină

    Theoretical Computer Science   686   1 - 24   2017年7月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    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.

    DOI: 10.1016/j.tcs.2017.04.009

  • Initial semantics in logics with constructors 査読 国際誌

    Daniel Găină, Kokichi Futatsugi

    Journal of Logic and Computation   25 ( 1 )   95 - 116   2015年9月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    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.

    DOI: 10.1093/logcom/exs044

  • Foundations of logic programming in hybridised logics

    Daniel Găină

    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   69 - 89   2015年1月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(その他学術会議資料等)  

    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.

    DOI: 10.1007/978-3-319-28114-8_5

  • Proving sufficient completeness of constructor-based algebraic specifications 査読

    Masaki Nakamura, Daniel Gaina, Kazuhiro Ogata, Kokichi Futatsugi

    Lecture Notes in Electrical Engineering   373   15 - 21   2015年1月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    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.

    DOI: 10.1007/978-981-10-0281-6_3

  • Forcing, Downward Löwenheim-Skolem and Omitting Types Theorems, Institutionally 査読

    Daniel Mircea Gaina

    Logica Universalis   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.

    DOI: 10.1007/s11787-013-0090-0

  • On automation of OTS/CafeOBJ method 査読

    Daniel Gǎinǎ, Dorel Lucanu, Kazuhiro Ogata, Kokichi Futatsugi

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)   8373   578 - 602   2014年1月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    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.

    DOI: 10.1007/978-3-642-54624-2_29

  • Constructor-based inductive theorem prover

    Daniel Gǎinǎ, Min Zhang, Yuki Chiba, Yasuhito Arimoto

    5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013 Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings   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.

    DOI: 10.1007/978-3-642-40206-7-26

  • Interpolation in logics with constructors 査読

    Daniel Gǎinǎ

    Theoretical Computer Science   474   46 - 59   2013年2月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    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.

    DOI: 10.1016/j.tcs.2012.12.002

  • Principles of proof scores in CafeOBJ 招待 査読 国際誌

    Kokichi Futatsugi, Daniel Găină, Kazuhiro Ogata

    Theoretical Computer Science   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.

    DOI: 10.1016/j.tcs.2012.07.041

  • Constructor-based logics 査読

    Daniel Gǎinǎ, Kokichi Futatsugi, Kazuhiro Ogata

    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.

  • Completeness by forcing 査読 国際誌

    Daniel Găină, Marius Petria

    Journal of Logic and Computation   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.

    DOI: 10.1093/logcom/exq012

  • Constructor-based institutions

    Daniel Gǎinǎ, Kokichi Futatsugi, Kazuhiro Ogata

    3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2009 Algebra and Coalgebra in Computer Science - Third International Conference, CALCO 2009, Proceedings   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.

    DOI: 10.1007/978-3-642-03741-2_27

  • Birkhoff completeness in institutions 査読 国際誌

    Mihai Codescu, Daniel Găină

    Logica Universalis   2 ( 2 )   277 - 309   2008年9月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    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.

    DOI: 10.1007/s11787-008-0035-1

  • 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) 査読

    Daniel Gǎinǎ, Andrei Popescu

    Journal of Logic and Computation   17 ( 3 )   2007年6月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.1093/logcom/exm022

  • An institution-independent proof of the Robinson Consistency Theorem 査読 国際誌

    Daniel Găină, Andrei Popescu

    Studia Logica   85 ( 1 )   41 - 73   2007年2月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    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.

    DOI: 10.1007/s11225-007-9022-4

  • An institution-independent generalization of Tarski's elementary chain theorem 査読

    Daniel Gǎinǎ, Andrei Popescu

    Journal of Logic and Computation   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.

    DOI: 10.1093/logcom/exl006

▼全件表示

講演・口頭発表等

  • Forcing and its applications in hybrid logics 招待 国際会議

    Daniel Găină

    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年7月 

     詳細を見る

    開催年月日: 2020年6月 - 2020年7月

    記述言語:英語  

    開催地:"Dunărea de Jos" University of Galati   国名:ルーマニア  

    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.

    その他リンク: https://sites.google.com/view/congmatro9/home

  • Birkhoff style proof systems for hybrid-dynamic quantum logic 招待 国際会議

    Daniel Găină

    Formal verification of quantum circuits/protocols/programs, Japan Advanced Institute for Science and Technology  2024年1月 

     詳細を見る

    開催年月日: 2024年1月

    記述言語:英語   会議種別:シンポジウム・ワークショップ パネル(公募)  

    国名:日本国  

    We explore a simple approach to quantum logic based on hybrid and dynamic modal logic, where the set of states is given by some Hilbert space. In this setting, a notion of quantum clause is proposed in a similar way the notion of Horn clause is advanced in first-order logic, that is, to give logical properties for use in logic programming and formal specification. We propose proof rules for reasoning about quantum clauses and we investigate soundness and compactness properties that correspond to this proof calculus. Then we prove a Birkhoff completeness result for the fragment of hybrid- dynamic quantum logic determined by quantum clauses.

  • Initiality in Hybrid-Dynamic Quantum Logic 招待 国際会議

    Daniel Găină

    Cracow Logic Conference (CLoCk)  2023年6月 

     詳細を見る

    開催年月日: 2023年6月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Department of Logic, Institute of Philosophy, Jagiellonian University, Kraków   国名:ポーランド共和国  

  • Robinson consistency in many-sorted hybrid first-order logics 国際会議

    Daniel Găină

    Advances in Modal Logic, AiML 2022  2022年8月 

     詳細を見る

    開催年月日: 2022年8月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Institute for Research in Computer Science and Random Systems, Rennes   国名:フランス共和国  

  • Stability of termination under pushouts via amalgamation 国際会議

    Daniel Găină

    Australian and New Zealand Industrial and Applied Mathematics  2022年2月 

     詳細を見る

    開催年月日: 2022年2月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:online   国名:オーストラリア連邦  

    その他リンク: https://anziam2022.com.au

  • Omitting Types Theorem in hybrid-dynamic first-order logic with rigid symbols 国際会議

    Daniel Găină

    Mathematical Society of Japan  2021年9月 

     詳細を見る

    開催年月日: 2021年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:online   国名:日本国  

    その他リンク: https://www.mathsoc.jp/en/meeting/chiba21sept/

  • Stability of termination under pushouts via amalgamation

    Daniel Găină

    32nd Seminar on Algebra, Logic and Geometry in Informatics (ALGI)  2021年9月 

     詳細を見る

    開催年月日: 2021年9月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:online   国名:日本国  

  • Omitting Types Theorem in hybrid-dynamic first-order logic with rigid symbols 国際会議

    Daniel Găină

    The Australasian Association for Logic  2021年6月 

     詳細を見る

    開催年月日: 2021年6月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:online   国名:オーストラリア連邦  

    その他リンク: https://blogs.unimelb.edu.au/logic/aal-2021/

  • Forcing and Calculi for Hybrid Logics 国際会議

    Daniel Găină

    Australasian Logic Group  2020年12月 

     詳細を見る

    開催年月日: 2020年12月

    記述言語:英語  

    開催地:online   国名:日本国  

  • Specification and Verification of Invariant Properties of Transition Systems 国際会議

    Daniel Găină

    25th Asia-Pacific Software Engineering Conference (APSEC 2018)  2018年12月 

     詳細を見る

    開催年月日: 2020年11月

    記述言語:英語  

    国名:日本国  

  • Forcing and Calculi for Hybrid Logics

    Daniel Găină

    31st Seminar on Algebra, Logic and Geometry in Informatics (ALGI)  2020年9月 

     詳細を見る

    開催年月日: 2020年9月

    記述言語:英語  

    国名:日本国  

    その他リンク: https://sites.google.com/site/algimeeting/home/31/program

  • Specification and Verification of Invariant Properties of Transition Systems 招待 国際会議

    Daniel Găină

    Working Formal Methods Symposium (FROM 2017)  2017年7月 

     詳細を見る

    開催年月日: 2020年7月

    記述言語:英語   会議種別:口頭発表(一般)  

    開催地:Bucharest   国名:ルーマニア  

    その他リンク: http://unibuc.ro/~conference/from2017/#2

  • Horn Clauses in Hybrid-Dynamic First-Order Logic

    Daniel Găină

    The 15th Theorem Proving and Provers meeting (TPP 2019)  2019年11月 

     詳細を見る

    開催年月日: 2019年11月

    記述言語:英語  

    開催地:National Institute of Informatics   国名:日本国  

    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.

    その他リンク: https://akihisayamada.github.io/tpp2019/

  • Birkhoff Completeness for Hybrid-Dynamic First-Order Logic

    Daniel Găină

    The 18th Logic and Computation Seminar  2019年11月 

     詳細を見る

    開催年月日: 2019年11月

    記述言語:英語  

    開催地:Nishijin Plaza, Multi-purpse Room(2-16-23 Nishijin, Sawara-ku, Fukuoka-shi)   国名:日本国  

    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.

    その他リンク: https://lcseminar.wordpress.com/2019/11/12/lcseminar18/

  • Mathematical structures for developing reconfigurable systems 国際会議

    Daniel Găină

    La Trobe - Kyushy Joint Seminar on Mathematics for Industry  2017年5月 

     詳細を見る

    開催年月日: 2017年5月

    記述言語:英語  

    国名:日本国  

▼全件表示

Works(作品等)

  • Transition Algebra Theorem Prover

    Daniel Găină, Ionuţ Ţuţu, Adrián Riesco, Go Hashimoto

    2023年10月

     詳細を見る

    Expressivity and executability are two highly desirable yet often clashing features of formal specification languages. One empowers the users of such languages to capture a broad range of applications in a natural, convenient manner, while the other is essential for rapid prototyping, as it provides immediate feedback on the functional behavior of the systems specified in this way. In general, neither can be fully achieved without sacrificing the other. This has led to modern specification languages that either enjoy the expressive power of full first-order logics or attempt to maximize expressivity while preserving executability within the bounds of some Horn-clause fragment. We have shown that, for formal verification purposes, executability and expressivity may still coexist. To this end, we present a theorem prover that combines executable specifications written in Maude—utilized both in system specification and for conducting proofs—with the expressivity of transition algebra, a logical system built by enhancing many-sorted first-order logic with features of dynamic logic. To illustrate the approach and the benefits of having an executable basis for formal verification, we explored Robin Milner’s calculus of communicating systems—a process calculus that enables syntactic descriptions of concurrent systems to be written, manipulated, and analyzed.

  • Constructor-based Interractive Theorem Prover

    Daniel Găină, Ionuţ Ţuţu, Adrián Riesco

    2018年12月

     詳細を見る

    The Constructor-based Inductive Theorem Prover (CITP) is a proof management tool built on top of a variation of conditional equational logic enhanced with many modern features.
    The tool consists of two parts:
    - the core, which implements proof tactics, and
    - the user interface, which implements the parser, displays the results, and defines commands through which users can interact with the tool.

所属学協会

  • 日本数学会

学術貢献活動

  • Program Committee member 国際学術貢献

    International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols FAVPQC 2022  ( Madrid Spain ) 2022年10月

     詳細を見る

    種別:大会・シンポジウム等 

  • 学術論文等の審査

    役割:査読

    2022年

     詳細を見る

    種別:査読等 

    国際会議録 査読論文数:1

    国内会議録 査読論文数:3

  • 学術論文等の審査

    役割:査読

    2021年

     詳細を見る

    種別:査読等 

    国際会議録 査読論文数:1

    国内会議録 査読論文数:3

  • Programme Committee member 国際学術貢献

    8th Conference on Algebra and Coalgebra in Computer Science CALCO 2019  ( London UnitedKingdom ) 2019年6月

     詳細を見る

    種別:大会・シンポジウム等 

  • 学術論文等の審査

    役割:査読

    2019年

     詳細を見る

    種別:査読等 

    外国語雑誌 査読論文数:1

    国際会議録 査読論文数:3

    国内会議録 査読論文数:3

共同研究・競争的資金等の研究課題

  • A theorem prover for the correct development of reconfigurable systems 国際共著

    2023年4月 - 2027年4月

      詳細を見る

    担当区分:研究代表者 

  • A theorem prover for the correct development of reconfigurable systems

    研究課題/領域番号:60050  2023年 - 2026年

    日本学術振興会  科学研究費助成事業  基盤研究(C)

      詳細を見る

    担当区分:研究代表者  資金種別:科研費

  • Mathematical foundations for the reconfiguration paradigm 国際共著

    2020年4月 - 2024年3月

      詳細を見る

    担当区分:研究代表者 

  • Mathematical foundations for the reconfiguration paradigm

    研究課題/領域番号:12030  2020年 - 2024年

    日本学術振興会  科学研究費助成事業  基盤研究(C)

      詳細を見る

    担当区分:研究代表者  資金種別:科研費

  • The relationship between gaining expressive power in extending first-order logics and losing 'control' over the extension 国際共著

    2018年4月 - 2021年3月

      詳細を見る

    担当区分:研究代表者 

    The purpose of this project is to complete the work started by Lindstrom on the expressivity of first-order logic by making his result not only syntactic-free but also semantic-free in the spirit of abstract model theory.

教育活動概要

  • I have taught a variety of applied mathematical subjects such as algebraic specification, model theoretic topics for the design of specification and verification languages, or term rewriting. I organize lectures in collaboration with other universities such as La Trobe University. I also supervise graduate research students.

担当授業科目

  • 情報数学特論1

    2024年10月 - 2025年3月   後期

  • 数理科学特論19

    2024年4月 - 2024年9月   前期

  • MMA数学特論II

    2024年4月 - 2024年9月   前期

  • 数学共創概論Ⅱ

    2023年10月 - 2024年3月   後期

  • 機能数理学概論Ⅰ

    2023年10月 - 2024年3月   後期

  • MMA数学特論II

    2023年10月 - 2024年3月   後期

  • 数理科学特論19

    2023年10月 - 2024年3月   後期

  • 数学共創概論Ⅱ

    2023年10月 - 2024年3月   後期

  • 機能数理学概論Ⅰ

    2023年10月 - 2024年3月   後期

  • MMA数学特論II

    2023年10月 - 2024年3月   後期

  • 数理科学特論19

    2023年10月 - 2024年3月   後期

  • 数学創発モデリング

    2023年4月 - 2024年3月   通年

  • 数学創発モデリング

    2023年4月 - 2024年3月   通年

  • 計算数理学Ⅰ

    2023年4月 - 2023年9月   前期

  • ルベーグ積分

    2023年4月 - 2023年9月   前期

  • 計算数理学Ⅰ

    2023年4月 - 2023年9月   前期

  • ルベーグ積分

    2023年4月 - 2023年9月   前期

  • Functional Mathematics I

    2022年10月 - 2023年3月   後期

  • Functional Mathematics I

    2022年10月 - 2023年3月   後期

  • 数学共創概論Ⅱ

    2022年10月 - 2023年3月   後期

  • 機能数理学概論Ⅰ

    2022年10月 - 2023年3月   後期

  • MMA数学特論II

    2022年10月 - 2023年3月   後期

  • 数理科学特論19

    2022年10月 - 2023年3月   後期

  • 数学共創モデリング

    2022年4月 - 2023年3月   通年

  • 数学共創モデリング

    2022年4月 - 2023年3月   通年

  • Topics in Computational Mathematics I

    2022年4月 - 2022年9月   前期

  • Topics in Computational Mathematics I

    2022年4月 - 2022年9月   前期

  • Topics in Computational Mathematics I

    2022年4月 - 2022年9月   前期

  • 計算数理学Ⅰ

    2022年4月 - 2022年9月   前期

  • 計算数理学Ⅰ

    2022年4月 - 2022年9月   前期

  • 応用数学A

    2022年4月 - 2022年9月   前期

  • 機能数理学概論Ⅰ

    2021年10月 - 2022年3月   後期

  • MMA数学特論II

    2021年10月 - 2022年3月   後期

  • 数理科学特論19

    2021年10月 - 2022年3月   後期

  • 機能数理学概論Ⅰ

    2021年10月 - 2022年3月   後期

  • MMA数学特論II

    2021年10月 - 2022年3月   後期

  • 数理科学特論19

    2021年10月 - 2022年3月   後期

  • 機能数理学概論Ⅰ

    2021年10月 - 2022年3月   後期

  • MMA数学特論II

    2021年10月 - 2022年3月   後期

  • 数理科学特論19

    2021年10月 - 2022年3月   後期

  • 計算数理学Ⅰ

    2021年4月 - 2021年9月   前期

  • 応用数学A

    2021年4月 - 2021年9月   前期

  • 計算数理学Ⅰ

    2021年4月 - 2021年9月   前期

  • 応用数学A

    2021年4月 - 2021年9月   前期

  • 計算数理学Ⅰ

    2021年4月 - 2021年9月   前期

  • 応用数学A

    2021年4月 - 2021年9月   前期

  • [M2]Topics in Computational Mathematics I

    2021年4月 - 2021年9月   前期

  • [M2]計算数理学Ⅰ

    2021年4月 - 2021年9月   前期

  • MMA数学特論Ⅱ

    2020年10月 - 2021年3月   後期

  • 数理科学特論19

    2020年10月 - 2021年3月   後期

  • 機能数理学概論Ⅰ

    2020年4月 - 2020年9月   前期

  • 応用数学Ⅱ

    2020年4月 - 2020年9月   前期

  • MMA数学入門

    2020年4月 - 2020年9月   前期

  • MMA数学入門

    2020年4月 - 2020年9月   前期

  • MMA数学入門

    2020年4月 - 2020年9月   前期

▼全件表示

その他教育活動及び特記事項

  • 2023年  学友会・同好会等の指導  I am involved in organizing a soccer circle/club open to both international and Japanese students

社会貢献・国際連携活動概要

  • I am involved in research collaborations with European and Australian academics as well as with Japanese researchers.
    I organize an online seminar for the development of a software tool for the specification and verification of reconfigurable systems. My collaborators for this project are Adrian Riesco (Complutense University of Madrid) and Ionut Tutu (Institute of Mathematics of the Romanian Academy).
    I work with Tomasz Kowalski (Jagiellonian University, Poland) and Guillermo Badia (The University of Queensland) on a project where we study the relationship between gaining expressive power in extending first-order logics and losing 'control' over the extension.
    I am involved in the organization of joint research seminars with Mathematics and Statistics Department of La Trobe University.

政策形成、学術振興等への寄与活動

  • 2018年2月   Co-organized by the Institute of Mathematics for Industry at Kyushu University and La Trobe University

    Main organizer of the international “Workshop on Logic, Algebra and Category Theory”, Melbourne, February 12-16, 2018

海外渡航歴

  • 2022年8月 - 2022年9月

    滞在国名1:ルーマニア   滞在機関名1:Institute of Mathematics of the Romanian Academy

  • 2022年8月

    滞在国名1:フランス共和国   滞在機関名1:The french laboratory for research and innovation in digital science and technology (IRISA)

学内運営に関わる各種委員・役職等

  • 2023年4月 - 2024年4月   部門 Auditorium Committee member

  • 2022年4月 - 2024年4月   部門 University Archives Committee member

  • 2022年4月 - 2024年4月   部門 Secretary of International Advisory Board

  • 2022年4月 - 2024年4月   部門 Secretary of International Project Committee