- Exploring the problem of formalization of reasoning and decision making in cases when knowledge is incomplete and/or uncertain or too large and complex to be analyzed
- Development and adaptation of logical systems used for to formalization of intelligent reasoning; examination of soundness, completeness, decidability and complexity problems
- Designing efficient algorithms for theorem provers, satisfiability checkers, approximate inference engines, and building programming environments that use these algorithms

Diversity and complexity of problems that people solve using computers, especially in the Internet era, requires high quality programming tools. Incorporating elements of human intelligence into software helps in developing programming systems capable for autonomous work and decision making in complex, fuzzy and/or incompletely described real-world situations. Formal mathematical logic systems are universal specification languages and powerful tools for description od human knowledge, in particular in the fields of qualitative and quantitative modeling of uncertainty, beliefs, decision etc. Investigations and applications of these logics give a theoretical base for intelligent software development, e.g., databases and Internet agents, able to work autonomously in complex and unpredictable environments. Algebraic and fuzzy methods, as well as neural networks are used in optimization of decision diagrams, in signal processing and design, reliability evaluation and testing of digital systems.

The following problems will be investigated:

- completeness, decidability, complexity and some other features of some logics
- conservative generalization of classical to (0,1)-valued logic and applications
- adding new operators (probabilistic, fuzzy) in logics
- development applications and adaptation of different proof procedures and satisfiability checkers
- systematic search for finite models and countermodels
- Boole's and Post's equitations, their general and reproductive solutions and relationships between them,
- analysis of algorithms, and possibilities for improving their efficiency
- applications of the developed procedures to real fields, algebraic and the other formal theories, functional equalities
- algebraic theory of semigroups and its application in the automata theory
- neural networks, algebraic and hybrid methods and their applications in control, design, risk analysis and testing of digital systems
- development of software for approximative reasoning, theorem provers based on the tableau and some related methods, WWW-learning systems, intelligent agents

New results are expected in theoretical analysis as well as development of various formal systems of mathematical logic, and related software.

- semantical and proof theoretical analysis of logical systems supporting reasoning in real-world situations
- developing efficient complete and semi-complete decision procedures, and approximate reasoning procedures and algorithms for manipulation and analysis of decision diagrams,
- including formal procedures into programming environments that allow applications in scientific and the other fields.
- organizing conferences and seminars with the corresponding subjects

This project considers interdisciplinary topics that belong to the border between mathematical logic and artificial intelligence. There are many similar research projects worldwide often financially supported by industry. That leads to exploitation of intelligent software in real-world environment – from Windows operating system to autonomous systems for manufacture control, software and hardware verification, signal processing and system design. Commemorating the 50th anniversary of Association for Computing Machinery, two volumes of Computing surveys were published (vol. 28, nr. 4,5, 1996.). Problems to be investigated in this project were mentioned among other strategic directions in computing research.

The research in this field started in 70's with dr M.Kapetanović's papers about tableaux, and the system "Graph" developed by prof. D.Cvetković's group. Further research has been mostly done trough the seminars and projects at Mathematical institute. The M.Kapetanović's and dr A.Krapež's group developed dual tableau method and implemented it in some theorem provers. Prof. Rašković's group achived remarkable results about probability logic. P.Janičić's PhD thesis deals with strategies for building decision procedures into automated reasoning systems. Dr D.Radojević examines multivalued (0,1)-logic as a mathematical base for fuzzy logic. Prof. S.Prešić discovered reproductivity method, a new procedure for functional and Boolean equitations solving, further developed by A.Krapež and prof. D.Banković. The group lead by prof. R.Stanković and prof. M.Stanković investigates methods for control, designing and testing of digital systems

The methods of Mathematical logic can be used as a base for inference engine in intelligent systems, like expert systems, decision making systems, and systems for reliability evaluation. These system can be used as assistant tools in many sciences, for instance in archaeology and law.

Algorithms for manipulation and calculations with decision diagrams can be used as a basis for development of many efficient algorithms for signal processing and system design and related applications. The application of decision diagrams permits to overcome restrictions imposed by the exponential complexity of the corresponding algorithms, as for example FFT-like algorithms.