Declarative Rule

• Name: Negative Paramodulation
• Description in English: "The inference rule negative paramodulation reasons from negated equalities rather than equalities. The rule is sound if the functions involved satisfy certain cancellation-like properties. For example, from A<>B and AC=D, we can derive BC<>D by negative paramodulation provided that right cancellation holds for product."
• Source(s):
  • Name: Negative Paramodulation, Proceedings of CADE-8, Lecture Notes in Computer Science 230, pp. 229-239
  • Author(s):
    • Name: Larry Wos
    • URL: http://www-unix.mcs.anl.gov/~wos/

    ---

    • Name: William McCune
    • URL: http://www-unix.mcs.anl.gov/~mccune/
  • Publisher:
    • Name: Springer-Verlag Heidelberg
    • URL: http://www.springer.de/

(Registration details...)

Copyright 2009 Inference Web group.
All Rights Reserved.