Go to Logic in Informatics Home Page


Here You can find short information about projects, which are being developed by the Group Members:
  1. 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 well-known 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 semantic-syntactic 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.

  2. 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 computer-made proof step, EA information environment having an influence on a current evidence of computer-made proof step, and interactive man-assistant search of proof.
    Project Leader: Alexander V. Lyaletski (Kiev National University)
    Project Members:Konstantine P. Verchinine (Universite Paris-XII 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

  3. BaCoN

    Project Name:Composition-Nominative 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 beta-version testing stage
    Applications:Tools developed may be used for formal development of software, requirements description, program systems correctness proof and software properties verification