Как составить алгоритм доказательства в ИВ?

[Kosarar]

Как составить алгоритм доказательства какого-нибудь общезначимого высказывания с помощью исчисления высказываний?

Более подробно – ниже.

-

Как доказать какое-нибудь общезначимое высказывание с помощью исчисления высказываний? Например, x v !x? Можно использовать, к примеру, эту аксиоматику:
1: A -> ( B -> A)
2: (A -> B) -> (( A -> (B -> C)) -> (A -> C)
3: A & B -> A
4: A & B -> B
5: A -> (B -> A & B)
6: A -> A v B
7: B -> A v B
8: (A -> Q) -> ((B -> Q) -> (A v B ->Q))
9: (A -> B) -> ((A -> !B) -> !A)
10: !!A -> A

Я смотрю на примеры доказательств (http://mathhelpplanet.com/static.php?p= ... skazyvaniy - они не без помарок, но в общем понятные). Там вывод осуществляется из гипотез (которые неявно объединены в конъюнкцию), есть семантическое следование из них в доказываемое высказывание. Здесь же у нас нет гипотез, нет следования. Я где-то читал что-то в том роде, что мы можем вводить гипотезы - но как? Как конкретно доказать какое-нибудь общезначимое высказывание с помощью исчисления высказываний? Я пытаюсь решить (наметить план решения) третье задание следующего содержания (перепишу основную его часть):

«Написать программу, строящую доказательство указанного во входном файле высказывания (если оно общезначимо), либо дающую оценку пропозициональных переменных, на которых высказывание ложно (если оно опровержимо).
Входной файл состоит из единственной строки, содержащей формулу исчисления высказываний, которую требуется доказать или опровергнуть. Высказывание удовлетворяет грамматике из первого задания. Выходной файл должен либо содержать доказательство высказывания (в формате доказательства из первого задания)…»

Первое задание (тоже не очень понятно как решать) задаёт грамматику формами Бэкуса-Наура и его основная часть звучит следующим образом:

«Написать программу, проверяющую доказательства в исчислении высказываний на корректность. Входной файл представляет из себя последовательность высказываний, по высказыванию на строку. ... Результатом работы программы должен быть проаннотированный текст доказательства, касательно каждой строки должно быть указано, из чего и как она получается.»

[Гость]

На самом деле вам нужно констуировать ДКА, поетому наверняка придется изпользовать теорему превращения НДКА в ДКА.
По отношение функции перехода из одно состояние в другое, возможно применение тоже булевой алгебре и соответвующие двоичнъье функции.