Haskell 使用数学逻辑

Question

我正在研究这个练习题，我必须用 Haskell 函数式编程语言编写一堆函数。我设法写了一些但不是全部，我需要那些我无法完成的练习sheet。有人可以提出一些想法吗？

以下是我正在使用的类型：

data Litteral = Pos Char | Neg Char
      deriving (Show, Eq)

type Clause = [Litteral]

type Formule = [Clause]

type Distribution = [(Char, Bool)]

以下是我能够编写的函数：

negate :: Litteral -> Litteral
negate (Pos v) = Neg v
negate (Neg v) = Pos v

unitClaus :: Clause -> Bool
unitClaus [_] = True
unitClaus _  = False

associate :: Litteral -> (Char, Bool)
associate (Pos c) = (c, True)
associate (Neg c) = (c, False)


isTautology:: Clause -> Bool
isTautology [] = False
isTautology [_] = False
isTautology (x:xs)
    | elem (negation x) xs = True
    | otherwise = isTautology (xs)

我还需要：

一个函数isEvidentContradictory returns 如果表达式（逻辑表达式）包含至少两个单元子句，其中一个包含文字而另一个包含相反的，则为真文字;例如：[[a], [b], [- b]]
一个函数 hasAlone 如果一个表达式包含一个只包含一个文字的子句 ex: [[a], [a, b, - c]]
一个函数 findAlone 检查表达式是否验证 hasAlone 以及 returns 单独的文字；例如：[[- a][b, c, e]] => [- a]
一个函数removeAlone，它从表达式

Answer 1

使用您已经定义的函数：

函数 hasAlone 如果表达式包含一个仅包含一个文字 ex 的子句：[[a], [a, b, - c]]。

所以基本上，它逐项检查以查看它是否是单元子句，在这种情况下 returns True.

hasAlone :: Formule -> Bool
hasAlone [] = False
hasAlone (x:xs)
    | unitClaus x = True
    | otherwise = hasAlone xs

一个函数 findAlone 检查表达式是否验证 hasAlone 以及 returns 单独的文字；例如：[[- a][b, c, e]] => [- a]。

在这种情况下，我假设您只需要出现的第一个单元子句的文字。在 hasAlone 中的想法相同，但不是返回 Bool 它 returns 文字。

findAlone :: Formule -> Litteral
findAlone [] = error "No alone litteral"
findAlone (x:xs)
    | unitClaus x = head x
    | otherwise = findAlone xs

一个函数 removeAlone 从表达式中删除包含 alone 文字的子句。

在这种情况下，我包括两个版本，一个删除所有单元子句，另一个只删除第一个。如果它不是单元子句，我会通过将它添加到递归结果列表的顶部来保留它。

-- Removes all the unit clauses
removeAlone :: Formule -> Formule
removeAlone [] = []
removeAlone (x:xs)
    | unitClaus x = removeAlone xs
    | otherwise = x:(removeAlone xs)

-- Removes the first unit clauses
removeAlone1 :: Formule -> Formule
removeAlone1 [] = []
removeAlone1 (x:xs)
    | unitClaus x = xs
    | otherwise = x:(removeAlone xs)

一个函数isEvidentContradictory returns True if 一个表达式（逻辑表达式）包含至少两个单元子句，其中一个包含一个文字而另一个包含相反的文字;例如：[[a], [b], [- b]]。

在这种情况下，我首先假设表达式表示 Formule（我希望没关系）。之后，该函数逐项检查它是否是一个单元子句（到目前为止我在所有函数中都在做同样的事情），在这种情况下，它会在其余部分中查找包含相反文字的单元子句列表。

你可以定义一个辅助函数来完成这部分 elem ((Main.negate (head x)):[]) xs，它正在寻找包含否定文字的单元子句，这样看起来更整洁。

isEvidentContradictory :: Formule -> Bool
isEvidentContradictory [] = False;
isEvidentContradictory (x:xs) 
    | unitClaus x = elem ((Main.negate (head x)):[]) xs || isEvidentContradictory xs
    | otherwise = isEvidentContradictory xs

Haskell 使用数学逻辑

Haskell working with Math Logic

haskell

boolean-logic