jukebox-0.2.6: A first-order reasoning toolbox
Jukebox.Monotonox.Monotonicity
data Extension Source
Constructors
Instances
data Var Source
annotateMonotonicity :: Problem Clause -> IO (Problem Clause) Source
monotone :: [Clause] -> IO (Map Type (Maybe (Map Function Extension))) Source
fromModel :: [Function] -> Type -> (Var -> Bool) -> Map Function Extension Source
extension :: Function -> (Var -> Bool) -> Extension Source
clause :: [Literal] -> Sat Var Type () Source
literal :: [Literal] -> Literal -> Sat Var Type () Source
safe :: [Literal] -> Term -> Form Var Source
guards :: Literal -> Variable -> Form Var Source