logic-classes-1.4.7: Framework for propositional and first order logic, theorem proving

Safe HaskellNone




class Variable v => Skolem f v | f -> v whereSource

This class shows how to convert between atomic Skolem functions and Ints. We include a variable type as a parameter because we create skolem functions to replace an existentially quantified variable, and it can be helpful to retain a reference to the variable.


toSkolem :: v -> fSource

Built a Skolem function from the given variable and number. The number is generally obtained from the skolem monad.

isSkolem :: f -> BoolSource


Skolem Function String 
Variable v => Skolem (AtomicFunction v) v