Orbital library

Class LiteralOrders

  extended by 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.

André Platzer

Field Summary
static java.util.Comparator DEPTH_ORDER
          L-Order based on term-depths.
Constructor Summary
Method Summary
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail


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


public LiteralOrders()

Orbital library
1.3.0: 11 Apr 2009

Copyright © 1996-2009 André Platzer
All Rights Reserved.