Упрощение булевых логических выражений до DNF и CNF (в Haskell)

Я понимаю, что существуют общепринятые алгоритмы приведения заданного булево-логического выражения к КНФ или ДНФ. Я нашел несколько веб-сайтов об этом, но ничего такого, что я мог бы использовать для создания программы на Haskell вокруг этого.

Это не домашняя работа, и я не прошу кого-нибудь написать мне код — я просто ищу какой-то ресурс, которому я могу следовать, чтобы помочь мне создавать свои функции.

Мне кажется, что я должен определить тип данных Exp, который имеет дело с Or Exp Exp, And Exp Exp, и т.д., и т.д.. а затем создайте стандартные «правила» (Де Моргана, Modus Ponens, Modus Tollens, какие у вас есть), чтобы использовать их для многократного применения к Exp, пока я не достигну точки где я не получаю дальше.

(Поскольку я играл с Agda и т. д., я, как правило, писал все на Haskell, прежде чем переводить на Agda. Так что да, если вы больше знакомы с выражением чего-либо на Agda, тогда я тоже это пойму))


logic functional-programming haskell boolean-logic agda
person Allan    schedule 26.07.2014    source источник
comment
У вас есть правильная идея. Если ваш Exp равен только And или Or, то вам на самом деле нужен только один из законов Де Моргана (от этого выбора зависит, достигнете ли вы CNF или DNF). В чем именно заключается ваш вопрос?   -  person Karolis Juodelė    schedule 26.07.2014
comment
Если вы добавите больше операций, вам нужно будет только переписать их с помощью and, or, not. Это не добавляет сложности. Кроме того, я что-то напутал в правилах. Вам нужны оба Де Моргана. Вместо этого вам нужен один дистрибутив.   -  person Karolis Juodelė    schedule 26.07.2014
comment
Я не уверен, какое там описание. Вы сопоставляете каждый конструктор, вызываете свой toCNF для дочерних элементов и объединяете результаты. Очевидно, toCNF (And a b) = And (toCNF a) (toCNF b). Вам также нужно сопоставить Not (And a b) и Not (Or a b) для Де Моргана. Сопоставление Or — это, конечно, самая интересная часть, но это всего лишь распределение. Если вы сочтете это сложным, я предлагаю сначала написать функцию, которая применяет Де Моргана до тех пор, пока все отрицания не будут литералами. Это проще, но в основном то же самое.   -  person Karolis Juodelė    schedule 26.07.2014
comment
Вы можете попробовать реализовать, например. преобразование Цейтина. Есть много сайтов, объясняющих, как это работает.   -  person aztek    schedule 08.08.2014

Ответы (1)


arrow_upward
3
arrow_downward

Вы можете использовать для этого хороший пакет hatt. Он имеет API для преобразования в NNF, CNF и т. д. Это пример кода:

import Data.Logic.Propositional
import Data.Logic.Propositional.NormalForms

a = Variable (Var 'A')
b = Variable (Var 'B')
c = Variable (Var 'C')
d = Variable (Var 'D')

expression = Conjunction a (Disjunction b (Conjunction c d))

И тогда вы можете поиграть с expression в ghci:

λ> expression
(A ∧ (B ∨ (C ∧ D)))
λ> toCNF expression
(A ∧ ((B ∨ C) ∧ (B ∨ D)))

Я бы посоветовал вам посмотреть на источник пакета, так как это не очень сложно.

person Sibi    schedule 26.07.2014