Project 174026

Representations of logical structures and formal languages and their application in computing

Leader: Professor Silvia Ghilezan

Abstract

Mathematical logic comprises both the mathematical study of logical systems and the applications of formal logic to other areas of mathematics. Apart from its fundamental role in the development of mathematics, in the last few decades mathematical logic has become the foundation of computer science and artificial intelligence. The research in this project will be directed towards fundamental research and related relevant applications in computer science. The basic research directions will be:

The main research topics will be:

The comprehensive research team has recognised expertise and well-established international collaboration. The researchers take part in European projects, which will ensure that the project results will follow the state-of-the-art of international research.

Project Description

The research will include all of the basic areas of mathematical logic: proof theory, model theory, set theory, type theory, as well as relevant applications of logic in computer science and logical design. The project research and activities will be divided across three subprojects:

The basic research directions of the subprojects are:

(a) Representation of logical structures with applications - subproject leader Z. Petrić.

The fundamental research of all of the subprojects will be in all of the basic areas of mathematical logic: proof theory, model theory, set theory, type theory and systems for formal reasoning. Following the up-to-date achievements, in this project we will explore issues which are significant both from the theoretical point of internal development as well as by being possible tools for representing and reasoning about some important concepts in computation. These issues include: Categorical proof theory, particularly coherence results in category theory and related results in algebra, geometry and topology; Applications outside the area of logic, in the theory of polytopes and semantics of proofs; Model-theoretic and proof-theoretic analysis of systems for different fragments of intuitionistic, classical, intermediate, substructural and probabilistic logics; Procedures for approximate reasoning and systems for formal reasoning with applications to decision-making systems; Representation and classification of various infinite and finite algebraic structures; Algebraic theory of quasigroups and equations on Boolean and Post algebras.

(b) Spectral representations of discrete functions and their applications - subproject leader R. Stanković.

Many of contemporary digital systems can be viewed as implementations of a well organized series of signal processing algorithms, specifically selected and sophisticatedly interconnected to perform a complex task. The basic blocks of such systems, as well as the algorithms used, are inevitably becoming more and more complex, and the specification of interconnections among them into a meaningful entire system requires novel data structures (for instance, decision diagrams), and data processing tools based on them. To compete with the complexity, the level of abstraction in modeling and description for implementation of digital systems has to be increased. At this level, sophisticated algebraic structures are used for a precise and, at the same time, compact modeling and description of digital systems. The main task in this subarea of research within the project will be devoted to the exploiting of different algebraic structures in representation of discrete signals with applications in the modeling and design of digital systems. We plan to investigate both bit-level and word level spectral representations over different finite groups. The research task is to find which of them are best suited for certain applications.

(c) Logical and formal systems for sequential and distributed computing - subproject leader J. Pantović.

Formal systems of mathematical logic represent the theoretical foundation of computation. In practice, lambda calculus is the core calculus underlying many programming languages, while its other applications can be found in important fields, such as verification of software and complex information systems. The main objectives of this subproject will be the investigation of computational interpretations of intuitionistic, classical, substructural, intermediate and probabilistic logics. The main task of this subproject in the area of concurrency formalisms is to upgrade and analyze the existing, and to develop new formal models for distributed systems, such as web applications and services. One of the essential steps in managing distributed systems with data is the security administration. Role-based access control (RBAC) is an access control technology which relies on the notion of roles. Our research team, with the use of methods from type theory, will be designing systems for dynamic modeling of role-based access rights control within networks. We plan to further develop the existing systems, and design new ones with access control in web services. We will investigate type checking and type inference for this calculus, and study possible simplifications without losing expressiveness.

The fundamental research in subproject (a) will be coordinated with more practically oriented research in subprojects (b) and (c), which will, in turn, motivate new fundamental research. The research will be conducted using the equipment purchased in the III 044006 project of the Mathematical Institute.

Expected key results

The research in this project will be directed towards fundamental research in all basic areas of mathematical logic and related relevant applications in computer science. The expected results are:

Coherence results for categories in proof theory. Related results in algebra, geometry and topology.
New approaches to the semantics of proofs in classical logic.
Cut elimination in sequent systems and maximal segments in natural deduction systems.
Completeness, decidability and complexity of logical systems for uncertain reasoning, probabilistic, temporal and modal logics.
Cylindric and probabilistic algebras.
Characterization of partially ordered sets with probabilistic measures.
Classification of countable first-order structures.
Structural description, bands and semilattice decomposition of new classes of semigroups.
Equations and inequalities in multivalued logics, Boolean, Post and Stone algebras.
Order theory in Bishop's constructive mathematics.
The method of semantic tableaux for modal and substructural logics with applications in authomated theorem proving.
Classes of quasigroups with applications in encryption.

Modeling and description of digital systems by algebraic structures.
Spectral representations on finite groups.
Complexity of the representations.
Relation between the structure and real-life representations.
Optimization of modeling and design of digital systems and the regularity of the structures.
Fast algorithms for computations on discrete functions.

Resource control in intuitionistic logic.
Diagrammatic representation of proofs in classical and intuitionistic logic.
New interpretations of substructural, intermediate and probabilistic logics in computer science.
Termination properties of the proposed systems.
Safety and security control in distributed systems.
Role-based access control.
Type systems for communication security control.
Behavioral equivalence.

Research Relevance

The addressed topics encompass a wide range of fundamental research in mathematical logic in all of its basic areas: proof theory, model theory, set theory, type theory. The relevance of this research lies is its implementation in the foundations of computer science, programming languages, artificial intelligence, software verification, and logical design, as well as the development of new concepts in computer science, such as concurrency. The interaction between the theoretical results and the demands of the practice will be both a driving force and an important positive result of the proposed research. Active, on-going international research within all these fields illustrates the actuality of the proposed Project. The comprehensive project team, consisting of over 40 researchers, gathers together researchers from the Mathematical Institute of the Serbian Academy of Sciences and all of the four state universities in Serbia: the University of Belgrade, the University of Novi Sad, the University of Nis and the University of Kragujevac. The team has recognized expertise and well-established international collaboration. The number of early stage researchers and PhD students is significant, over 20%. Great many of the researchers in question have already taken part in many past, are involved in many current, and will be further involved in future European scientific projects, such as FP, COST, and bilateral projects, thus ensuring that the results of the project will closely follow state-of-the-art international research. The project involves three experienced external experts: S. Krstić (Intel, USA), I. Farah (University of Toronto, Canada), and V. Kuncak (EPFL, Switzerland), all of whom have begun their scientific careers in Belgrade and Novi Sad. One final important issue is the continuation and further development of international collaboration (joint research activities) with leading experts from Universite Paris 7, EPFL Laussane, the University of Toronto, the University of Torino, the University of Florence, ENS Lion, Ecole Polytechnique Paris, the McGill University Montreal, the University of Tampere, as well as with leading research institutions, such as INRIA-Sophia Antipolis, France, and companies, such as Intel, USA.