Safe Haskell	Safe-Inferred

FirstOrderTheory.Syntax

Synopsis

Documentation

data Literal

Instances

Eq Literal
Ord Literal
Show Literal

data Atom

Instances

Eq Atom
Ord Atom
Show Atom

data Term

Instances

Eq Term
Ord Term
Show Term

data NNFFormula

A quantifier free formla in negation normal form

Instances

Eq NNFFormula
Ord NNFFormula
Show NNFFormula

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

lit :: Atom -> Literal

nLit :: Atom -> Literal

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

Returns a new atom

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

var :: Name -> Term

intConst :: Int -> Term