Twee.KBO

An implementation of Knuth-Bendix ordering.

Documentation

lessEq :: (Function f, Sized f, Weighted f) => Term f -> Term f -> Bool

Check if one term is less than another in KBO.

lessIn :: (Function f, Sized f, Weighted f) => Model f -> Term f -> Term f -> Maybe Strictness

Check if one term is less than another in a given model.

lessEqSkolem :: (Function f, Sized f, Weighted f) => Term f -> Term f -> Bool

class Sized a where

Methods

size :: a -> Integer

Compute the size.

Instances

(Labelled f, Sized f) => Sized (Fun f)

Defined in Twee.KBO

Methods

size :: Fun f -> Integer

(Labelled f, Sized f, Weighted f) => Sized (Term f)

Defined in Twee.KBO

Methods

size :: Term f -> Integer

(Labelled f, Sized f, Weighted f) => Sized (TermList f)

Defined in Twee.KBO

Methods

size :: TermList f -> Integer

(Labelled f, Sized f, Weighted f) => Sized (Equation f)

Defined in Twee.KBO

Methods

size :: Equation f -> Integer

class Weighted f where

Methods

argWeight :: f -> Integer

Instances

(Weighted f, Labelled f) => Weighted (Fun f)

Defined in Twee.KBO

Methods

argWeight :: Fun f -> Integer