Declarative Rule

• Name: Demodulation
• Description in English: "The demodulation rule takes an equality statement x = y and any sentence with a nested term that unifies with x and derives the same sentence with y substituted for the nexted term."
• Example in English: "If b.a=c is inferred in the presence of (x^(-1))^(-1)=x, substitution immediately yields obviously related inferences such as (b^(-1))^(-1).a=c."
• Source(s):
  • Name: The Concept of Demodulation in Theorem Proving, JACM 14(4), pp. 698-709
  • Author(s):
    • Name: Daniel F. Carson

    ---

    • Name: George A. Robinson

    ---

    • Name: Leon Shalla

    ---

    • Name: Larry Wos
    • URL: http://www-unix.mcs.anl.gov/~wos/

(Registration details...)

Copyright 2009 Inference Web group.
All Rights Reserved.