# UNIVERSAL LOGIC METHODS IN COMPUTER SCIENCE

#### project PN-II-ID-PCE-2011-3-0439,
funded by UEFISCDI under contract 29/5.10.2011

Domain | PE.Mathematics, Physical Sciences, Information and Communication, Engineering, Universe and Earth Sciences |

Subdomain | Mathematical foundations: all areas of mathematics, pure and applied, plus mathematical foundations of computer science, mathematical physics and statistics |

- Project summary
- Members
- Publications
- Presentations in conferences
- Other dissemination activities/presentations of project's results
- Seminars and workshops organized on the theme of the project
- Doctoral theses
- Scientific Reports

## Project summary

Universal logic is a body of general theories of logical structures that respond to the recent big multiplicity of logical systems from mathematical logic and from computer science. It represents the most modern trend in mathematical logic and it is also deeply rooted in computer science. One of the major universal logic sub-areas, namely the institution theory of Goguen and Burstall, originates from algebraic specification where it has gained a paramount foundational status, with its role being spread to other logic-based computer science areas. In this project we develop a number of institution theoretic methods in formal specification and verification applicable also to other logic-based computer science areas. These include (1) a new general foundational approach to structuring and modularity of specification and programs that unifies the existing ones at a higher level of abstraction, (2) a logic-independent development of formal verification methodologies providing solid foundations for formal verifications applicable to a wide variety of specification formalisms, and (3) an institution theoretic approach to logical heterogeneity and combination of logical systems and of logic translations that addresses combination both at the syntactic and the semantic level and which constitutes foundations for combinations of logic-based computing paradigms. The significance of (3) extends into the heart of one of the hot issues in logic.

## Members

- Răzvan Diaconescu
- CS1, project director (Simion Stoilow Institute of Mathematics of the Romanian Academy – IMAR)
- Ionuț Țuțu
- PhD student (Royal Holloway University of London)
- Andrei Sipoș
- PhD student (University of Bucharest)

## Publications

- Institution Theory, Internet Encyclopedia of Philosophy (2016).
- Foundations of Graph Transformation as a Logic-Programming Language, in 23rd International Workshop on Algebraic Development Techniques (WADT 2016), (2016).
- A pushout-style approach to parameterised behavioural specifications, Theoretical Computer Science, Elsevier (submitted).
- Structuring of Specification Modules (extended), Computer Science Journal of Moldova 23(2):135-152), (2015).
- Structuring of Specification Modules, in S. Cojocaru and C. Gaindric (Eds.): Workshop on Foundations of Informatics 2015, 4-13, Institute of Mathematics and Computer Science, Academy of Sciences of Moldova volume 9463 of Lecture Notes in Computer Science
- Revisiting the Institutional Approach to Herbrand’s Theorem, in L.S. Moss and P. Sobocinski (Eds.): CALCO 2015, Leibniz International Proceedings in Informatics, 35:304-319, Schloss Dagstuhl (2015).
- Functorial Semantics of First-Order Views, Theoretical Computer Science, Elsevier http://dx.doi.org/10.1016/j.tcs.2016.09.009.
- Implicit Kripke Semantics and Ultraproducts in Stratified Institutions, J. Logic and Computation, DOI:10.1093/logcom/exw018, Oxford Univ. Press.
- M. Codescu, R. Diaconescu, I. Țuțu (Eds.): Recent Trends in Algebraic Development Techniques – 22nd International Workshop, WADT 2014, revised selected papers, volume 9463 of Lecture Notes in Computer Science, Springer (2015).
- From conventional to institution-independent logic programming, J. Logic and Computation DOI:10.1093/logcom/exv021, Oxford University Press (2015). IF2014 = 0.512 RIS2014 = 1.186
- Service-Oriented Logic Programming, Logical Methods in Computer Science, 11(3:3), (2015). IF2014 = 0.443 RIS2014 = 1.011
- The Algebra of Opposition (and universal logic interpretations), in A. Koslow and A. Buchsbaum (eds.): The Road to Universal Logic, pages 127-143, Springer Basel (2015).
- On the Existence of Translations of Structured Specifications, Information Processing Letters 115(1):15–22, Elsevier (2015). IF2013 = 0.479 RIS2013 = 1.060
- From Universal Logic to Computer Science, and back, in G. Ciobanu and D. Mery (Eds.): ICTAC 2014, Lecture Notes in Computer Science 8687:1-16, Springer (2014).
- The institution theoretic scope of logic theorems, Logica Universalis 8(3-4), Springer (2014).
- Graded consequence: an institution theoretic study, Soft Computing 18(7):1247--1267, Springer (2014). IF2013 = 1.304 RIS2013 = 0.850
- Comorphisms of structured institutions, Information Processing Letters 113:894–900, Elsevier (2013). IF2013 = 0.479 RIS2013 = 1.060
- Logical foundations of services, in A.V. Jones and N. Ng (Eds.): 2013 Imperial College Computing Student Workshop (ICCSW’13), OpenAccess Series in Informatics Dagstuhl 35:111--118, Dagstuhl Publishing (2013).
- A Logic-Programming Semantics of Services, in R. Heckel and S. Milius (Eds.): CALCO 2013, Lecture Notes in Computer Science 8089:299-313, Springer (2013).
- Foundations for structuring behavioural specifications, J. Logical and Algebraic Methods in Programming, 83(3-4):319-338, Elsevier (2014). IF2013 = 0.383 RIS2013 = 0.661
- Encoding hybridized institutions into first order logic, Mathematical Structures in Computer Science 26:745-788, Cambridge University Press (2016). IF2014 = 0.45 RIS2013 = 0.986
- Parameterisation for abstract structured specifications, Theoretical Computer Science 517:102–142, Elsevier (2014). IF2013 = 0.516 RIS2013 = 1.063
- Institutional semantics for many-valued logics, Fuzzy Sets and Systems 218:32–52, Elsevier (2013). IF2013 = 1.880 RIS2013 = 1.268
- An axiomatic approach to structuring specifications, Theoretical Computer Science 433:20–42, Elsevier (2012). IF2012 = 0.489 RIS2012 = 1.021
- Quasi-varieties and initial semantics for hybridized institutions, J. Logic and Computation 26(5):855-891, Oxford University Press (2016). IF2013 = 0.504 RIS2013 = 1.287

