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
- Leo Bachmair and Harald Ganzinger. Rewrite-based
equational theorem proving with selection and simplification.
Journal of Logic and Computation, 4(3):217-247, June 1994.
- Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder. Basic paramodulation.
Information and Computation, 121(2):172-192, September
1995.
- Adel Bouhoula, Emmanuel Kounalis, and Michaël Rusinowitch. Automated
mathematical induction. Journal of Logic and
Computation, 5(5):631-668, October 1995.
- Christopher Lynch. Local
simplification. Information and Computation,
142(1):102-126, 10 April 1998.
Selected references
- L. Henschen and L. Wos. Unit refutations and Horn
sets. Journal of the ACM, 21(4):590-605, October 1974.
- Gérard Huet. Confluent reductions: Abstract
properties and application to term rewriting systems. Journal
of the ACM, 27(4):797-821, October 1980.
- William H. Joyner Jr. Resolution strategies as decision
procedures. Journal of the ACM, 23(3):398-417, July
1976.
- Raymond Reiter. Two
results on ordering for resolution with merging and linear format.
Journal of the ACM, 18(4):630-646, October 1971.
- James R. Slagle. Automatic
theorem proving with renamable and semantic resolution.
Journal of the ACM, 14(4):687-697, October 1967.
- James R. Slagle. Automated
theorem-proving for theories with simplifiers, commutativity, and
associativity. Journal of the ACM, 21(4):622-642,
October 1974.
- Lawrence Wos, George A. Robinson, and Daniel F. Carson. Efficiency and completeness of the
set of support strategy in theorem proving. Journal of the
ACM, 12(4):536-541, October 1965.
Shortcuts: