A = {X, Y, Z}
A* - множество всех слов над алфавитом A (включая пустое слово).
Правила вывода:
∀α ∈ A* : αY ⇒ αYZ
∀α ∈ A* : Xα ⇒ Xαα
∀α,β ∈ A* : αYYYβ ⇒ αZβ
∀α,β ∈ A* : αZZβ ⇒ αβ
Теорема 1:
XY ⇒ XZ
Задача: определить выводимость Теоремы 1.
----
Ни для кого не будет спойлером, что теорема 1 невыводима. В самом деле, заданного базиса недостаточно, чтобы взяв за аксиому слово XY доказать слово XZ. Это можно доказать так называемым «аналитическим» способом, ручным разбором. Быть может, удастся уложиться на половину листа.
Есть ощущение, что к 2013-му году должен быть способ доказать невыводимость утверждения в рамках заданной формальной теории с алфавитом, элементами и аксиоматической базой.
Прологовский backtracking в данном случае, как и для любых неконструктивных задач, подходит слабо. DCG тоже пристроить некуда.
Coq, как theorem-prover, в подобных задачах автоматического доказательства тоже подходит довольно слабо. Но буду рад ошибиться насчёт него и agda.
Решаема ли эта задача полностью автоматически? Если да, то как, если нет, то почему?
