ACM SIGMOD Anthology ACM SIGMOD dblp.uni-trier.de

Logic Programming as Constructivism: A Formalization and its Application to Databases.

François Bry: Logic Programming as Constructivism: A Formalization and its Application to Databases. PODS 1989: 34-50
@inproceedings{DBLP:conf/pods/Bry89,
  author    = {Fran\c{c}ois Bry},
  title     = {Logic Programming as Constructivism: A Formalization and its
               Application to Databases},
  booktitle = {Proceedings of the Eighth ACM SIGACT-SIGMOD-SIGART Symposium
               on Principles of Database Systems, March 29-31, 1989, Philadelphia,
               Pennsylvania},
  publisher = {ACM Press},
  year      = {1989},
  isbn      = {0-89791-308-6},
  pages     = {34-50},
  ee        = {http://doi.acm.org/10.1145/73721.73725, db/conf/pods/Bry89.html},
  crossref  = {DBLP:conf/pods/89},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
BibTeX

Abstract

The features of logic programming that seem unconventional from the viewpoint of classical logic can be explained in terms of constructivistic logic. We motivate and propose a constructivistic proof theory of non-Horn logic programming. Then, we apply this formalization for establishing results of practical interest. First, we show that 'stratification' can be motivated in a simple and intuitive way. Relying on similar motivations, we introduce the larger classes of 'loosely stratified' and 'constructively consistent' programs. Second, we give a formal basis for introducing quantifiers into queries and logic programs by defining 'constructively domain independent' formulas. Third, we extend the Generalized Magic Sets procedure to loosely stratified and constructively consistent programs, by relying on a 'conditional fixpoint' procedure.

Copyright © 1989 by the ACM, Inc., used by permission. Permission to make digital or hard copies is granted provided that copies are not made or distributed for profit or direct commercial advantage, and that copies show this notice on the first page or initial screen of a display along with the full citation.

Load The ACM SIGMOD Anthology, CDROM Edition, Volume 1-3, PODS '82-'98. and ... Load The ACM SIGMOD Anthology, Silver Edition, DVD 1, Proceedings. and ... BibTeX

Printed Edition

Proceedings of the Eighth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, March 29-31, 1989, Philadelphia, Pennsylvania. ACM Press 1989, ISBN 0-89791-308-6
Contents BibTeX

Online Edition: ACM Digital Library

References

[A*88]
...
[BB*88]
Isaac Balbin, Graeme S. Port, Kotagiri Ramamohanarao, Krishnamurthy Meenakshi: Efficient Bottom-UP Computation of Queries on Stratified Databases. J. Log. Program. 11(3&4): 295-344(1991) BibTeX
[BC*86]
François Bancilhon, David Maier, Yehoshua Sagiv, Jeffrey D. Ullman: Magic Sets and Other Strange Ways to Implement Logic Programs. PODS 1986: 1-15 BibTeX
[BF88]
...
[BIS67]
...
[BOJ86]
Damjan Bojadziev: A Constructive View of Prolog. J. Log. Program. 3(1): 69-74(1986) BibTeX
[BR87]
Catriel Beeri, Raghu Ramakrishnan: On the Power of Magic. PODS 1987: 269-284 BibTeX
[BRO54]
...
[BRY88a]
...
[BRY88b]
François Bry: Logical Rewritings for Improving the Evaluation of Quantified Queries. MFDBS 1989: 100-116 BibTeX
[CAL79]
...
[CH85]
Ashok K. Chandra, David Harel: Horn Clauses Queries and Generalizations. J. Log. Program. 2(1): 1-15(1985) BibTeX
[CHU56]
...
[CL73]
...
[CLA78]
...
[DEM82]
...
[DF87]
Pierre Deransart, Gérard Ferrand: An Operational Formal Definition of PROLOG. SLP 1987: 162-172 BibTeX
[DIP69]
Robert A. Di Paola: The Recursive Unsolvability of the Decision Problem for the Class of Definite Formulas. J. ACM 16(2): 324-327(1969) BibTeX
[DP60]
Martin Davis, Hilary Putnam: A Computing Procedure for Quantification Theory. J. ACM 7(3): 201-215(1960) BibTeX
[FAG80]
Ronald Fagin: Horn Clauses and Database Dependencies (Extended Abstract). STOC 1980: 123-134 BibTeX
[FIT69]
...
[FIT85]
Melvin Fitting: A Kripke-Kleene Semantics for Logic Programs. J. Log. Program. 2(4): 295-312(1985) BibTeX
[GÖD58]
...
[GAB85]
Dov M. Gabbay: N-Prolog: An Extension of Prolog with Hypothetical Implication II - Logical Foundations, and Negation as Failure. J. Log. Program. 2(4): 251-283(1985) BibTeX
[GAB86]
Dov M. Gabbay: Modal Provability Foundations for Negation by Failure. ELP 1989: 179-222 BibTeX
[GR84]
Dov M. Gabbay, Uwe Reyle: N-Prolog: An Extension of Prolog with Hypothetical Implications I. J. Log. Program. 1(4): 319-355(1984) BibTeX
[GS86]
Dov M. Gabbay, Marek J. Sergot: Negation as Inconsistency I. J. Log. Program. 3(1): 1-35(1986) BibTeX
[HEY66]
...
[HUE80]
Gérard P. Huet: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems. J. ACM 27(4): 797-821(1980) BibTeX
[KER88]
...
[KP88]
...
[KRE65]
...
[KT88]
David B. Kemp, Rodney W. Topor: Completeness of a Top-Down Query Evaluation Procedure for Stratified Databases. ICLP/SLP 1988: 178-194 BibTeX
[KUH67]
...
[LEW85]
...
[LLO84]
John W. Lloyd: Foundations of Logic Programming, 1st Edition. Springer 1984, ISBN 3-540-13299-6
BibTeX
[LT86]
John W. Lloyd, Rodney W. Topor: A Basis for Deductive Database Systems II. J. Log. Program. 3(1): 55-67(1986) BibTeX
[NIC81]
Jean-Marie Nicolas: Logic for Improving Integrity Checking in Relational Data Bases. Acta Inf. 18: 227-253(1982) BibTeX
[PRA65]
...
[PRZ88a]
...
[PRZ88b]
...
[PRZ89]
Teodor C. Przymusinski: Every Logic Program Has a Natural Stratification And an Iterated Least Fixed Point Model. PODS 1989: 11-21 BibTeX
[QUI70]
...
[R*86]
J. Rohmer, R. Lescoeur, Jean-Marc Kerisit: The Alexander Method - A Technique for The Processing of Recursive Axioms in Deductive Databases. New Generation Comput. 4(3): 273-285(1986) BibTeX
[SHE88]
...
[SI88]
Hirohisa Seki, Hidenori Itoh: A Query Evaluation Method for Stratified Programs Under the Extended CWA. ICLP/SLP 1988: 195-211 BibTeX
[TRO77]
...
[TS86]
Hisao Tamaki, Taisuke Sato: OLD Resolution with Tabulation. ICLP 1986: 84-98 BibTeX
[ULL80]
...
[vEK76]
Maarten H. van Emden, Robert A. Kowalski: The Semantics of Predicate Logic as a Programming Language. J. ACM 23(4): 733-742(1976) BibTeX
[VGE88]
...
[VGT87]
Allen Van Gelder, Rodney W. Topor: Safety and Correct Translation of Relational Calculus Formulas. PODS 1987: 313-327 BibTeX
[VIE87]
Laurent Vieille: A Database-Complete Proof Procedure Based on SLD-Resolution. ICLP 1987: 74-103 BibTeX
[VIE88]
...

Referenced by

  1. Raghu Ramakrishnan, Divesh Srivastava, S. Sudarshan, Praveen Seshadri: The CORAL Deductive System. VLDB J. 3(2): 161-210(1994)
  2. Jia-Huai You, Li-Yan Yuan: Three-Valued Formalization of Logic Programming: Is It Needed? PODS 1990: 172-182
  3. John S. Schlipf: The Expressive Powers of the Logic Programming Semantics. PODS 1990: 196-204
  4. Véronique Royer: Backward Chaining Evaluation in Stratified Disjunctive Theories. PODS 1990: 183-195
  5. Kenneth A. Ross: Modular Stratification and Magic Sets for DATALOG Programs with Negation. PODS 1990: 161-171
  6. Hervé Gallaire, Jean-Marie Nicolas: Logic and Databases: An Assessment. ICDT 1990: 177-186
  7. Nicole Bidoit, P. Legay: WELL!: An Evaluation Procedure for All Logic Programs. ICDT 1990: 335-348
  8. Stefano Ceri, Georg Gottlob, Letizia Tanca: What you Always Wanted to Know About Datalog (And Never Dared to Ask). IEEE Trans. Knowl. Data Eng. 1(1): 146-166(1989)
  9. Teodor C. Przymusinski: Every Logic Program Has a Natural Stratification And an Iterated Least Fixed Point Model. PODS 1989: 11-21
  10. François Bry: Logical Rewritings for Improving the Evaluation of Quantified Queries. MFDBS 1989: 100-116
BibTeX
ACM SIGMOD Anthology - DBLP: [Home | Search: Author, Title | Conferences | Journals]
ACM SIGMOD Anthology: Copyright © by ACM (info@acm.org), Corrections: anthology@acm.org
DBLP: Copyright © by Michael Ley (ley@uni-trier.de), last change: Sat May 16 23:33:56 2009