Many resolution-based theorem provers impose a depth bound on the
terms they create. Not the least of the reasons for this is to
prevent infinite loops.
library(termdepth) provides five predicates:
term_depth(Var) = 0 term_depth(Const) = 0 term_depth(F(T1,...,Tn)) = 1 + max(term_depth(T1), ..., term_depth(Tn))
term_depth/2, is less than or equal to Bound. Bound is assumed to be a strictly positive integer. Note that
depth_bound/2will terminate even if Term is cyclic.
term_size(Var) = 0 term_size(Const) = 1 term_size(F(T1,...,Tn)) = 1 + term_size(T1) + ... + term_size(Tn).
term_size/2, is less than or equal to Bound. Bound is assumed to be a non-negative integer. Note that
size_bound/2will always terminate even if Term is cyclic.