Journal of Automated Reasoning

, Volume 7, Issue 1, pp 1–26 | Cite as

Near-Horn Prolog and beyond

  • Donald W. Loveland


Near-Horn Prolog is an extension of Prolog designed to handle disjunction and classical negation. The emphasis here is on minimal change from standard Prolog in regard to notation, derivation form, and speed of inner-loop computation. The procedure is optimized for the input program that is near-Horn; i.e., a program where almost all clauses are definite clauses. This paper goes beyond the near-Horn focus to report on the completeness of one version of nH-Prolog, along with soundness of the procedure. Completeness is important here not only for the usual reasons of guaranteed success on small problems and insight into the behavior of the procedure but also because we anticipate the introduction of negation-as-failure which requires conviction that a proof will be found if a proof exists.

Key words

Extended Prolog indefinite answers case analysis logic programming 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Chang, C. and Lee, R. C. T., Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, 1973, xiii + 331.Google Scholar
  2. 2.
    Clocksin, W. F. and Mellish, C. S., Programming in Prolog (Third edition). Springer-Verlag, Berlin, 1987, x + 281.Google Scholar
  3. 3.
    Gabbay, D. M., ‘N-Prolog: an extension of Prolog with hypothetical implication, Part 2’, J. Logic Progr. 4, 251–283 (1985).Google Scholar
  4. 4.
    Gabbay, D. M. and Reyle, U., ‘N-Prolog: an extension of Prolog with hypothetical implication, Part 1’. J. Logic Progr. 4, 318–355 (1984).Google Scholar
  5. 5.
    Gallier, J. H., Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row, New York, 1986, xv + 511.Google Scholar
  6. 6.
    Kowalski, R. and Kuehner, D., ‘Linear resolution with selection function’. Artif. Intell. 2, Winter 1971, 227–260.Google Scholar
  7. 7.
    Lloyd, J. W., Foundations of Logic Programming (2nd Ed.). Springer-Verlag, Heidelberg, 1987, xii + 212.Google Scholar
  8. 8.
    Loveland, D. W., ‘Mechanical theorem proving by Model Elimination’, J. Assoc. of Comput. Mach. 15, 236–251 (1968).Google Scholar
  9. 9.
    Loveland, D. W., Automated Theorem Proving: A Logical Basis. North-Holland, Amsterdam, 1978, xiii + 405.Google Scholar
  10. 10.
    Loveland, D. W., ‘Near-Horn prolog’. Logic Programming: Proc. of the Fourth Conf. (J. Lassez, ed.), MIT Press, 1987, 456–469.Google Scholar
  11. 11.
    Loveland, D. W. and Reed, D. W., ‘A near-Horn Prolog for compilation’. Comp. Science Tech. Report CS-1989–14, Duke Univ., Durham, 1989, 21pp. To appear in Computational Logic: Essays in Honor of Alan Robinson.Google Scholar
  12. 12.
    Plaisted, D. A., ‘Non-Horn clause logic programming without contrapositives’. J. Automated Reasoning 4(3), 287–325 (1988).Google Scholar
  13. 13.
    Plaisted, D. A., ‘A sequent-style model elimination strategy and a positive refinement’. J. Automated Reasoning 6(4), 389–402 (1990).Google Scholar
  14. 14.
    Poole, D. and Goebel, R., ‘Gracefully adding negation and disjunction to Prolog’, Proc. Third Int'l. Logic Progr. Conf., Lecture Notes in Computer Science 225, Springer-Verlag, 1986, 635–641.Google Scholar
  15. 15.
    Reed, D. W. and Loveland, D. W., ‘A comparison of three Prolog extensions’, Comp. Science Tech. Report CS-1989–8, Duke Univ., Durham, 1989, 28pp. To appear in the J. Logic Progr. Google Scholar
  16. 16.
    Smith, B. T. and Loveland, D. W., ‘A simple near-Horn Prolog interpreter’. Logic Programming: Proc. of the Fifth Intern. Conf. and Symp. (Kowalski and Bowen, eds.), MIT Press, 1988, 794–809.Google Scholar
  17. 17.
    Stickel, M. E., ‘A Prolog Technology Theorem Prover’, New Generation Computing 2(4), 371–383 (1984).Google Scholar
  18. 18.
    Stickel, M. E., ‘A Prolog Technology Theorem Prover: implementation by an extended compiler’. Proc. of the Eighth Conf. on Auto. Deduction (Siekmann, ed.), Lecture Notes in Computer Science 230, Springer-Verlag, 1988, 573–587.Google Scholar

Copyright information

© Kluwer Academic Publishers 1991

Authors and Affiliations

  • Donald W. Loveland
    • 1
  1. 1.Department of Computer ScienceDuke UniversityDurhamUSA

Personalised recommendations