Package edu.upc.fib.inlab.imp.kse.logics.logicschema.services

Class MGUFinder

java.lang.Object

edu.upc.fib.inlab.imp.kse.logics.logicschema.services.MGUFinder

public class MGUFinder
extends Object

Class with static functions to find Most General Unifier between literals, and atoms.

In the current version, two comparison built-in literals such as "2 < a" and "a > 2" are considered to be non-unifiable since they are using different comparison built-in.

Method Summary

Modifier and Type	Method	Description
static boolean	areAtomsUnifiable(Atom... atoms)
static boolean	areAtomsUnifiable(List<Atom> atoms)
static boolean	areLiteralsUnifiable(Literal... literals)
static boolean	areLiteralsUnifiable(Collection<Literal> literals)
static Optional<Substitution>	getAtomsMGU(Atom... atoms)
static Optional<Substitution>	getAtomsMGU(Collection<Atom> atoms)
static Optional<Substitution>	getLiteralsMGU(Literal... literals)
static Optional<Substitution>	getLiteralsMGU(Collection<Literal> literals)

Methods inherited from class java.lang.Object

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

Method Details

getLiteralsMGU

public static Optional<Substitution> getLiteralsMGU(Literal... literals)

getLiteralsMGU

public static Optional<Substitution> getLiteralsMGU(Collection<Literal> literals)

areLiteralsUnifiable

public static boolean areLiteralsUnifiable(Collection<Literal> literals)

areLiteralsUnifiable

public static boolean areLiteralsUnifiable(Literal... literals)

getAtomsMGU

public static Optional<Substitution> getAtomsMGU(Collection<Atom> atoms)

Parameters:

atoms - not null

Returns:

a Maximum General Unifier substitution between actual and atom2, if it exists

getAtomsMGU

public static Optional<Substitution> getAtomsMGU(Atom... atoms)

areAtomsUnifiable

public static boolean areAtomsUnifiable(List<Atom> atoms)

areAtomsUnifiable

public static boolean areAtomsUnifiable(Atom... atoms)