CODEWITHSUNDEEP
haskellboolean-logic
chihabeddineAourinmouche
chihabeddineAourinmouche

Reputation: 423

Haskell working with Math Logic

I'm working on this practice problem in which I have to write a bunch of functions in Haskell functional programming language. I manage to write some of them but not all, and I need those that I couldn't finish to proceed in the practice sheet. Can somebody suggest some ideas?

Here are the types I'm working with:

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

type Clause = [Litteral]

type Formule = [Clause]

type Distribution = [(Char, Bool)]

Here are the functions I was able to write:

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)

I still need:

Upvotes: 0

Views: 242

Answers (1)

moondaisy
moondaisy

Reputation: 4481

Using the functions you have already defined:

A function hasAlone if an expression contains a clause that contains only one literal ex: [[a], [a, b, - c]].

So basically, it checks item by item to see if it is an unit clause in which case it returns True.

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

A function findAlone that checks if an expression verifies hasAlone and also returns the alone literal; ex: [[- a][b, c, e]] => [- a].

In this case, I'm assuming you only want the literal for the first unit clause that shows up. It is the same idea that in hasAlone but instead of returning a Bool it returns the literal.

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

A function removeAlone that removes clause containing the alone literal from the expression.

In this case, I include two version, one that removes all the unit clauses and another that removes just the first one. See that if it isn't an unit clause I keep it by adding it at the top of the list that results from the recursion.

-- 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)

A function isEvidentContradictory that returns True if an expression (logical expression) contains at least two unit clauses, one of which contains a literal while the other contains the opposite literal; ex: [[a], [b], [- b]].

In this case I started by assuming that expression means Formule (I hope that's okay). After that, the function checks item by item to see if it is a unit clause (same thing I have been doing in all the functions so far), in which case it looks for a unit clause containing the oposite literal in the rest of the list.

You could define an auxiliar function that does this part elem ((Main.negate (head x)):[]) xs, which is looking for the a unit clause containing the negative literal, just so that it looks neater.

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

Upvotes: 1

Related Questions