During the last decades mathematical logic has become the calculus of computer science and artificial intelligence, and also has provided foundations for many areas in that field. Following those achievements, in this project we will explore issues which are interesting both from the theoretical point of internal development and as possible tools for representing and reasoning about some important concepts in computation: geometrical representation of proofs and category theory with application to semantics of programming languages, model-theoretic and proof-theoretic examination of computer science logical systems that are suitable to give a theoretical base and to cover more and more of intelligent reasoning required in real word problems that people try to solve using computers when knowledge is incomplete and/or uncertain (for example: probability logics and conservative generalization of classical to [0,1]-valued logic), development of the corresponding complete and semi-complete decision procedures, approximate reasoning procedures, theorem provers, and the other formal reasoning systems with application to systems for decision support, representations and classifications of various algebraic structures etc.

During the last decades mathematical logic has become the calculus of computer science and artificial intelligence, and also has provided foundations for many areas in that field. Following those achievements, in this project we will explore issues which are interesting both from the theoretical point of internal development and as possible tools for representing and reasoning about some important concepts in computation:

- Representation of proofs, in particular those of substructural logics, in structures of category theory, especially structures close to geometry, application of the results obtained in normalization and in deciding equality of proofs, which is important for the semantics of programming languages.
- Development and examination of logical systems used in knowledge representation and formalization of intelligent reasoning when knowledge is incomplete and/or uncertain.
- Algebraic theories of groupoids and semigroups (and their application to the theory of automata) and systems of Boole's (in)equations and equations in Stone algebras.
- complete and semi-complete decision procedures, approximate reasoning procedures, theorem provers, and the other formal reasoning systems.

The first part of the project activities concerns mainly categorial proof theory which describes logical systems that arise in proof theory. It is particularly interesting to find concrete categories that serve as models of abstract, "syntactic", categories inspired by logic. Such categories simplify the normalization procedure for proofs, and the decision procedure for equality of proofs. These procedures, which have up to now been developed in proof theory and in the lambda calculus in a syntactical manner, are important for computer science, because starting from them one can build methods for the verification of correctness of programs. Verification of programs is a major goal in the semantics of programming languages, since the correctness of many programs cannot be empirically tested. A family of nonclassical logics called substructural logics has especially interesting categorial models, and we would concentrate on these models. Geometrical categorial models connected to skein spaces and Temperley-Lieb algebras may lead to applications in quantum mechanics. Investigations would concentrate in particular on the following topics: coherence in bicartesian categories, coherence in substructural categories, generalization of natural transformations, axiomatizations of categories of tangles of finite and infinite skein spaces, their connection with the notion of self-adjunction, Post completeness of monoids and other structures that arise in that context, and matrix representations of Temperley-Lieb algebras and braid groups. In classical model theory, work would be pursued on classification of countable first-order structures. Some of the systems to be investigated have algebraic flavor: representations and classifications of algebraic structures (groupoids, semigroups) and describing general and reproductive solutions of systems of Boole's (in)equations and equations in Stone algebras.

The second part of the project activities is related to study of systems beyond propositional and first-order classical logic which includes logics for uncertain and nonmonotonic reasoning, modal logics etc. The idea is to provide logical systems strong enough to give a theoretical base and to cover more and more of intelligent reasoning required in problems that people try to solve using computers, e.g., databases and Internet agents, able to work autonomously in complex and unpredictable environments.

Particularly, we will consider probability logics and conservative generalization of classical to [0,1]-valued logic. The probability logics extend classical logic and allow us to express statements that speak about probability of some events, and are also suitable for modeling non-monotonic reasoning. The main logical properties of those systems (completeness, decidability, complexity) will be analyzed. The problem of combining and integrating decision procedures into theorem provers will be considered. Stochastic ultra-graphs will be investigated and applied to self-organized set of distributed agents.

- Geometrization of proofs, and applications in computer science which would enable the semantics of programming languages to leave the area of syntactic methods.
- Model-theoretic and proof-theoretic analysis of various systems of non-classical logics for incomplete and/or uncertain knowledge representation and reasoning about real world situations. Development of the corresponding decision procedures. Combinations of those procedures into theorem provers and intelligent programming environments that would enable automatic connection to diverse set of inference engines and domain specific ontologies.
- Description of general and reproductive solutions of systems of Boole's (in)equations and equations in Stone algebras.
- Using discrete difference dynamical systems in generating of some models which can be applied to computer science.
- Developing algorithms and software for sequential adaptation of parameters and structures of neural networks and application to systems for decision support.