Правильный способ доказать правильность и завершение алгоритма из преобразования формул

Question

Я хотел бы доказать правильность и завершение функции / алгоритма, который преобразует любую логическую формулу первого порядка в ее Нормальную форму отрицания (NNF). Однако я даже не знаю, с чего начать. Кто-нибудь может мне помочь?

Я пытался использовать пакет FOL, но потом понял, что не могу импортировать Main, чтобы использовать команду «fun» одновременно. Затем я начал с Main и доказал несколько правил эквивалентности, используя blast.

Теперь мне нужно создать функцию, которая преобразует формулу первого порядка в ее нормальную форму отрицания. Я начал с этого:

весело toNNF :: "prop ==> prop", где ...

но, похоже, это не работает должным образом (Изабель дает мне сообщение: «Ошибка объединения типов»). Здесь есть свет?

Answer 1

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

Надеюсь, это поможет, Рене