Data.Logic.Classes.Atom

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.

Documentation

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

Methods

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

allVariables :: atom -> Set v

freeVariables :: atom -> Set v

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

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

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

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

isRename :: atom -> atom -> Bool

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

Instances

Atom FOLEQ TermType String

(Predicate p, Variable v, Function f v) => Atom (Predicate p (PTerm v f)) (PTerm v f) v