Skip to main content
SpringerLink
Log in

A Horn clause that implies an undecidable set of Horn clauses

  • Conference paper
  • First Online:
Computer Science Logic (CSL 1993)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 832))

Included in the following conference series:

Abstract

In this paper we prove that there exists a Horn clauseHsuch that the problem: given a Horn clause G. Is G a consequence of H? is not recursive. Equivalently, there exists a one-clause PROLOG program such that there is no PROLOG implementation answering TRUE if the program implies a given goal and FALSE otherwise. We give a short survey of earlier results concerning clause implication and prove a classical Linial-Post theorem as a consequence of one of them.

This research has been supported by a KBN grant.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K. Apt: Logic Programming; in Handbook of Theoretical Computer Science vol B., J. van Leeuwen (ed). 1990.

    Google Scholar 

  2. C. Beeri, M.Y. Vardi: The implication problem for data dependencies; Proc. International Coll. on Automata, Languages and Programming 1981, Lecture Notes in Computer Science, vol 115, pp 73–85, Springer, Berlin.

    Google Scholar 

  3. W. Bibel, S. Hölldobler and J. Würtz: Cycle Unification; in D. Kapur (ed.), Proc. the Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol 607, Springer (June 1992).

    Google Scholar 

  4. A. K. Chandra, M. Y. Vardi: The implication problem for functional and inclusion dependencies is undecidable; SIAM J. Comput. vol 14, No 3, (1985).

    Google Scholar 

  5. C.L. Chang, R.C.T. Lee: Symbolic Logic and Mechanical Theorem Proving; Academic Press, New York, San Francisco, London 1973

    Google Scholar 

  6. P. Devienne, P. Lebégue and J.C. Routier: Halting Problem of one Binary Horn Clause is undecidable; proc. of STACS 93, Springer, LNCS, vol 665 pp 48–58.

    Google Scholar 

  7. P.Devienne, P.Lebégue J.C.Routier:Cycle Unification is Undecidable. prepr.1992

    Google Scholar 

  8. G.Gottlob, A.Leitsch:Fast Subsumption Algorithms; LNCS 204-II, Springer, 1985.

    Google Scholar 

  9. G. Gottlob, A. Leitsch: On the Efficiency of Subsumption Algorithms; JACM vol 32 No. 2 (April 1985), pp. 280–295.

    MathSciNet  Google Scholar 

  10. G. Gottlob, A. Leitsch: Deciding Horn clause implication problem by ordered semantic resolution; Comp. Intelligence II, F. Gardin, G. Mauri, (ed), 1990.

    Google Scholar 

  11. Y.S. Gurevich: The problem of equality of words for certain classes of semigroups; (Russian), Algebra i Logika 5,(1966) pp 25–35

    MATH  Google Scholar 

  12. P. Hanschke, J. Würtz: Satisfiability of the Smallest Binary Program; Information Processing Letters 496 (1993) pp. 237–241.

    Google Scholar 

  13. C. Herrmann: On the undecidability of implications between embedded multi-valued database dependencies; preprint.

    Google Scholar 

  14. P.C. Kanellakis: Elements of Relational Database Theory; in Handbook of Theoretical Computer Science vol B., J. van Leeuwen (ed). 1990.

    Google Scholar 

  15. A. Leitsch, Implication Algorithms for Classes of Horn Clauses; Statistik, Informatik und Ökonomie, Springer Verlag 1988, pp 172–179.

    Google Scholar 

  16. A. Leitsch, Deciding Horn Clauses by Hyperresolution, Proc. Computer Science Logic 89, Lecture Notes in Computer Science 440 (1989), pp 225–241

    MathSciNet  Google Scholar 

  17. S. Linial, E. Post: Recursive unsolvability of the deducibility, Tarski's completeness and independence of axioms problems of the propositional calculus (abstract); Bulletin of the American Mathematical Society, 55 p. 50 (1949).

    Google Scholar 

  18. R. McKenzie: On Spectra, and the Negative Solution of the Decision Problem for Identities Having a Finite Nontrivial Model; The Journal of Symbolic Logic, vol 40, No 2 pp 186–195, 1975.

    MATH  MathSciNet  Google Scholar 

  19. J. Marcinkowski, L. Pacholski: Undecidability of the Horn Clause Implication Problem; Proc 33rd Annual Symposium on the Foundations of Computer Science (1992). pp. 354–362.

    Google Scholar 

  20. W.E. Singletary: Results Regarding the Axiomatization of Partial Propositional Calculi; Notre Dame Journal of Formal Logic, vol IX, Number 3, 1968.

    Google Scholar 

  21. R.B. Stillman: The Concept of Weak Substitution In Theorem-proving; JACM vol.20.4(Oct. 1973), 648–667.

    MathSciNet  Google Scholar 

  22. M. Schmidt-Schauss: Implication of Clauses is Undecidable; Theoretical Computer Science 59 (1988), pp. 287–296.

    Article  MATH  MathSciNet  Google Scholar 

  23. J. Würtz: Unifying Cycles; ECAI 1982, B. Neumann ed. pp 60–64.

    Google Scholar 

  24. M. K. Yntema: A detailed argument for the Post-Linial theorems; Notre Dame Journal of Formal Logic, vol V, (1964). pp 35–51.

    MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, University of Wrocław, Poland

    Jerzy Marcinkowski

Authors
  1. Jerzy Marcinkowski
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Egon Börger Yuri Gurevich Karl Meinke

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Marcinkowski, J. (1994). A Horn clause that implies an undecidable set of Horn clauses. In: Börger, E., Gurevich, Y., Meinke, K. (eds) Computer Science Logic. CSL 1993. Lecture Notes in Computer Science, vol 832. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0049334

Download citation

  • DOI: https://doi.org/10.1007/BFb0049334

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58277-9

  • Online ISBN: 978-3-540-48599-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation