Карта сайта

(Рубрикация сайта на основе меню)

Основные разделы меню Разделы второго уровня Содержание и краткое описание пунктов меню
Алфавиты  Граф алфавитов VRML-граф всех алфавитов из БД
 Интерактивная работа с БД Форма для формирования запроса к БД об алфавитах
Пропозициональные алфавиты содержание раскрывающегося списка:  VRML-граф пропозициональных алфавитов
Список пропозициональных алфавитов из БД
Таблица включения алфавитов друг в друга
Бескванторные силлогистические алфавиты содержание раскрывающегося списка:  VRML-граф силлогистических алфавитов
Список силлогистических алфавитов из БД
Таблица включения алфавитов друг в друга
Бескванторные алгебраические алфавиты содержание раскрывающегося списка:  VRML-граф алгебраических алфавитов
Список алгебраических алфавитов из БД
Таблица включения алфавитов друг в друга
Алфавиты кванторных теорий содержание раскрывающегося списка:  VRML-граф кванторных алфавитов
Список кванторных алфавитов из БД
Классы термов  Граф классов термов VRML-граф всех классов термов из БД
 Интерактивная работа с БД Форма для формирования запроса к БД о классах термов
Список термов содержание раскрывающегося списка: Список классов термов из БД
Таблица включения классов термов друг в друга
Языки  Структурное представление языков Форма для выбора языка и его представления в виде иерархического графа объектов
 Граф языков VRML-граф всех языков из БД
 Интерактивная работа с БД Форма для формирования запроса к БД о языках
Пропозициональные языки содержание раскрывающегося списка:  VRML-граф пропозициональных языков
Список пропозициональных языков из БД
Таблица включения классов термов друг в друга
Бескванторные силлогистические языки содержание раскрывающегося списка:  VRML-граф силлогистических языков
Список силлогистических языков из БД
Таблица включения языков друг в друга
Бескванторные алгебраические языки содержание раскрывающегося списка:  VRML-граф алгебраических языков
Список алгебраических языков из БД
Таблица включения классов термов друг в друга
Языки кванторных теорий содержание раскрывающегося списка:  VRML-граф кванторных языков
Список кванторных языков из БД
Классификация языков по классу термов (VRML-графы) содержание раскрывающегося списка: Список групп языков с одним и тем же классом ППТ. Пункты меню служат ссылками на VRML-графы этих групп.
Описание и классификация теорий  Структурное представление теорий Форма для выбора теории и ее представления в виде иерархического графа объектов
 Интерактивная работа с БД Форма для формирования запроса к БД о теориях
Пропозициональные теории содержание раскрывающегося списка:  VRML-граф различных формализаций, фрагментов и расширений классической логики высказываний
 VRML-граф импликативных пропозициональные логики (по А.С.Карпенко)
Список пропозициональных теорий из БД
Бескванторные силлогистические теории содержание раскрывающегося списка:  VRML-граф силлогистик в языке LSa,e,i и их подтеории
 VRML-граф чистых негативных силлогистик А.А.Ильина
 VRML-граф расширений С2 в других языках
Список силлогистических теорий из БД
Бескванторные алгебраические теории содержание раскрывающегося списка:  VRML-граф алгебраических теорий из БД
Список алгебраических теорий из БД
Кванторные теоории содержание раскрывающегося списка:  VRML-граф кванторных теорий из БД
Статья "Формализация фрагмента Части I Этики Спинозы" (А.Блюм и С.Малинович, пер. с англ. Т.А.Шиян)
Список кванторных теорий из БД
Классификация теорий по языку содержание раскрывающегося списка: Список классов эквивалентности теорий по языку. Пункты меню служат гиперссылками на VRML-графы, представляющие соотношение теорий по дедуктивной силе внутри каждой группы
Классификация теорий по классу термов содержание раскрывающегося списка: Список классов эквивалентности теорий по классу термов. Пункты меню служат гиперссылками на VRML-графы, представляющие соотношение теорий по дедуктивной силе внутри каждой группы
Некоторые классы индуктивной взаимопогружаемости содержание раскрывающегося списка: Гипотетическое соотношение классов взаимопогружаемости CS, TS, Eq, BA и US1
Соотношение по дeдуктивной силе теорий класса CS (классическая силлогистика)
Соотношение по дeдуктивной силе теорий класса TS (традиционная силлогистика)
Соотношение по дeдуктивной силе теорий класса Eq (бескванторная теория равенства)
Соотношение по дeдуктивной силе теорий класса US1 (обобщенная силлогистика 1)
Соотношение по дeдуктивной силе теорий класса BA (бескванторная булева алгебра)
Дополнительные возможности содержание раскрывающегося списка: Форма для выбора теории и генерации на основе данных из БД статьи в LaTeX про выбранную теорию
Поиск альтернативных имен теорий
 Справочник по формальным реконструкциям силлогистических учений (Работы запланированы на 2006 год.)
Дедукция (NEW!) О проекте Дедукция на theo.ru О планах развития раздела Дедукция
Поиск формул, доказуемых в выбранной теории Форма для выбора теорий и поиска доказуемых в нихъ формул
Схемы аксиом с описанием и поиск теорий, в которых доказуема выбранная формула Список схем формул, использованных в БД для аксиоматического определения теорий, их интерпретация (для некоторых формул) и поиск теорий, в которых доказуема выбранная формула
Поиск подтеорий и расширений теорий Форма для поиска подтеорий и расширений теорий из БД
Ресурсы в сети содержание раскрывающегося списка: Online-cистема автоматического построения доказательств в классической логике высказываний (философский факультет МГУ)
Программы автоматического поиска теорем Otter и автоматического поиска конечных моделей MACE, created at Argonne National Laboratory.
База данных существующих систем автоматического доказательства теорем и т.п.
Коллекция web-ориентированных программ интерактивного и автоматического доказательства теорем, построения выводов и т.п.
Еще коллекция ссылок на подобные ресурсы
Литература  Лексический поиск по литературе Форма контекстного поиска по таблице литературы
 Поиск библиографии по формальным теориям Форма для поиска библиографии по формальным теориям
 Сравнение формальных теорий: основные источники Список основных источников, использованных при наполнении БД
 Публикации по проекту Список публикаций по проекту с возможностью скачать тексты
Глоссарий Глоссарий Толковый словарь логических понятий, встречающихся в описаниях из БД, и математических понятий, относящихся к положенной в основу данного комплекса теории
Лексический поиск по глоссарию Форма для осуществления контекстного поиска по глоссарию
Теоретическая справка Метаязык описания теорий Использованные в БД обозначения при описании классов термов, языков и теорий
Интерпретация символов алфавитов из БД Список символов алфавитов из БД (кроме алфавита реконструкции Спинозы) с их содержательной интерпретацией
Принципы построения индексов алфавитов, классов термов, языков и теорий в базе данных Принципы построения в базе данных индексов и других обозначений для алфавитов, классов термов, языков и теорий
Не решенные проблемы Описание задач, вставших при построении ИС и пока не решенных
Справка по сайту Титульная страница Ссылка на первую страницу сайта
 Как работать с системой Краткое описание возможных способов работы с нашим информационно-справочным комплексом и доступных сервисов
 Карта сайта Ссылка на настоящую страничку
Основные обновления Список основных обновлений сайта
Рабочая группа проекта О рабочей группе проекта. Контактная информация
Планируемые обновления Планы дальнейшего развития и обновления сайта