Top

Published in:

2013 | OriginalPaper | Chapter

6. The Deductive Spreadsheet

Author : Iliano Cervesato

Published in: The Deductive Spreadsheet

Publisher: Springer Berlin Heidelberg

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

This chapter defines the deductive spreadsheet proper by adding recursion to the logical interpretation provided in Chap. 5, hence turning it into a constrained form of Datalog with negation. This step provides a substantial boost in expressiveness while requiring only small theoretical adjustments. It also enables further extensions, notably the ability to weave simple lists into the language. The added deductive power, which includes inferential closure, hypothetical reasoning and some form of aggregation, is illustrated by way of examples.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

It should be noted that this problem can also be solved in a purely functional manner by relying on the extended array operators \(\vec{\sigma }\) and \(\vec{\pi }\) introduced in Chap. 4. A purely clausal solution is also possible, but requires further extensions to our language. It will be examined in Sect. 6.5.

It should be noted that the appellation semi-naïve evaluation is usually reserved for the technique we are about to present, which reaps benefits only for recursive definitions, rather than the general approach we have been developing (which will include this technique as a subroutine). We justify broadening the use of this terminology by the fact that our previous efforts are in the same spirit as this better recognized but also more specialized application.

To be fully precise, the theoretical expressiveness will remain the same as in our current language, but in the majority of circumstances it will provide the illusion of a language with unrestricted head constraints.

In the above examples, the syntax [_ | _] is also used as a destructor in the conjunct L ′ = [Y | L ′]: it does not construct L ′ by combining Y and L ′, but instead checks that the first element of L ′ is Y. While such traditional usage of the list constructor has a simple formalization based on pattern-matching, an approach more in line with our language would introduce an operation, head, which returns the first element of its argument and express this constraint as Y = head(L ′).

See http://genealogy.math.ndsu.nodak.edu/

This simple but rather stringent restriction could be loosened by performing a form of dataflow analysis known as mode checking [DW88; Sar10]. In order for a clause to be acceptable, the mode analysis shall certify that X can always be instantiated before attempting to solve the embedded implication.

This influential paper identifies the notion of stratification as an effective approach to embedding negation in logic programming, both computationally and cognitively. It develops its general theory and fixpoint semantics, and specializes SLD-resolution to it.

This paper develops the characterization of the model semantics of logic programs consisting of Horn clauses (i.e., pure Prolog) as the least fixpoint of a continuous operator. It also observes that some forms of finite-failure (but not all) correspond to its greatest fixpoint.

This paper describes Forms/3, a conservative extension of the traditional spreadsheet with procedural abstractions such as recursion, data abstractions such as graphical values, and graphic time-based output. As it does so, it strives to maintain the usability characteristics that have made the spreadsheet popular with end-users.

This dissertation explores a principled way to extend deductive databases with hypothetical reasoning. It does so by allowing the body of a clause to mention “embedded clauses”. This adds significantly to the expressive power of the language, a fact that is thoroughly analyzed in the context of complexity theory. The model theory of this extension is investigated in [BM90] while the key insight was already present in [BMV89].

This paper develops the author’s dissertation [Bon91] by focusing on forms of hypothetical reasoning that only add temporary facts in a deductive database and create new constants dynamically. It explores its proof-theory, its model theory, and the computational complexity of the extended language.

This expanded version of [CGT89] is an excellent survey with some in-depth analysis of important concepts, in particular semantics, optimizations and the interface with actual databases. It covers the experimental deductive database system of the time at length.

This paper provides a detailed classification of the expressive powers of various fragments of relational algebra and (extensions of) Datalog. It is particularly concerned with how different forms of negation impact expressiveness.

This is the original article on negation-as-failure.

This book is a classic introductory text to Prolog. Generations of students have relied on it to learn logic programming to build applied programs.

This technical report is widely considered to be the first mention on what was to become Prolog. Its original application was the processing of natural language (French, to be precise).

This book is one of the best introductory accounts of what can be done with a deductive database. Specifically, it explores in great depth problems that combine large sets of data and require a truly deductive form of inference, above and beyond what the relational data model has to offer. It targets people who will be using a deductive database as a tool more than students interested in the underlying theory.

This paper describes a method for automatically determining correct input/output mode declarations in a Prolog program. This permits us to specialize the operational interpretation of a program, thereby achieving greater efficiency.

This is a classic paper on the foundations of logic programming. It defines top-down evaluation and the fixpoint semantics, and relates them to proof- and model-theory respectively.

