aima.core.logic.fol.inference

Class Paramodulation

java.lang.Object

aima.core.logic.fol.inference.AbstractModulation

aima.core.logic.fol.inference.Paramodulation

public class Paramodulation
extends AbstractModulation

Artificial Intelligence A Modern Approach (3r Edition): page 354.

Paramodulation: For any terms x, y, and z, where z appears somewhere in literal m_i, and where UNIFY(x,z) = θ,

                          l1 OR ... OR lk OR x=y,     m1 OR ... OR mn
     ------------------------------------------------------------------------
     SUB(SUBST(θ,x), SUBST(θ,y), SUBST(θ, l1 OR ... OR lk OR m1 OR ... OR mn))
 

Paramodulation yields a complete inference procedure for first-order logic with equality.

Author:

Ciaran O'Reilly

Nested Class Summary

Nested classes/interfaces inherited from class aima.core.logic.fol.inference.AbstractModulation

AbstractModulation.IdentifyCandidateMatchingTerm, AbstractModulation.ReplaceMatchingTerm

Field Summary

Fields inherited from class aima.core.logic.fol.inference.AbstractModulation

substVisitor, unifier, variableCollector

Constructor Summary

Constructors

Constructor and Description
Paramodulation()

Method Summary

Modifier and Type	Method and Description
java.util.Set<Clause>	apply(Clause c1, Clause c2)
java.util.Set<Clause>	apply(Clause c1, Clause c2, boolean standardizeApart)
protected boolean	isValidMatch(Term toMatch, java.util.Set<Variable> toMatchVariables, Term possibleMatch, java.util.Map<Variable,Term> substitution)

Methods inherited from class aima.core.logic.fol.inference.AbstractModulation

getMatchingSubstitution

Methods inherited from class java.lang.Object

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

Constructor Detail

Paramodulation

public Paramodulation()

Method Detail

apply

public java.util.Set<Clause> apply(Clause c1,
                                   Clause c2)

apply

public java.util.Set<Clause> apply(Clause c1,
                                   Clause c2,
                                   boolean standardizeApart)

isValidMatch

protected boolean isValidMatch(Term toMatch,
                               java.util.Set<Variable> toMatchVariables,
                               Term possibleMatch,
                               java.util.Map<Variable,Term> substitution)

Specified by:

isValidMatch in class AbstractModulation