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:
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.