jukebox-0.1.2: A first-order reasoning toolbox

Safe HaskellNone

Jukebox.Monotonox.ToFOF

Documentation

data Scheme Source

Constructors

Scheme 

Fields

makeFunction :: Type -> NameM Function
 
scheme1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1
 

data Scheme1 Source

Constructors

Scheme1 

Fields

forAll :: Bind Form -> Form
 
exists :: Bind Form -> Form
 
equals :: Term -> Term -> Form
 
funcAxiom :: Function -> NameM Form
 
typeAxiom :: Type -> NameM Form
 

guard :: Scheme1 -> (Type -> Bool) -> Input Form -> Input FormSource

translate :: Scheme -> (Type -> Bool) -> Problem Form -> Problem FormSource

translate1 :: Scheme -> (Type -> Bool) -> Problem Form -> Problem FormSource

tagsFlags :: OptionParser BoolSource

tags :: Bool -> SchemeSource

tags1 :: Bool -> (Type -> Bool) -> (Type -> Function) -> Scheme1Source

tagsAxiom :: Bool -> (Type -> Bool) -> (Type -> Function) -> Function -> NameM FormSource

tagsExists :: (Type -> Bool) -> Type -> Function -> NameM FormSource

guards :: SchemeSource

guards1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1Source

naked :: Symbolic a => Bool -> Variable -> a -> BoolSource

guardsAxiom :: (Type -> Bool) -> (Type -> Function) -> Function -> NameM FormSource

guardsTypeAxiom :: (Type -> Bool) -> (Type -> Function) -> Type -> NameM FormSource