- Автоматизация рассуждений с помощью логики точек зрения с помощью вложенных последовательностей (arXiv)
Автор: Тим С. Лайон, Лусия Гомес Альварес.
Аннотация: Логика точек зрения — это недавно предложенный формализм в контексте интеграции знаний, который защищает подход с несколькими точками зрения, позволяющий рассуждать с выбором различных и, возможно, конфликтующих точек зрения, а не принуждать их к объединению. В этой статье мы вводим вложенные секвенциальные исчисления для логики пропозициональной точки зрения — системы доказательств, которые манипулируют деревьями, узлы которых являются мультимножествами формул — и показываем, как автоматизировать рассуждения с точки зрения с помощью недетерминированных алгоритмов поиска доказательств. Чтобы получить оптимальное по сложности доказательство в наихудшем случае, мы вводим новый метод в контексте вложенных секвенций, называемый «раскрашиванием», который состоит в том, что в качестве входных данных принимается формула, угадывается определенная раскраска ее подформул, а затем выполнение проверки во вложенном секвенциальном исчислении на цветном вводе. Наша методика позволяет нам определить достоверность формул точек зрения в CoNP, поскольку поиск доказательств дает только частичное доказательство относительно каждой разрешенной раскраски входных данных. Мы показываем, как все частичные доказательства могут быть объединены вместе, чтобы построить полное доказательство, когда входные данные верны, и как некоторые частичные доказательства могут быть преобразованы в контрмодель, когда входные данные неверны. Эти «сертификаты» (то есть доказательства и контрмодели) служат объяснениями (не)валидности входных данных.
2. Автоматизированные рассуждения в неклассической логике в мире TPTP (arXiv)
Автор: Александр Стин, Дэвид Фуэнмайор, Тобиас Гляйснер, Джефф Сатклифф, Кристоф Бенцмюллер.
Аннотация: Неклассическая логика используется в широком спектре дисциплин, включая искусственный интеллект, информатику, математику и философию. Де-факто стандартная инфраструктура для автоматического доказательства теорем, TPTP World, в настоящее время поддерживает только классическую логику. Подобных стандартов для неклассических логических рассуждений не существует (пока). Это затрудняет практическое развитие систем рассуждений и ограничивает их взаимодействие и применение. В этой статье описывается последнее расширение TPTP World, которое предоставляет языки и инфраструктуру для рассуждений в неклассической логике. Расширения легко интегрируются с существующим TPTP World.
