Additional Key Words and Phrases: theorem-proving, resolution, paramodulation, factoring, first-order logic, Horn set
Selected papers that cite this one
- John Grant and Barry E. Jacobs. On the family of generalized dependency constraints. Journal of the ACM, 29(4):986-997, October 1982.
- 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.
- Bernhard Nebel and Hans-Jürgen Bürckert. Reasoning about temporal relations: A maximal tractable subclass of Allen's interval algebra. Journal of the ACM, 42(1):43-66, January 1995.
- Bart Selman and Henry Kautz. Knowledge compilation and theory approximation. Journal of the ACM, 43(2):193-224, March 1996.
- Susumu Yamasaki and Shuji Doshita. The satisfiability problem for a class consisting of Horn sentences and some non-Horn sentences in proportional logic. Information and Control, 59(1-3):1-12, October/November/December 1983.
Selected references
- C. L. Chang. The unit proof and the input proof in theorem proving. Journal of the ACM, 17(4):698-707, October 1970.
- 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.