 Unifying mathematical logic, computability theory and theory of programming
Project Name: 
Unifying mathematical logic, computability theory and theory of programming 
Project Goal(s): 
Development of methodological principles and formulation of the main concepts of the integrated theory;construction and investigation of mathematical models of logic, computability and programming of various levels of abstraction and generality. 
Short Description: 
The unification is based on the wellknown methodological principles of development from abstract to concrete and unity of logical and historical development. Following these principle the formal notion of composition nominative system is defined and investigated. Concretization of such systems present various formalisms studied in logic, computability and programming. 
Project Leader: 
Mykola S. Nikitchenko 
Project Members: 
Stepan S. Shkilnyak Taras V. Panchenko Ludmila Omel’chuk Vadim Yu. Vinnik 
Project Progress: 
Composition nominative logics of various abstractions levels have been defined and investigated. Soundness and completeness theorems are proved. The notion of abstract computably has been defined. Complete classes of computable functions of various abstraction levels have been described. Formal semanticsyntactic models of specification and programming languages have been defined and investigated. More than 30 papers have been published. 
Applications: 
Program development and verification, requirement capturing. New educational courses in mathematical logic, computability and programming. 
 SAD
Project Name: 
System for Automatic Deduction (SAD) 
Project Goal(s): 
Automation of mathematical deductions in different fields 
Short Description: 
Simultaneous investigations into formalized languages for presenting mathematical texts in the form most appropriate for a user, formalization and evolutional development of computermade proof step, EA information environment having an influence on a current evidence of computermade proof step, and interactive manassistant search of proof. 
Project Leader: 
Alexander V. Lyaletski (Kiev National University) 
Project Members: 
Konstantine P. Verchinine (Universite ParisXII Val de Marne) Andrey (Andrij) Yu. Paskevich (Kiev National University) Alexandre A. Lyaletsky (Jr.) (Kiev National University) 
Project Progress: 
The first version is ready. You can try it at http://ea.unicyb.kiev.ua. Now the user interface and different languages support mechanism are elaborating 
Applications: 
Some applications of SAD are:
 distributed automated theorem proving
 verification of mathematical texts
 remote training in mathematical disciplines
 construction of databases for mathematical theories

 BaCoN
Project Name: 
CompositionNominative Languages Software Support 
Project Goal(s): 
To develop the software tools for Composition Nominative Languages (CNL) 
Short Description: 
There are developing software tools for support at least three CNL:
 BaCoN (Basic CNL)
 DeCoN (Descriptive CNL = BaCoN + descriptive expressions of new compositions via basic ones)
 ReCoN (Recursive CNL = DeCoN + recursive expressions of new compositions via basic ones)

Project Leader: 
Taras V. Panchenko 
Project Members: 
Igor Yu. Tkachuk 
Project Progress: 
BaCoN and DeCoN are at the betaversion testing stage 
Applications: 
Tools developed may be used for formal development of software, requirements description, program systems correctness proof and software properties verification 
