Part of the Lecture Notes in Computer Science book series (LNCS, volume 171)
Some reordering properties for inequality proof trees
KeywordsProof 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.
Unable to display preview. Download preview PDF.
- [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
- [Bl-Ku-Sh]W. W. Bledsoe — K. Kunen — R. Shostak: Completeness Results for Inequality Provers. Manuscript 1982.Google Scholar
- [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
- [Ku]K. Kunen: A Completeness Theorem for Multiple Chaining, Univ. of Texas Math. Dept. Memo ATP 61, Aug. 1980.Google Scholar
- [Lo]D. W. Loveland: Automated Theorem Proving: A Logical Basis. Amsterdam 1978.Google Scholar
© Springer-Verlag Berlin Heidelberg 1984