Информационная система
по формальным теориям Theo.ru
Что такое Информационная система по формальным теориям?
Что такое "Информационная система по
формальным теориям"?
Основу системы составляет база данных формальных теорий. База
данных содержит:
сведения о языках формальных теорий (алфавиты, множества термов, множества
формул);
описание исчислений со схемами аксиом, задающих формальные теории;
библиографию по формальным теориям;
ряд дополнительных сведений о формальных теориях (некоторые алгебраические
соотношения, сведения о разрешимости, историко-логические комментарии и т.п.);
сведения о соотношении формальных теорий по множеству теорем;
описание некоторых групп взаимопогружаемости теорий.
На основе базы данных работают различные приложения, позволяющие
выводить описание теорий в различных видах: описание отдельных теорий, описание
всех теорий в одной таблице (с возможностью выбора отображаемых свойств теорий
и списка теорий), описание отдельных свойств теорий (например, описание только
алфавитов, только множеств термов, только множеств формул и т.п.);
выводить описание отдельных теорий в виде статьи на LaTEX;
представлять группы теорий в виде 3-мерных графов (на VRML), демонстрирующих
соотношение теорий по множеству теорем; среди фиксированных групп: теории
в одном языке, теории в одном классе взаимопогружаемости, некоторые выборочные
группы по другим основаниям; предусмотрено формирование произвольных групп
пользователем;
представлять теории и языки в виде иерархии подобъектов (3-мерные графы
на VRML);
осуществлять некоторый аналог дедуктивного и знаниевого вывода (определять
формулы, доказуемые в выбранной теории, теории, в которых доказуема выбранная
формула, находить подтеории и расширения выбранной теории и др.).
Система включает глоссарий, поясняющий основные логические термины и понятия,
встречающиеся в описаниях формальных теорий или положенные в основы работы информационной
системы.