Folly.Formula

Documentation

data Term

Instances

Eq Term

Ord Term

Show Term

data Formula

Instances

Eq Formula

Ord Formula

Show Formula

fvt :: Term -> Set Term

subTerm :: Map Term Term -> Term -> Term

isVar :: Term -> Bool

isConst :: Term -> Bool

isFunc :: Term -> Bool

funcName :: Term -> String

funcArgs :: Term -> [Term]

appendVarName :: String -> Term -> Term

var :: String -> Term

func :: [Char] -> [Term] -> Term

constant :: String -> Term

te :: Term -> Formula -> Formula

fa :: Term -> Formula -> Formula

pr :: String -> [Term] -> Formula

con :: Formula -> Formula -> Formula

dis :: Formula -> Formula -> Formula

neg :: Formula -> Formula

imp :: Formula -> Formula -> Formula

bic :: Formula -> Formula -> Formula

t :: Formula

f :: Formula

vars :: Formula -> Set Term

freeVars :: Formula -> Set Term

generalize :: Formula -> Formula

subFormula :: Map Term Term -> Formula -> Formula

applyToTerms :: Formula -> (Term -> Term) -> Formula

literalArgs :: Formula -> [Term]

toPNF :: Formula -> Formula

toSkolemForm :: Formula -> Formula

skf :: Int -> [Term] -> Term

type Clause = [Formula]

toClausalForm :: Formula -> [Clause]

isTautology :: Clause -> Bool

matchingLiterals :: Formula -> Formula -> Bool