Advertisement

Some reordering properties for inequality proof trees

  • Michael M. Richter
Section II: Algorithms
Part of the Lecture Notes in Computer Science book series (LNCS, volume 171)

Keywords

Proof Tree Unit Clause Empty Clause Multiple Chain Bottom Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Bl-Hi]
    W. W. Bledsoe — L. M. Hines: Variable elimination and chaining in a resolution — based prover for inequalities. Proc. 5th Conference on Automated Deduction. Springer LNCS 87, ed. W. Bibel — R. Kowalski, p. 70–87.Google Scholar
  2. [Bl-Ku-Sh]
    W. W. Bledsoe — K. Kunen — R. Shostak: Completeness Results for Inequality Provers. Manuscript 1982.Google Scholar
  3. [Bl-Ne-Sh]
    W. W. Bledsoe — R. Neveln — R. Shostak: Completeness Results for a Class of Inequality Provers, Univ. of Texas Math. Dept. Memo ATP 60, March 1981Google Scholar
  4. [Ku]
    K. Kunen: A Completeness Theorem for Multiple Chaining, Univ. of Texas Math. Dept. Memo ATP 61, Aug. 1980.Google Scholar
  5. [Lo]
    D. W. Loveland: Automated Theorem Proving: A Logical Basis. Amsterdam 1978.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Michael M. Richter
    • 1
  1. 1.Technische Hochschule AachenGermany

Personalised recommendations