This paper considers an extension of a logical language for deductive databases with embedded implication based on [Mil89]. It explores implicational stratification of programs, a model-theoretic semantics, and a fixpoint semantics, but limits the antecedent of embedded implications to universally closed formulas. In particular, there is no sharing of variables with the parent clause.

This article contains an in-depth discussion of the semi-naïve strategy.

This collection contains many of the very first papers on using logic programming in the context of data- and knowledge-bases. The seminal work on the closed world assumption and negation-as-failure first appeared in it.

This paper proposes a precise model of the run-time of a logic program that supports using logic programs for studying the execution time of algorithms.

This is an early proposal to use theorem proving for problem solving.

This paper develops the proof-theory of negation-as-failure for hereditary Harrop formulas, whose body formulas admit embedded clauses. To this effect, it defines a proof theory for non-derivability in intuitionistic logic.

This is the original paper on constraint logic programming, a paradigm that seamlessly incorporates constraints over generic domains within logic programming in the style of Prolog. The result is a family of languages, one for each specific domain and accompanying constraint-solving procedures, that retain the declarative nature of logic for programming purposes, but specializes it to domains of interest in a natural way.

This paper surveys the foundations, applications and developments of constraint logic programming since its inception in [JL87].

This paper proposes an approach to representing and retrieving data in a database that stores information not as facts (or tuples), but as a conjunction of simple constraints over a given domain. This is especially useful for applications, such as geographic databases, where objects of interest are naturally expressed as constraints, spatial constraints in this case.

This collection surveys the then-nascent field of constraint databases, with contributions by many of it pioneers. Constraint databases rely on constraints to describe some types of data, for example temporal or spatial data, and to draw inferences from them in an efficient way.

This classic book investigates the application of logic to problem solving and computer programming using Prolog.

This work refines [Kri82] and implements its design as a system called LogiCalc. Its initial goal was to “reconstruct logically, in micro-Prolog, a typical spreadsheet program”. Besides capturing most of the functionalities of early spreadsheets, it provides powerful extensions such as relational manipulations, integrity constraints, bidirectional variables, symbolic reasoning, and complex objects (e.g., lists, graphics and spreadsheets themselves). It is based on the limited teletype interface that predated the widespread availability of graphical user interfaces with windows. LogiCalc relies a lot on user input, even for non-essential tasks.

This paper models the propagation of the assertion of new facts or the retraction of old facts in the Datalog system by means of inference in linear logic. To this effect, it translates Datalog clauses into linear logic formulas that also contain specifications about how to propagate updates.

This is the classical textbook on the theory of logic programming: it collects and unifies results on SLD-resolution, unification, model and fixpoint semantics, negation-as-failure, that had appeared in separate papers. It does not consider any of the recent proof-theoretic developments, but it is a valuable reference. As such, it has been used by generations of students and scholars of logic programming.

This paper shows how Datalog can fruitfully be used to specify access control and trust management policies in order to decide authorization and access in a distributed system of computers. To this effect, it extends Datalog with constraints over signed messages. The paper explores the theoretical properties of the resulting language and relates it to other authorization and trust management languages.

This paper examines proof irrelevance, a mechanism for selectively hiding the identities of terms in type theories, and relates it to refinement types, a powerful approach to classify terms.

This paper describes a method for transforming a Datalog program into an efficient specialized implementation with guaranteed worst-case time and space complexities. The transformation exploits fixed-point computation, incremental maintenance of invariants, and combinations of indexed and linked data structures.

This paper describes a method for computing run-time complexity bounds for Datalog programs. More generally, it shows that specifying an algorithm using Datalog is beneficial for reasoning about its complexity.

This is another good textbook on mathematical logic. It is notable for its breadth of topics.

This paper explores the theory and application of a general language of Horn clauses augmented with embedded implication and quantification (hereditary Harrop formulas), which goes well beyond Datalog. It studies its proof theory, model theory and fixpoint semantics in an intuitionistic setting. It shows how embedded clauses provide a foundational justification for parametric modules in logic programming.

This book collects original articles by the main players of the then-nascent and very fertile field of deductive databases. It grew out of a workshop by the same title held in Washington, DC the year before.

This now classic paper was the first to establish top-down logic programming on solid proof-theoretic grounds. The methodology it embraced, based on the notion of uniform proofs, identified fragments of logic larger than Prolog’s Horn clauses that could be used for programming. Specifically, it shows that hereditary Harrop formulas, which extend Horn clauses with embedded implication, fit into this pattern, and so do higher-order variants of both languages.

