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

Safe HaskellNone

Data.Logic.Classes.Skolem

Synopsis

Documentation

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.

Methods

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

Instances

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