проекты


  1. Объединение математической логике, теории вычислимости и теории программирования
    Название проекта: Объединение математическая логика, теория вычислимости и теории программирования
    Цель проекта (ы): Разработка методологических принципов и формулирование основных понятий интегрированной теории;. построения и исследования математических моделей логика, вычислимость и программирования различных уровней абстракции и общности
    Краткое описание: объединение основано на известных методологических принципов развития от абстрактного к конкретному и единства логического и исторического развития. После этих принципа формального понятия составе номинативных системы определяется и исследуется. Конкретизация такие системы представляют различные формализмы учился в логике, вычислимость и программирования.
    Руководитель проекта: Николай С. Никитченко
    проекта: Степан С. Shkilnyak Тарас В. Панченко Людмила Omel’chuk Вадим Ю.. Винник
    Ход объекта: Состав именительном логику различных уровнях абстракции, были определены и исследованы. Корректность и полнота теоремы. Понятие абстрактное вычислимо был определен. Полные классы вычислимых функций различных уровней абстракции были описаны. Формальные семантико-синтаксической модели спецификации и языки программирования были определены и исследованы. Более 30 работ были опубликованы.
    применения: развития программы и проверки, требование захвата. Новые учебные курсы в области математической логики, вычислимость и программирования.
  2. САД
    Название проекта: система для автоматического вычета (САД)
    Цель проекта (ы): автоматизации математических отчислений в различных областях
    Краткое описание: Одновременное расследование формализованных языков для представления математических текстов в форме, наиболее подходящим для пользователей, формализации и эволюционного развития компьютерных сделал шаг доказательства, EA информационной среды, влияющих на современные данные компьютерного производства доказательство шаг, и интерактивный человек-помощник поиска доказательств.
    Руководитель проекта: Александр Владимирович Lyaletski (Киевский национальный университет)
    проекта: Константин П. Verchinine (Universite Paris-XII Валь-де-Марн) Андрей (Андрей) Ю.. Паскевич (Киевский национальный университет) Александр А. Lyaletsky (мл.) (Киевский национальный университет)
    Ход объекта: первая версия готова. Вы можете попробовать его на http://ea.unicyb.kiev.ua . Теперь пользовательский интерфейс и поддержка различных языков механизма разработки
    применения: Некоторые приложения САД являются:

    • распределенных автоматизированных доказательства теорем
    • верификации математических текстов
    • дистанционного обучения в математических дисциплин
    • строительство баз данных для математических теорий
  3. Бэкон
    Название проекта: Композиция-именительном программного обеспечения Языки поддержки
    Цель проекта (ы): Разработка программных средств для Состав именительном Языки (CNL)
    Краткое описание: Есть разработки программных средств для поддержки не менее трех CNL:

    • Бэкон (Основные CNL)
    • DECON (Описательная CNL = Бекон + описательные выражения новых составов через основные из них)
    • Recon (Рекурсивные CNL = DECON + рекурсивного выражения новых составов через основные из них)
    Руководитель проекта: Тарас В. Панченко
    проекта: Игорь Юрьевич. Ткачук
    Ход объекта: беконом и DECON находятся в бета-версии стадии тестирования
    применения: Инструменты, разработанные могут быть использованы для формального разработке программного обеспечения, требования к описанию, программных систем доказательства корректности и верификации программного обеспечения свойств
Новини
Дошка оголошень
Цікаві факти