This paper explores an efficient asynchronous algorithm to incrementally compute the changes to the states of a distributed Datalog system, as proposed in some network protocols and multi-agent systems, in response to the insertions and deletions of base facts.

This classic textbook focuses on advanced programming techniques in Prolog as well as on universal programming notions such as elegance and understanding a problem before starting to write code. It is best read after [CM87] or [SS94].

This paper describes the Elf system, which provides a type-checker, type-reconstruction support, and top-down execution in the style of Prolog to the LF type theory.

This volume brings together the principal approaches to weaving types in logic programming. Essays within describe specific techniques but also emphasize the overall benefits of types, including reduced error rates, support for modularity, and compilation assistance.

This is the original paper on local stratification.

This paper describes Twelf, a reimplementation of the Elf system [Pfe89] extended with theorem-proving capabilities for specifications written in the LF type theory.

This classic paper sets the foundations of theorem proving and introduces the resolution principle, which is one of the tenets of top-down evaluation in logic programming.

This paper reviews the state of the art of bottom-up evaluation and proposes a transformation on Datalog programs to speed up that semi-naïve evaluation. It also discusses extensions to negation, set terms, constraints and quantitative reasoning. Comparisons with numerous systems are included.

This thesis examines in great detail, among other things, mode-checking and termination in the Twelf system, which embeds a higher-order logic programming language with a top-down execution semantics.

This work proposes to combine logic programming and spreadsheets under the umbrella of the PERPLEX system. It does so by making heavy use of integrity constraints in a way that is clearly expressive, but likely to be unnatural for an entry-level user. PERPLEX supports exploratory programming and the paradigm of “query-by-example” to perform many programming tasks. While very powerful, it is not clear that this blends smoothly in the spreadsheet mindset. This is the first logical spreadsheet extension to make use of graphical input and not just output.

This paper studies in great detail to what depth it is sufficient to expand a derivation tree for a top-down evaluation of a logic program. It also leverages properties such as transitivity and subsumption, as well as characteristics of the domain to extend the class of prunable programs.

This is another classic introductory textbook on programming in Prolog that has been used by generations of students.

This two-volume set is a now classic reference to constructive logic and its applications in a variety of fields. It covers intuitionistic logic both at an introductory level and in exhaustive depth.

XSB is Prolog with a form of memoization called tabling. Declaratively, it does not differ substantially from Prolog. Procedurally, however, it substantially improves on the standard top-down SLDNF resolution strategy of this language by nearly eradicating control-induced infinite loops. In particular, an XSB query always terminates against a Datalog program. Tabling can also have a positive effect on efficiency, although this may depend on how the user writes his programs. This makes XSB a promising candidate as the underlying explanation engine of a deductive spreadsheet.

[ABW87].

Apt, K. R., Blair, H. A., & Walker, A. (1987). Towards a theory of declarative knowledge. In J. Minker (Ed.), Foundations of deductive databases and logic programming [Min87] (pp. 89–148). Los Altos: Morgan Kaufmann. ⁷

[AvE82].

Apt, K. R., & van Emden, M. H. (1982). Contributions to the theory of logic programming. Journal of the ACM, 29(3), 841–862. ⁸

[BAD + 01].

Burnett, M., Atwood, J., Djang, R. W., Reichwein, J., Gottfried, H., & Yang, S. (2001). Forms/3: A first-order visual language to explore the boundaries of the spreadsheet paradigm. Journal of functional programming, 11(2), 155–206. ⁹

[Bon91].

Bonner, A. J. (1991). Hypothetical reasoning in deductive databases. PhD thesis, Rutgers University. ¹⁰

[Bon94].

Bonner, A. J. (1994). Hypothetical reasoning with intuitionistic logic. In R. Demolombe & T. Imielinski (Eds.), Non-standard queries and answers (Studies in logic and computation, chapter 8, pp. 187–219). Oxford: Oxford University Press. ¹¹

[CGT90].

Ceri, S., Gottlob, G., & Tanca, L. (1990). Logic programming and databases. Berlin/New York: Springer. ¹²

[CH85].

Chandra, A. K., & Harel, D. (1985). Horn clause queries and generalizations. Journal of Logic Programming, 1, 1–15. ¹³

[Cla78].

