FirstOrderTheory- Grammar and typeclass for first order theories

Safe HaskellSafe-Inferred




class FirstOrderTheory t where

Description of a decidable first order theory

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

predicateDecl :: Name -> Arity -> [Sort] -> PredicateDecl

Specify a new predicate declaration

functionDecl :: Name -> Arity -> [Sort] -> Sort -> FunctionDecl

Specify a new function declaration