Первая помощь

Что такое "Информационная система по формальным теориям Theo.ru"?
Требования к программному обеспечению
Как работать с системой?
Карта сайта

О проекте

Последние обновления
История создания и обновлений системы (2003-2005)
История создания и обновлений объединенной системы (2008)
О создателях системы

Состояние системы

Информация в БД формальных теорий
Сервисы ИС по формальным теориям
English version

Информационная система по формальным теориям Theo.ru

Что такое Информационная система по формальным теориям?

Что такое "Информационная система по формальным теориям"?

Основу системы составляет база данных формальных теорий. База данных содержит:

  • сведения о языках формальных теорий (алфавиты, множества термов, множества формул);
  • описание исчислений со схемами аксиом, задающих формальные теории;
  • библиографию по формальным теориям;
  • ряд дополнительных сведений о формальных теориях (некоторые алгебраические соотношения, сведения о разрешимости, историко-логические комментарии и т.п.);
  • сведения о соотношении формальных теорий по множеству теорем;
  • описание некоторых групп взаимопогружаемости теорий.

На основе базы данных работают различные приложения, позволяющие

  • выводить описание теорий в различных видах: описание отдельных теорий, описание всех теорий в одной таблице (с возможностью выбора отображаемых свойств теорий и списка теорий), описание отдельных свойств теорий (например, описание только алфавитов, только множеств термов, только множеств формул и т.п.);
  • выводить описание отдельных теорий в виде статьи на LaTEX;
  • представлять группы теорий в виде 3-мерных графов (на VRML), демонстрирующих соотношение теорий по множеству теорем; среди фиксированных групп: теории в одном языке, теории в одном классе взаимопогружаемости, некоторые выборочные группы по другим основаниям; предусмотрено формирование произвольных групп пользователем;
  • представлять теории и языки в виде иерархии подобъектов (3-мерные графы на VRML);
  • осуществлять некоторый аналог дедуктивного и знаниевого вывода (определять формулы, доказуемые в выбранной теории, теории, в которых доказуема выбранная формула, находить подтеории и расширения выбранной теории и др.).

Система включает глоссарий, поясняющий основные логические термины и понятия, встречающиеся в описаниях формальных теорий или положенные в основы работы информационной системы.

Имеется возможность элементарного поиска по БД.