Clark, K. L. (1978). Negation as failure. In H. Gallaire & J. Minker (Eds.), Logic and data bases (pp. 293–322). New York: Plenum. ¹⁴

[CM87].

Clocksin, W. F., & Mellish, C. S. (1987). Programming in Prolog (3rd ed.). Berlin/New York: Springer. ¹⁵

[Col70].

Colmerauer, A. (1970). Les systèmes-Q ou un formalisme pour analyser et synthétiser des phrases sur ordinateur. Technical report, Department of Computer Science, University of Montreal, Montreal. ¹⁶

[Col98].

Colomb, R. M. (1998). Deductive databases and their applications. London/Bristol: Taylor & Francis. ¹⁷

[DW88].

Debray, S. K., & Warren, D. S. (1988). Automatic mode inference for logic programs. Journal of Logic Programming, 5, 207–229. ¹⁸

[EK76].

Van Emden, M. H., & Kowalski, R. A. (1976). The semantics of predicate logic as a programming language. Journal of the ACM, 23(4), 733–742. ¹⁹

[Fre92].

Freitag, B. (1992). Extending deductive database languages by embedded implications. In A. Voronkov (Ed.), Proceedings of the third international conference on logic programming and automated reasoning – LPAR’92, St. Petersburg (Lecture notes in computer science, Vol. 642, pp. 84–95). Springer. ²⁰

[GKB87].

Güntzer, U., Kiessling, W., & Bayer, R. (1987). On the evaluation of recursion in (deductive) database systems by efficient differential fixpoint iteration. In Proceedings of the third international conference on data engineering, Los Angeles (pp. 120–129). IEEE Computer Society. ²¹

[GM78].

Gallaire, H., & Minker, J. (Eds.). (1978). Logic and data bases. New York: Plenum. ²²

[GM02].

Ganzinger, H., & McAllester, D. (2002). Logical algorithms. In Proceedings of the 18th international conference on logic programming – ICLP’02, London (pp. 209–223). Springer. ²³

[Gre69].

Green, C. (1969). Application of theorem proving to problem solving. In D. E. Walker & L. M. Norton (Eds.), Proceedings of the international joint conference on artificial intelligence, Washington, DC (pp. 219–239). ²⁴

[Har94].

Harland, J. (1994). Towards a sequent calculus for negation as failure. In Proceedings of the workshop on proof-theoretical extensions of logic programming, Santa Margherita Ligure (pp. 19–27). ²⁵

[JL87].

Jaffar, J., & Lassez, J. -L. (1987). Constraint logic programming. In Proceedings of the 14th symposium on principles of programming languages – POPL’87, Munich (pp. 111–119). ²⁶

[JM94].

Jaffar, J., & Maher, M. J. (1994). Constraint logic programming: A survey. Journal of Logic Programming, 19/20, 503–581. ²⁷

[KKR95].

Kanellakis, P., Kuper, G., & Revesz, P. (1995). Constraint query languages. Journal of Computer and System Sciences, 51(1), 26–52. ²⁸

[KLP00].

Kuper, G., Libkin, L., & Paredaens, J. (Eds.). (2000). Constraint databases. Berlin/New York: Springer. ²⁹

[Kow79].

Kowalski, R. A. (1979). Logic for problem solving. Prentice Hall. ³⁰

[Kri88].

Kriwaczek, F. (1988). Logicalc: A Prolog spreadsheet. Machine intelligence, 11, 193–208. ³¹

[LC12].

Lam, E. S. L., & Cervesato, I. (2012). Modeling datalog fact assertion and retraction in linear logic. In A. King (Ed.), Proceedings of the 14th international ACM symposium on principles and practice of declarative programming – PPDP’12, Leuven. ³²

[Llo87].

Lloyd, J. W. (1987). Foundations of logic programming (2nd extended ed.). Berlin/New York: Springer. ³³

[LM03].

Li, N., & Mitchell, J. C. (2003). Datalog with constraints: A foundation for trust management languages. In Proceedings of the fifth international symposium on practical aspects of declarative languages (PADL’03), New Orleans. ³⁴

[LP09].

Lovas, W., & Pfenning, F. (2009). Refinement types as proof irrelevance. In P. -L. Curien (Ed.), Proceedings of the 9th international conference on typed lambda calculi and applications – TLCA’09, Brasilia (Lecture notes in computer science, Vol. 5608, pp. 157–171). Springer. ³⁵

