orbital.moon.logic.resolution
Class LiteralOrders

java.lang.Object
  orbital.moon.logic.resolution.LiteralOrders

public class LiteralOrders
extends java.lang.Object

Provides literal L-orders.

An L-order is an irreflexive, transitive relation on literals which is substitutive, i.e. all substitutions are monotonic:

∀σ∈SUB (p<q &imply; pσ<qσ) L-orders are always partial because unifiable literals are incomparable.

Author:

André Platzer

Field Summary

static java.util.Comparator

DEPTH_ORDER L-Order based on term-depths.

Constructor Summary

LiteralOrders()

Method Summary

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

DEPTH_ORDER

public static final java.util.Comparator DEPTH_ORDER

L-Order based on term-depths.

This implementation compares for maximal overall term depth in favour of maximum individual variable depths.

p<q :⇔ τ(p)<τ(q) ∧ ∀x∈Var(p) τ(x,p)<τ(x,q)

where τ(p) is the maximal term depth in d, and τ(x,p) is the maximum depth of the occurrences of x in p.

Constructor Detail

LiteralOrders

public LiteralOrders()