nach oben

Erschienen in:

2013 | OriginalPaper | Buchkapitel

5. The Logical Spreadsheet

verfasst von : Iliano Cervesato

Erschienen in: The Deductive Spreadsheet

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

This chapter provides a logical interpretation of the resulting relational spreadsheet as the nonrecursive fragment of a suitable flavor of Datalog enriched with negation and constraints. The theory of this language is developed into a model that emphasizes the unique requirements of a spreadsheet. In particular, it provides a logical account of key spreadsheet functionalities such as evaluation, update and explanation. A spreadsheet based on this interpretation can already be called “deductive”, for a very weak notion of deduction.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel The Relational Spreadsheet

Nächstes Kapitel The Deductive Spreadsheet

Many authors fix the term language of first-order logic to be the free algebra generated by a set of constants, an infinite set of variables, and a set of constructors. Although we will rely on a simple instance of precisely this scheme, there is no reason not to allow more liberal languages, for example, featuring types, equational rewriting, or binders.

The correspondence between a domain of interest and a logical representation is an entirely different question.

See footnote 4 for a brief description of how to incorporate scalar and array formulas in the present discussion.

This translation can easily be extended [vEOT86] to express the scalar part of a spreadsheet by associating each cell l with a unary predicate l(v _l) containing the value of l. Then, every scalar expression e is interpreted into a pair e ^∗ = (æ, B) as follows:

$$\displaystyle{\begin{array}{llll} {l}^{{\ast}} & = & (L_{l},l(L_{l})) & \text{where}\ L_{l}\ \text{is a variable uniquely assigned to cell l} \\ {v}^{{\ast}} & = & (v,\mathit{true}) \\ \mathit{op}(e_{1},\ldots,e_{n}) & = & (op(\mathit{\ae }_{1},\ldots,\mathit{\ae }_{n}),B_{1} \wedge \ldots \wedge B_{n}) & \text{where }e_{i}^{{\ast}} = (\mathit{\ae }_{i},B_{i})\text{ for }i = 1..n \end{array} }$$

Finally, every binding l↦e in a spreadsheet s is modeled by inserting the formula

$$\displaystyle{X = \mathit{\ae } \wedge B \rightarrow l(X)}$$

into cell l, where e ^∗ = (æ, B).

While this approach extends to array formulas, it does not take into consideration partial interactions with calculated relational expressions, such as in Fig. 4.7 where a scalar expression draws its input from a relational result. Although this could be addressed using the techniques described in Sect. 5.2.3, we are more inclined to take the more conservative path of relying on tested approaches.

It should be observed that every fact $p(\vec{v})$ is logically equivalent to the clause $p(\vec{X}) \leftarrow \vec{X} = \vec{v}$. Furthermore, the transformation in Sect. 5.2.2 may itself produce clauses in this form. For these reasons, many presentations in the literature, especially those concerned with general logic programming [Llo87] more than Datalog, dispense with factual theories altogether by bundling facts in the clausal component $\Gamma$. In our context, keeping the distinction between facts derived from primitive predicates and clauses obtained by translating complex relational expressions will prove advantageous, both conceptually and in terms of presentation.

This expression will be our final definition for $T_{\Pi,\Gamma }$ for definite programs. As mentioned in footnote 5, it is uncommon to draw a separation between facts and clauses in a definite theory since a fact can be seen as a particular case of a clause. The above operator assumes a slightly different form in that case, which is commonly seen in the logic programming literature [Llo87; EK76]:

The two formulations can easily be shown to be equivalent.

Another approach, embraced by a certain flavor of parallel logic programming, considers all the choices at once. We will not investigate it further because commercial implementations still use the more traditional sequential model and there is a substantial overhead in managing parallelism.

In classical logic, this clause is logically equivalent to q(X) ← ¬p(X) ∧ r(X), which underlies a further justification for the second model, and explains the symmetry between them.

A more general notion, local stratification [Prz87; CGT90], admits a larger class of theories by taking into consideration the ground predicates of a theory rather than just the predicate symbols that appear in a clause. The added class of theories is however likely to be inconsequential in the spreadsheet context. Moreover, local stratifiability is undecidable.

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 is the first systematic investigation of focusing, a proof technique that underlies much of the recent research in logic programming. Focusing relies on the observation that, when in a proof, some steps can be permuted without affecting the ability to complete the proof. Focusing systematically delays some steps while eagerly carrying out others, which results in a very efficient strategy.

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 dissertation combines two established approaches to automate reasoning more effectively in a refinement of traditional logic called linear logic. These are the inverse method, due to Maslov, and Andreoli’s focusing [And92].

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 work extends [vEOT86] to tables in the sense of relational algebra. It is still heavily based on incremental queries but now supports the display of multiple solutions in a tabular way. The implementation is based on the recently introduced graphical display. Several windows show different views of the system. However the basic input mode is still essentially through the command lines, with other windows used only for displaying results in a tabular way.

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 is the original paper on linear logic. It describes in great detail its proof-theory and several forms of semantics for it.

This paper explores negation-as-failure in the context of hereditary Harrop formulas, which differ from the Horn clauses on which Prolog is founded by allowing embedded implication and quantification in the body of clauses. The paper extends the classical model semantics of Horn clauses to an intuitionistic one based on Kripke models. Particularly interesting is the treatment of extensional universal quantification.

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 paper describes the first attempt at marrying the proof-theoretic approach to logic programming pioneered in [MNPS91] with linear logic, a then-novel logic to reason about resources rather than truths. The result was Lolli, the first linear logic programming language. The paper also applies it to numerous examples in areas such as theorem proving, natural language parsing, and data base programming, and it explores its model theory.

