Логические модели

1. Philosopher's Web

   Интерактивная карта философского знания, которая построена на основе Википедии. В карте есть множество метрик и параметров, благодаря которым можно по-разному визуализировать связи. Узлы в карте различаются по цвету (в зависимости от исторического периода) и размеру (в зависимости от количества связей узла с другими), данные параметры можно изменять. Кроме того, на сайте можно создавать собственные интерактивные карты, пройдя предварительную бесплатную регистрацию. Для собственного проекта доступны различные шаблоны, можно добавлять описание, тэги, импортировать информацию из других источников.

   Ссылка

   

2. Philosophy of Mind, Interactive Mind Map

   Карта философии сознания представляет визуализацию иерархий концептов, идей и направлений в философии сознания. Карта составлена на основе статьи в Википедии, посвященной философии сознания. По карте нельзя перейти на внешние ссылки, чтобы ознакомиться с конкретной темой.

   Ссылка

   

3. History of Philosophy (formalized & visualised)

   Интерактивный таймлайн с философами, упорядоченными по хронологии. Карта визуализирует связи между авторами и их идеями, которые представлены в виде краткого тезиса. Каждый тезис связан с тезисами других авторов: красным цветом обозначена критика, а зелёным – согласующиеся тезисы и расширяющие исходный.

   Ссылка

   

4. SQEMA

   Калькулятор, который сопоставляет модальным формулам формулы логики предикатов первого порядка; вычисляет является ли формула «салквистовой формулой» (подробнее про «салквистовые формулы» можно прочитать тут). Формулы первого порядка не всегда выводятся в сокращенном виде.

   Ссылка

   

5. Truth Table Generator

   Калькулятор для построения таблиц истинности. В нём есть несколько опций для вывода значений: 0/1, T/F или ⊤/⊥, и несколько вариантов для ввода будевых связок, который указаны под панелью ввода. Калькулятор может выводить либо всю таблицу, либо значение главных связок. Кроме того, калькулятор генерирует таблицу в виде текста, а также код для построения таблицы в LaTex’е. Есть возможность вводить несколько формул через запятую.

   Ссылка

   

6. Построение таблицы истинности, СДНФ, СКНФ, полином Жегалкина

   Калькулятор для таблиц истинности. Он может строить таблицу истинности по функции или двоичному вектору, строит СКНФ, СДНФ, полином Жегалкина (методами Паскаля, треугольника, неопределённых коэффициентов), карту Карно, минимизирует ДНФ и КНФ, ищет фиктивные переменные, определяет принадлежность функции к каждому из пяти классов Поста. На сайте есть видеоинструкция к калькулятору.

   Ссылка

   

7. Таблица истинности

   Калькулятор для таблиц истинности на основе Wolfram’а. Выводит значение для каждой переменной и главного знака формулы.

   Ссылка

   

8. Truth Table Generator (LaTex)

   Калькулятор строит таблицы истинности для каждой подформулы. Есть возможность сгенерировать таблицу для LaTex, HTML, ASCII.

   Ссылка

   

9. Logic Calculator: Truth Tables

   Калькулятор строит таблицы истинности и выводит значение для всех связок или только значение главного знака формулы. В калькуляторе есть интерактивное дополнение: фиолетовый монстр и утка. Чтобы построить таблицу, нужно нажать на утку. Чтобы стереть один знак, нужно нажать на монстра, а чтобы стереть всю формулу – нажать на него дважды. Есть возможность вводить несколько формул через запятую.

   Ссылка

   

10. Таблица истинности

    Калькулятор для таблиц истинности, который считает значения для главной формулы и для подформул. Есть возможность строить булевы уравнения из таблиц истинности.

    Ссылка

    

11. Truth Table Generator (one more)

    Калькулятор для таблиц истинности. Выводит значения переменных и главной формулы.

    Ссылка

    

12. Truth Table Generator (mobile app)

    Калькулятор для таблиц истинности, который выводит значения для всех подформул и главной формулы. Доступен в App Store и Google Play.

    Ссылка

    

13. Калькулятор логических выражений

    Калькулятор для упрощения логических выражений. Есть возможность вывода результата в разных форматах (ДНФ, КНФ и др.). Внизу дан справочный материал.

    Ссылка

    

14. PHI 251 FitchFX Proof Constructor

    Прувер для фитчевского натурального вывода. Генерирует код вывода для LaTex.

    Ссылка

    

15. Natural deduction proof editor and checker

    Прувер для фитчевского натурального вывода. К калькулятору дана подробная инструкция и упражнения.

    Ссылка

    

16. Tableaux'method for S4

    Прувер для модальной логики в системе S4. Расписывает по шагам доказательство от противного с указанием правил для каждого шага.

    Ссылка

    

17. Tree Proof Generator

    Калькулятор аналитических таблиц. Можно проверять формулы классической логики высказываний, логики предикатов, модальной логики, выводимость из посылок.

    Ссылка

    

18. Modal logic playground

    Прувер для модальной логики, который оценивает формулу в модели Крипке. Модель Крипке можно редактировать, добавляя оценку пропозициональных переменных и отношения достижимости на возможных мирах. Калькулятор позволяет варьировать количество пропозициональных переменных в возможных мирах от 1 до 5. Внизу страницы даны справочные материалы.

    Ссылка

    

19. ELVis (Epistemic Logic Visualizer)

    Самый масштабный прувер для эпистемической логики: классической эпистемической логики (EL), логики публичных объявлений (PAL) и динамической эпистемической логики (DEL). Для каждой логики приводятся справочные материалы и калькулятор секвенциальных исчислений с возможностью выбора аксиом (T, D, B, 4, 5), а также код для LaTex’a. Есть возможность строить модели и оценивать на них формулы. Кроме того, для DEL приведен редактор для событийных моделей.

    Ссылка