Journal of the ACM Bibliography

Jieh Hsiang and Michaël Rusinowitch. Proving refutational completeness of theorem-proving strategies: The transfinite semantic tree method. Journal of the ACM, 38(3):559-587, July 1991. [BibTeX entry]
Categories and Subject Descriptors: F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic -- mechanical theorem proving, proof theory; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving -- deduction, resolution

General Terms: Theory

Additional Key Words and Phrases: Refutational Theorem Proving Strategies, Transfinite Ordinals, Transfinite Semantic Trees, Resolution, Complete simplification orderings, completeness, first-order logic with equality, functional reflexive axioms, paramodulation, resolution, transfinite ordinals, transfinite semantic trees

Selected papers that cite this one

Selected references


Shortcuts:

  • Journal of the ACM homepage
  • Bibliography top level
  • Journal of the ACM Author Index
  • Search the HBP database