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

Safe HaskellSafe-Inferred



Substitution and finding variables are two basic operations on formulas that contain terms and variables. If a formula type supports quantifiers we can also find free variables, otherwise all variables are considered free.


class Atom atom term v | atom -> term v whereSource


substitute :: Map v term -> atom -> atomSource

allVariables :: atom -> Set vSource

freeVariables :: atom -> Set vSource

unify :: Map v term -> atom -> atom -> Failing (Map v term)Source

match :: Map v term -> atom -> atom -> Failing (Map v term)Source

Very similar to unify, not quite sure if there is a difference

foldTerms :: (term -> r -> r) -> r -> atom -> rSource

isRename :: atom -> atom -> BoolSource

getSubst :: Map v term -> atom -> Map v termSource