Abstract
It is shown how certain refutation methods can be extended into semi-decision procedures that are complete for both unsatisfiability and finite satisfiability. The proposed extension is justified by a new characterization of finite satisfiability. This research was motivated by a database design problem: Deduction rules and integrity constraints in definite databases have to be finitely satisfiable.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
9. References
Bayer, R. Query Evaluation and Recursion in Deductive Database Systems. Technical Report TUM-18503, Technical University of Munich, 1985.
Bry, F., Decker, H. and Manthey, R. A Uniform Approach to Constraint Satisfaction and Constraint Satisfiability in Deductive Databases. In Advanced in Database Technology — Proc. EDBT '88. Mar., 1988. Springer-Verlag, LNCS 303.
Beth, E.W. The Foundation of Mathematics. North Holland, Amsterdam, 1959. cited in [SMUL 68].
Bry, F. and Manthey, R. Checking Consistency of Database Constraints: A Logical Basis. In Proc. 12th Int. Conf. on Very Large Data Bases (VLDB '86). Aug. 25–28, 1986.
Dreben, B. and Goldfarb, W. The Decision Problem — Solvable Classes of Quantified Formulas. Addison-Wesley, Reading, Massachussetts, 1979.
Davis, M. and Putnam, H. A Computing Procedure for Quantification Theory. J. of the ACM 7(3), Jul., 1960.
Fagin, R. and Vardi M.Y. The Theory of Data Dependencies — An Overview. In Proc. of ICALP. 1984.
Gallaire, H., Minker, J. and Nicolas, J.-M. Logic and Databases: A Deductive Approach. ACM Computing Surveys 16(2), Jun., 1984.
Kuhns, J.L. Answering Questions by Computer — A Logical Study. Rand Memo RM 5428 PR, Rand Corp., Santa Monica, Calif., 1967.
Loveland, D. Automated Theorem Proving: A Logical Basis. North-Holland, Amsterdam, 1978.
Manthey, R. and Bry, F. A Hyperresolution Proof Procedure and its Implementation in Prolog. In Proc. 11th German Workshop on Artificial Intelligence (GWAI '87). Sep. 28–Oct. 2, 1987. Springer-Verlag, IF 152.
Manthey, R. and Bry, F. SATCHMO: A Theorem Prover Implemented in Prolog. In Proc. 9th Conf. on Automated Deduction (CADE '88). May 23–26, 1988. Springer-Verlag, LNCS.
Mendelson, E. Introduction to Mathematical Logic. Van Nostrand Reinhold, New York, 1969.
Nicolas, J.-M. and Gallaire, H. Database: Theory vs. Interpretation. In Logic and Databases. Plenum, New York, 1978.
Reiter, R. Towards a Logical Reconstruction of Relational Database Theory. In On Conceptual Modelling. Springer-Verlag, Berlin and New York, 1984.
Smullyan, R. First-Order Logic. Springer-Verlag, New York, 1968.
Trachtenbrot, B.A. Impossibility of an Algorithm for the Decision Problem in Finite Classes. Dokl. Acad. Nauk. SSSR 70, 1950. in Russian, translated into English in Amer. Soc. Trans., Series 2, 23, 1963.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag
About this paper
Cite this paper
Bry, F., Manthey, R. (1988). Proving finite satisfiability of deductive databases. In: Börger, E., Büning, H.K., Richter, M.M. (eds) CSL '87. CSL 1987. Lecture Notes in Computer Science, vol 329. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50241-6_28
Download citation
DOI: https://doi.org/10.1007/3-540-50241-6_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50241-8
Online ISBN: 978-3-540-45960-6
eBook Packages: Springer Book Archive