FirstOrderTheory- Grammar and typeclass for first order theories

Safe HaskellSafe-Inferred




data Atom


data Term


data NNFFormula

A quantifier free formla in negation normal form

nnfLit :: Literal -> NNFFormula

Returns a NNF Formula consisting of only the input literal

nnfCon :: NNFFormula -> NNFFormula -> NNFFormula

Returns the conjunction of two NNF formulas

nnfDis :: NNFFormula -> NNFFormula -> NNFFormula

Return the disjunction of two NNF formulas

toPropositionalCNF :: NNFFormula -> CNF Literal

Convert NNFFormula to propositional formula in conjunctive normal form

negateLit :: Literal -> Literal

Return the negation of the input literal

atomArgs :: Atom -> [Term]

Return the terms that are arguments to the predicate of the input atom

predicateName :: Atom -> Name

Return the name of the predicate of the input atom

isFunctionWithName :: Name -> Term -> Bool

Returns True if the input term is a function with the give name, and false otherwise

isNeg :: Literal -> Bool

Returns false if the literal is an atomic formula and true if the literal is the negation of an atomic formula

getAtom :: Literal -> Atom

Returns the atomic formula of the given literal

varName :: Term -> Name

Return the name of the input variable, throws error if input term is not a variable

intVal :: Term -> Int

Returns the integer value of an Integer constant or an error if the input is not an integer

funcArgs :: Term -> [Term]

Returns the input function's argument list, throws error if input term is not a function

atom :: Name -> [Term] -> Atom

Returns a new atom

func :: Name -> [Term] -> Term

var :: Name -> Term