Основные разделы меню |
Разделы второго уровня |
Содержание и краткое описание пунктов меню |
Алфавиты |
Граф
алфавитов |
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-ориентированных программ интерактивного и автоматического доказательства
теорем, построения выводов и т.п. |
Еще коллекция
ссылок на подобные ресурсы |
Литература |
Лексический
поиск по литературе |
Форма контекстного поиска по таблице литературы |
Поиск
библиографии по формальным теориям |
Форма для поиска библиографии по формальным теориям |
Сравнение
формальных теорий: основные источники |
Список основных источников, использованных при наполнении
БД |
Публикации
по проекту |
Список публикаций по проекту с возможностью скачать тексты |
Глоссарий |
Глоссарий |
Толковый словарь логических понятий, встречающихся в описаниях
из БД, и математических понятий, относящихся к положенной в основу данного
комплекса теории |
Лексический поиск по глоссарию |
Форма для осуществления контекстного поиска по глоссарию |
Теоретическая справка |
Метаязык описания теорий |
Использованные в БД обозначения при описании классов термов,
языков и теорий |
Интерпретация символов
алфавитов из БД |
Список символов алфавитов из БД (кроме алфавита реконструкции
Спинозы) с их содержательной интерпретацией |
Принципы построения индексов
алфавитов, классов термов, языков и теорий в базе данных |
Принципы построения в базе данных индексов и других обозначений
для алфавитов, классов термов, языков и теорий |
Не решенные проблемы |
Описание задач, вставших при построении ИС и пока не решенных |
Справка по сайту |
Титульная страница |
Ссылка на первую страницу сайта |
Как
работать с системой |
Краткое описание возможных способов работы с нашим информационно-справочным
комплексом и доступных сервисов |
Карта
сайта |
Ссылка на настоящую страничку |
Основные обновления |
Список основных обновлений сайта |
Рабочая группа проекта |
О рабочей группе проекта. Контактная информация |
Планируемые обновления |
Планы дальнейшего развития и обновления сайта |