我正在尝试创建一个将命题更改为析取范式的函数。
它将通过读取 Valuation 列表来做到这一点:
type Valuation = [(Variable, Bool)] -- Valuation of variables to truth values
并使用这些:
findBool :: (Variable, Bool)->Bool
findBool (_,x) = x
findVar :: (Variable, Bool)->Variable
findVar (x,_) = x
命题也是:
data Prop = Falsum -- a contradiction, or
| Var Variable -- a variable, or
| Not Prop -- a negation of a formula, or
| Or Prop Prop -- a disjunction of two formulae, or
| And Prop Prop -- a conjunction of two formulae, or
| Imp Prop Prop -- a conditional of two formulae.
deriving (Eq, Show)
我认为到目前为止我所拥有的非常可靠,但我不知道该怎么处理空箱子。这是我到目前为止所拥有的:
minterm :: Valuation -> Prop
minterm [] = ?
minterm (x:xs) = if (findBool x) then (And (findVar x) (minterm xs)) else (And (Not(findVar x) (minterm xs))
我的目标是:minterm [("p",True),("q",False)]
返回:And (Var "p") (Not (Var "q"))
编辑: Falsum 无效,但如果它没有返回任何东西,我会更喜欢。无论如何我可以排除它会被退回的情况,所以我可以得到这样的东西:
minterm [("p",True),("q",False)]
==And (Var "p") (Not (Var "q"))