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

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

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

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

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

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

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