[LS09].

Liu, Y., & Stoller, S. (2009). From datalog rules to efficient programs with time and space guarantees. ACM Transactions on Programming Languages and Systems – TOPLAS, 31(6), 1–38. ³⁶

[McA02].

McAllester, D. (2002). On the complexity analysis of static analyses. Journal of the ACM, 49, 512–537. ³⁷

[Men97].

Mendelson, E. (1997). Introduction to mathematical logic (4th ed.). Princeton: Van Nostrand-Reinhold. ³⁸

[Mil89].

Miller, D. (1989). A logical analysis of modules in logic programming. Journal of Logic Programming, 6(1–2), 79–108. ³⁹

[Min87].

Minker, J. (Ed.). (1987). Foundations of deductive databases and logic programming. Los Altos: Morgan Kaufmann. ⁴⁰

[MNPS91].

Miller, D., Nadathur, G., Pfenning, F., & Scedrov, A. (1991). Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51, 125–157. ⁴¹

[NJLS11].

Nigam, V., Jia, L., Loo, B. T., & Scedrov, A. (2011). Maintaining distributed logic programs incrementally. In Proceedings of the 13th international ACM symposium on principles and practice of declarative programming – PPDP’11, Odense (pp. 125–136). ACM. ⁴²

[O’K90].

O’Keefe, R. A. (1990). The craft of Prolog. Cambridge: MIT. ⁴³

[Pfe89].

Pfenning, F. (1989). Elf: A language for logic definition and verified meta-programming. In Fourth annual symposium on logic in computer science, Pacific Grove (pp. 313–322). IEEE Computer Society Press. ⁴⁴

[Pfe92].

Pfenning, F. (Ed.). (1992). Types in logic programming. Cambridge: MIT. ⁴⁵

[Prz87].

Przymusinski, T. C. (1987). On the declarative semantics of stratified deductive databases and logic programs. In J. Minker (Ed.), Foundations of deductive databases and logic programming [Min87] (pp. 193–216). Los Altos: Morgan Kaufmann. ⁴⁶

[PS99].

Pfenning, F., & Schürmann, C. (1999). System description: Twelf – A meta-logical framework for deductive systems. In Proceedings of the 16th international conference on automated deduction – CADE-16, Trento (Lecture notes in artificial intelligence, Vol. 1632, pp. 202–206). Springer. ⁴⁷

[Rob65].

Robinson, J. A. (1965). A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1), 23–41. ⁴⁸

[RSS92].

Ramakrishnan, R., Srivastava, D., & Sudarshan, S. (1992). Efficient bottom-up evaluation of logic programs. In P. Dewilde & J. Vandewalle (Eds.), The state of the art in computer systems and software engineering. Kluwer Academic. ⁴⁹

[Sar10].

Sarnat, J. (2010). Syntactic finitism in the metatheory of programming languages. PhD thesis, Department of Computer Science, Yale University. ⁵⁰

[SB89].

Spenke, M., & Beilken, C. (1989). A spreadsheet interface for logic programming. In CHI’89: Proceedings of the SIGCHI conference on human factors in computing systems, Austin (pp. 75–80). ACM. ⁵¹

[SGG86].

Smith, D. E., Genesereth, M. R., & Ginsberg, M. L. (1986). Controlling recursive inference. Artificial Intelligence, 30(3), 343–389. ⁵²

[SS94].

Sterling, L., & Shapiro, E. (1994). The art of Prolog (2nd ed.). Cambridge: MIT. ⁵³

[TvD88].

Troelstra, A. S., & van Dalen, D. (Eds.). (1988). Constructivism in mathematics: An introduction. Amsterdam/New York: North-Holland. ⁵⁴

[War98].

Warren, D. S. (1998). Programming with tabling in XSB. In D. Gries & W. P. de Roever (Eds.), Programming concepts and methods, IFIP TC2/WG2.2,2.3 international conference on programming concepts and methods (PROCOMET’98): Vol. 125 of IFIP conference proceedings, Shelter Island (pp. 5–6). Chapman & Hall. ⁵⁵

Title: The Deductive Spreadsheet
Author: Iliano Cervesato
Publisher: Springer Berlin Heidelberg
Book: The Deductive Spreadsheet
Print ISBN: 978-3-642-37746-4

Electronic ISBN: 978-3-642-37747-1

Copyright Year: 2013
DOI: https://doi.org/10.1007/978-3-642-37747-1_6

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner