Abstract
The paper contains a survey of results in various areas of logic and theoretical computer science which seem to have similar logical structure. The author believes that similarity is not restricted to similar frasing of results and that many of the results described below can be proved in a uniform way.
This research has been supported by KBN grant 2 1197 91 01.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
C. Beeri, M. Vardi, The Implication Problem for Data Dependencies, Proc. 8th ICALP, Lecture Notes in Computer Science 115, (1981), pp. 73–85.
W. Bibel, S. Hölldobler, J. Würtz, Cycle Unification, in D. Kapur (ed.), Proceedings of the Conference on Automated Deduction, Lecture Notes on Artificial Intelligence, vol. 607 (1992).
P. Devienne, P. Lebégue, J.C. Routier, Halting problem of one binary Horn clause is undecidable, Proceedings of Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science, vol. 665 (1993).
P. Devienne, P. Lebégue, J.C. Routier, Cycle unification is undecidable, unpublished manuscript.
A. Chandra, M. Vardi, The implication problem for functional and inclusion dependencies is undecidable, SIAM Journal of Computing 14 (1985), pp. 671–677.
Y. Gurevich, On the Classical Decision Problem, Bulletin of European Association for Theoretical Computer Science 42 (1990), pp. 140–150.
P. Hanschke, J. Würtz, Satisfiability of the smallest binary program, Information Processing Letters 45 (1993), pp.237–241.
G.G. Hillebrand, P.C. Kanellakis, H.G. Mairson, M.Y. Vardi, Undecidable boundedness problems for Datalog programs, to appear.
A.J. Kfoury, J. Tiuryn, P. Urzyczyn, The undecidability of the semiunification problem, Proc. 22-nd ACM Symposium on Theory of Computing, Baltimore 1990, pp. 468–476.
A. Leitsch, Deciding Horn clauses by hyperresolution, Proc. Computer Science Logic 89, Lecture Notes in Computer Science 440 (1989), pp. 225–241.
A. Leitsch, G.Gottlob, Deciding Horn clause implication problems by ordered semantic resolution, Computational Intelligence II, F. Gardin and G. Mauri, ed., 1990, pp.19–26.
H.R. Lewis, W. Goldfarb, The decision problem for formulas with a small number of atomic subformulas, Journal of Symbolic Logic 38 (1973), pp. 471–480.
S. Linial, E. Post, Recursive unsolvability of the deducibility, Tarski's completeness and independence of axioms problems of propositional calculus, Bull. Amer. Math. Soc, vol 55, 1949, p. 50
J. Marcinkowski, L. Pacholski, Undecidability of the Horn clause implication problem, Proceedings of 33rd Annual IEEE Symposium on Foundations of Computer Science, Los Alamitos 1992, pp. 354–362.
J. Marcinkowski, A Horn clause that implies an undecidable set of Horn clauses, to appear.
G.F. Mcnulty, The decision problem for equational bases of algebras, Annals of Mathematical Logic 11 (1976), pp. 193–259.
J.C. Mitchell, The implication problem for functional and inclusion dependencies, Information and Control 56 (1983), pp 154–173.
M. Schmidt-Schauss, Implication of Clauses is Undecidable, Theoretical Computer Science 59 (1988), pp. 287–296.
W. Singletary, Results regarding the axiomatization of partial propositional calculi, Notre Dame J. of Formal Logic, vol. 9 (1968), pp. 193–221.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pacholski, L. (1993). Undecidability of implication problems in logic programming, database theory and classical logic. In: Gottlob, G., Leitsch, A., Mundici, D. (eds) Computational Logic and Proof Theory. KGC 1993. Lecture Notes in Computer Science, vol 713. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022554
Download citation
DOI: https://doi.org/10.1007/BFb0022554
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57184-1
Online ISBN: 978-3-540-47943-7
eBook Packages: Springer Book Archive