aima.core.logic.fol.inference

Class Demodulation

java.lang.Object

aima.core.logic.fol.inference.AbstractModulation

aima.core.logic.fol.inference.Demodulation

public class Demodulation
extends AbstractModulation

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

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

                 x=y,    m1 OR ... OR mn[z]
     ------------------------------------------------------------
     SUB(SUBST(θ,x), SUBST(θ,y), m1 OR ... OR mn)
 

where SUBST is the usual substitution of a binding list, and SUB(x,y,m) means to replace x with y everywhere that x occurs within m.

Some additional restrictions/clarifications highlighted in:
Demodulation Restrictions
1. Unit Equations Only.
2. Variables substituted in Equation Only.

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
Demodulation()

Method Summary

Modifier and Type	Method and Description
AtomicSentence	apply(TermEquality assertion, AtomicSentence expression)
Clause	apply(TermEquality assertion, Clause clExpression)
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

Demodulation

public Demodulation()

Method Detail

apply

public Clause apply(TermEquality assertion,
                    Clause clExpression)

apply

public AtomicSentence apply(TermEquality assertion,
                            AtomicSentence expression)

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