Language：English   Publishing type：Research paper (scientific journal)  

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

Other Link： https://academic.oup.com/logcom/article-abstract/30/7/1377/5900766

Language：English   Publishing type：Research paper (scientific journal)  

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

Other Link： https://www.sciencedirect.com/science/article/pii/S0304397520305235?via%3Dihub

Language：English   Publishing type：Research paper (other academic)  

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

Language：English   Publishing type：Research paper (other academic)  

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

Language：English   Publishing type：Research paper (scientific journal)  

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

Language：English   Publishing type：Research paper (scientific journal)  

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

Language：English   Publishing type：Research paper (scientific journal)  

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

Language：English   Publishing type：Research paper (scientific journal)  

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

Language：English   Publishing type：Research paper (other academic)  

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

Language：English   Publishing type：Research paper (scientific journal)  

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

Language：English   Publishing type：Research paper (scientific journal)  

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

Language：English   Publishing type：Research paper (scientific journal)  

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

Language：English   Publishing type：Research paper (other academic)  

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

Language：English   Publishing type：Research paper (scientific journal)  

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

Language：English   Publishing type：Research paper (scientific journal)  

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

Language：English   Publishing type：Research paper (scientific journal)  

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.

Language：English   Publishing type：Research paper (scientific journal)  

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

Language：English   Publishing type：Research paper (other academic)  

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

Language：English   Publishing type：Research paper (scientific journal)  

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

Language：English   Publishing type：Research paper (scientific journal)  

DOI： 10.1093/logcom/exm022

Language：English   Publishing type：Research paper (scientific journal)  

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

Language：English   Publishing type：Research paper (scientific journal)  

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 ⁰ 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

Event date： 2021.9

Language：English   Presentation type：Oral presentation (general)  

Venue：online   Country：Japan  

Other Link： https://www.mathsoc.jp/en/meeting/chiba21sept/

Event date： 2021.9

Language：English   Presentation type：Oral presentation (general)  

Venue：online   Country：Japan  

Event date： 2021.6

Language：English   Presentation type：Oral presentation (general)  

Venue：online   Country：Australia  

Other Link： https://blogs.unimelb.edu.au/logic/aal-2021/

Event date： 2020.12

Language：English  

Venue：online   Country：Japan  

Event date： 2020.11

Language：English  

Country：Japan  

Event date： 2020.9

Language：English  

Country：Japan  

Other Link： https://sites.google.com/site/algimeeting/home/31/program

Event date： 2020.7

Language：English   Presentation type：Oral presentation (general)  

Venue：Bucharest   Country：Romania  

Other Link： http://unibuc.ro/~conference/from2017/#2

Event date： 2019.11

Language：English  

Venue：National Institute of Informatics   Country：Japan  

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.

Other Link： https://akihisayamada.github.io/tpp2019/

Event date： 2019.11

Language：English  

Venue：Nishijin Plaza, Multi-purpse Room(2-16-23 Nishijin, Sawara-ku, Fukuoka-shi)   Country：Japan  

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.

Other Link： https://lcseminar.wordpress.com/2019/11/12/lcseminar18/

Event date： 2017.5

Language：English  

Country：Japan