#### PHASE 6 (2016)

#### PHASE 5 (2015)

#### PHASE 4 (2014)

#### PHASE 3 (2013)

#### PHASE 2 (2012)

#### PHASE 1 (2011)

Note: The average publication cycle in journals of the research area of the project, from submission to actual publication, is between 1–5 years.

## Presentations in conferences (with participation funded by the project)

- Composition of specification modules: recent developments, presentation given at the 2014 Conferenceon Computational Intelligence and Software Engineering (CiSE 2014), Beijing, China, July 2014.
- The institution theoretic scope of logic theorems, presentation given at the 4th World Congress on Universal Logic, Rio de Janeiro, Brazil, April 2013.
- Theory of Institutions, tutorial given at the 4th World School on Universal Logic, Rio de Janeiro, Brazil, March/April 2013.
- A module algebra for behavioural specifications, presentation given at the 21th Workshop on Algebraic Development Techniques, Salamanca, Spain, June 2012.

#### PHASE 4 (2014)

#### PHASE 3 (2013)

#### PHASE 2 (2012)

## Other dissemination activities/presentations of project's results

- , 23rd International Workshop on Algebraic Development Techniques (WADT 2016), Nijmegen, Netherlands, June 2015. Foundations of Graph Transformation as a Logic-Programming Language
- Structuring of Specification Modules, invited talk at Workshop on Foundations of Informatics, Chișinău, Moldova, August 2015.
- Institution-independent Logic Programming, PhD thesis defense, Royal Holloway Univ. of London, England, July 2015.
- Composition of specification modules: recent developments, Workhsop of the THALES project Algebraic modeling of topological and computational structures, Athens, Greece, July 2015.
- Revisiting the Institutional Approach to Herbrand's Theorem, 6th Conference on Algebra and Coalgebra in Computer Science, Nijmegen, Netherlands, June 2015.
- From universal logic to computer science, and back, invited talk at 11th International Colloquium on Theoretical Aspects of Computing, Bucharest, Romania, September 2014.
- Solving Queries over Modular Logic Programs, 22nd International Workshop on Algebraic Development Techniques, Sinaia, Romania, September 2014.
- A Full Operational Semantics of Asynchronous Relational Networks, 22nd International Workshop on Algebraic Development Techniques, Sinaia, Romania, September 2014.
- What is a logic-programming language?, 14th Computer Science Postgraduate Research Colloquium, Egham, United Kingdom, June 2014.
- Institution theory and Applications, habilitation defense, IMAR, Romania, May 2014.
- An Institution-Independent Approach to Logic Programming, IFIP WG1.3 Meeting , Theddingworth near Leicester, January 2014.
- Logical foundations of services, 2013 Imperial College Computing Student Workshop, London, United Kingdom, September 2013.
- A logic-programming semantics of services, 5th Conference on Algebra and Coalgebra in Computer Science, Warsaw, Poland, September 2013.
- Thoughts on graded consequence, Mondrian Workshop, Aveiro, Portugal, July 2013.
- From service-oriented computing to logic programming and back, Seminar on Logic in Computer Science, Faculty of Mathematics and Computer Science, University of Bucharest, April 2013.
- Institution theory: internal logic, Logic Seminar, Institute of Mathematics of the Romanian Academy, March 2013.
- Institution theory: introduction, Logic Seminar, Institute of Mathematics of the Romanian Academy, March 2013.
- On the instantiation of parameterized specifications, 21th International Workshop on Algebraic Development Techniques, Salamanca, Spain, June 2012.
- Towards Automated Structural Induction: an institution-independent methodology, Third Romanian-Japanese Algebraic Specification Workshop, Sinaia, Romania, April 2012.
- Multiple Parameterized Specifications with Sharing, Third Romanian-Japanese Algebraic Specification Workshop, Sinaia, Romania, April 2012.

## Seminars and workshops organized on the theme of the project

- 22nd International Workshop on Algebraic Development Techniques, Sinaia, Romania, September 2014.
- Logic and Formal Specification (online regular project seminar).
- Third Romanian-Japanese Algebraic Specification Workshop, Sinaia, Romania, April 2012.

## Doctoral theses (emerged from the project)

- Foundations and Techniques for Software Reconfigurability – an institution-independent approach for specifying and reasoning about reconfigurable systems, MAP-i (joint doctoral programme in informatics of the universities Minho, Aveiro and Porto), Portugal, 2013. Winner of the IBM Scientific Award 2013.
- Institution-independent Logic Programming, Royal Holloway University of London, England 2015.