This dissertation expands Andreoli’s use of focusing [And92] from linear logic to mainstream intuitionistic logic.

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

This is a classical textbook on mathematical logic by one of the masters of the field.

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

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 synthesizes in a single presentation some of the best results that have been proposed about focusing and polarization. Focusing guides the task of executing a logic program or searching for a proof in logic, while polarization systematically decorates formulas to direct and enable focusing.

This paper is an interesting account of the development of the theory of fixpoints.

This paper introduces Lollimon, a concurrent linear logic programming language inspired by CLF [WCPW03]. Lollimon combines Prolog-style backward-chaining inference with several forms of forward-chaining (Datalog-style saturation for persistent programs, and quiescence for terminating linear programs). Backward- and forward-chaining are regulated by a monad.

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

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 paper gives a thorough characterization of polarization in the computation-as-proof-search paradigm. In particular, it shows that the standard backward and forward strategies for Prolog and Datalog correspond simply to two different polarizations of atomic formulas in focused proofs.

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 forthcoming textbook gives a modern presentation of logic geared towards computer scientists. It develops logic around the general notion of judgment rather than truth. Special attention is given to the computational uses of logic, with a rigorous development of the operational aspects of logic programming out of pure logic foundations.

This is the original paper on local stratification.

This is the original paper on the closed world assumption.

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 revisits the premises by which a generic logical derivation can be transformed into a focused derivation, thereby replacing the “long and tedious proofs”, which producing such a result has required so far, with a simple structural argument.

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

This paper describes an implementation of the concept of incremental query, by which a standard Prolog query can be refined interactively, and its application for solving spreadsheet-like problems. The output takes the form of the rudimentary, teletype-based, spreadsheets of the time; the input is however still given from the command line. While taking limited advantage of the input facilities of a spreadsheet, this extends their typical functionalities with forms of symbolic reasoning. Multiple solutions are however shown one at a time. The whole system is implemented in Prolog, and efficiently realizes top-down search with intelligent backtracking. The claims to target relatively smart users rather than expert programmers is hardly met.

[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. ¹¹

[And92].

Andreoli, J. -M. (1992). Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3), 297–347. ¹²

[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. ¹⁴

[Cha06].

Chaudhuri, K. (2006). The focused inverse method for linear logic. PhD thesis, Computer Science Department, Carnegie Mellon University. ¹⁵

[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. ¹⁷

[CvEL88].

Cheng, M. H. M., van Emden, M. H., & Lee, J. H. -M. (1988). Tables as a user interface for logic programs. In Fifth generation computer systems, Tokyo (pp. 784–791). ¹⁸

[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. ¹⁹

[Gir87].

Girard, J. -Y. (1987). Linear logic. Theoretical Computer Science, 50, 1–102. ²⁰

[Har93].

Harland, J. (1993). Success and failure for hereditary Harrop formulae. Journal of Logic Programming, 17(1), 1–29. ²¹

[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). ²²

[HM94].

Hodas, J. S., & Miller, D. (1994). Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110(2), 327–365. ²³

[How98].

Howe, J. M. (1998). Proof search issues in some non-classical logics. PhD thesis, University of St Andrews. ²⁴

[JM94].

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

[Kle67].

Kleene, S. C. (1967). Mathematical logic. New York: Wiley. ²⁶

[Kow79].

Kowalski, R. A. (1979). Logic for problem solving. Prentice Hall. ²⁷

[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. ²⁹

[LM09].

Liang, C., & Miller, D. (2009). Focusing and polarization in linear, intuitionistic, and classical logic. Theoretical Computer Science, 410(46), 4747–4768. ³⁰

[LNS82].

Lassez, J. -L., Nguyen, V. L., & Sonenberg, L. (1982). Fixed point theorems and semantics: A folk tale. Information Processing Letters, 14(3), 112–116. ³¹

[LPPW05].

López, P., Pfenning, F., Polakow, J., & Watkins, K. (2005). Monadic concurrent linear logic programming. In A. Felty (Ed.), Proceedings of the 7th international symposium on principles and practice of declarative programming – PPDP’05, Lisbon (pp. 35–46). ACM. ³²

[Men97].

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

[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. ³⁵

[NM10].

Nigam, V., & Miller, D. (2010). A framework for proof systems. Journal of Automated Reasoning, 45(2), 157–188. ³⁶

[O’K90].

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

[Pfe].

Pfenning, F. (Forthcoming). Computation and deduction. Cambridge University Press. ³⁸

[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. ³⁹

[Rei78].

Reiter, R. (1978). On closed world data bases. In H. Gallaire & J. Minker (Eds.), Logic and data bases (pp. 55–76). New York: Plenum. ⁴⁰

[Rob65].

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

[Sim12].

Simmons, R. J. (2012). Structural focalization. Available at http://arxiv.org/pdf/1109.6273v3.pdf. ⁴²

[SS94].

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

[vEOT86].

van Emden, M. H., Ohki, M., & Takeuchi, A. (1986). Spreadsheets with incremental queries as a user interface for logic programming. New Generation Computing, 4(3), 287–304. ⁴⁴

Titel: The Logical Spreadsheet
verfasst von: Iliano Cervesato
Verlag: Springer Berlin Heidelberg
Buch: The Deductive Spreadsheet
Print ISBN: 978-3-642-37746-4

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

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

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"