Abstract
Over the last few decades a good deal of research in logic has been prompted by the realization that logical systems can be successfully employed to formalize and solve a variety of computational problems. Traditionally, the theoretical framework for most applications was assumed to be classical logic. However, this assumption often turned out to clash with researchers’ intuitions even in well-established areas of application. Let us consider, for example, what is probably the most representative of these application areas: logic programming The idea that the execution of a Prolog program is to be understood as a derivation in classical logic has played a key role in the development of the area. This interpretation is the leitmotiv of Kowalski’s well-known [1979], whose aim is described as an attempt ‘to apply the traditional methods of [classical] logic to contemporary theories of problem solving and computer programming’. However, here are some quotations which are clearly in conflict with the received view (and with each other) as to the correct interpretation of logic programs:
Relevance Logic not only shows promise as a standard for modular reasoning systems, but it has, in a sense, been already adopted by artificial intelligence researchers. The resolution method for Horn clauses appears to be based on classical logic, but procedural derivation (see [Kowalski, 1979]), the method actually used for logic programming, is not complete for classical logic, and is in fact equivalent to Relevance Logic.[...] the systems of modules which are actually used in computer science have the feature that relevance, not classical logic, provides a theory of their behaviour. [Carson, 1989, p.214]
According to the standard view, a logic program is a definite set of Horn clauses. Thus logic programs are regarded as syntactically restricted first-order theories within the framework of classical logic. Correspondingly, the proof-theory of logic programs is considered as a specialized version of classical resolution, known as SLD-resolution. This view, however, neglects the fact that a program clause a 0 ← a l, a 2, ..., a n , is an expression of a fragment of positive logic [a subsystem of Intuitionistic Logic] rather than an implication formula of classical logic. The logical behaviour of such clauses is in no way related to any negation or complement operation. So (positive) logic programs are ‘sub-classical’. The classical interpretation seems to be a semantical overkill’ [Wagner, 1991, p.835].
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
V. M. Abrusci. Noncommutative intuitionistic linear propositional logic. Zeitschr. f Math. Logik u. Grundlagen d. Math., 36: 297–318, 1990.
V. M. Abrusci. Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic. Journal of Symbolic Logic, 56: 1403–1451, 1991.
G. Allwein and J. M. Dunn. Kripke models for linear logic. the Journal of Symbolic Logic, 58: 514–545, 1993.
G. Amati and F. Pirri. A uniform tableau method for intuitionistic modal logics I. Manuscript, 1993.
A. R. Anderson and N. D. Belnap Jr. Entailment: the Logic of Relevance and Necessity, Princeton University Press, Princeton, 1975.
A. R. Anderson, N. D. Belnap Jr and J. M. Dunn. Entailment: The Logic of Relevance and Necessity. Princeton University Press, Princeton, 1992.
A. Avron. The semantics and proof theory of linear logic. Theoretical Computer Science, 57: 161–184, 1988.
A. Avron. The semantics and proof theory of linear logic. Theoretical Computer Science, 57: 161–184, 1988.
A. Avron. Simple consequence relations. Journal of Information and Computation, 92: 105–139, 1991.
B. Beckert, R. Hähnle, and P. Schmitt. The even more liberalized 6-rule in free-variable semantic tableaux. In G. Gottlob, A. Leitsch, and Daniele Mundici, editors, Proceedings of the 3rd Kurt Gödel Colloquium, Brno, Czech Republic, number 713 in Lecture Notes in Computer Science, pages 108–119. Springer-Verlag, 1993.
M. Bozic and K. Do`en. Models for normal intuitionistic modal logics. Studia Logica, 43: 217–245, 1984.
K. Broda, M. Finger and A. Russo. LDS-Natural Deduction for Substructural Logics. Technical Report DOC 97–11. Department of Computing, Imperial College, 1987. Short version presented at WOLLIC 96, Journal of the IGPL, 4: 486–491.
K. Broda, M. D’Agostino, and. A. Russo. Transformation methods in LDS. In Hans Jiirgen Ohlbach and Uwe Reyle, editors, Logic, Language and Reasoning. Essays in Honor of Dov Gabbay. pp. 347–390. Kluwer Academic Publishers, 1997. To appear.
R. Bull and K. Segerberg. Basic modal logic. In Dov Gabbay and Franz Guenthner, editors, Handbook of Philosophical Logic, volume II, chapter II.I, pages 1–88. Kluwer Academic Publishers, 1984.
M. D’Agostino and D. M. Gabbay. A generalization of analytic deduction via labelled deductive systems.Part I: Basic substructural logics. Journal of Automated Reasoning, 13: 243–281, 1994.
M. D’Agostino and D. M. Gabbay. A generalization of analytic deduction via labelled deductive systems. Part II: full substructural logics. Forthcoming, 1999.
M. D’Agostino, D. M. Gabbay, and A. Russo. Grafting modalities onto substructural implication systems. Studia Logica, 59: 65–102, 1997.
Kosta Dôsen. Sequent systems and groupoid models I. Studia Logica, 47: 353–385, 1988.
K. Dösen. Sequent systems and groupoid models II. Studia Logica, 48: 41–65, 1989.
K. Dôsen. A historical introduction to substructural logics. In P. Schroeder Heister and Kosta Dosen, editors, Substructural Logics, pages 1–31. Oxford University Press, 1993.
M. Dunn. Relevance logic and entailment. In D. M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume III, chapter 3, pages 117–224. Kluwer Academic Publishers, 1986.
G. Fischer-Servi. On modal logic with an intuitionistic base. Studia Logica, 36: 141–149, 1977.
M. Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, Dordrecht, 1983.
D. M. Gabbay. How to construct a logic for your application. In Hans Juergen Ohlbach, editor, GWAI-92: Advances in Artificial Intelligence (LNAI 671), pages 1–30. Springer, 1992.
D. M. Gabbay. Labelled Deductive Systems, Volume I - Foundations. Oxford University Press, 1996.
J. Garson. Modularity and relevant logic. Notre Dame Journal of Formal Logic, 30: 207–223, 1989.
G. Gentzen. Unstersuchungen über das logische Schliessen. Math. Zeitschrift, 39:176–210, 1935. English translation in [Szabo, 1969 ].
J.-Y. Girard. Linear logic. Theoretical Computer Science, 50: 1–102, 1987.
R. Kowalski. Logic For Problem Solving. North-Holland, Amsterdam, 1979.
J. Lambek. The mathematics of sentence structure. Amer. Math. Monthly, 65: 154–169, 1958.
W. MacCaull. Relational semantics and a relational proof system for full Lambek calculus. Technical report, Dept. Mathematics and Computing Sciences, St. Francis Xavier University, 1996.
M. A. McRobbie and N. D. Belnap. Relevant analytic tableaux. Studia Logica, XXXVIII: 187–200, 1979.
M. A. McRobbie and N. D. Belnap. Proof tableau formulations of some first-order relevant orthologics. Bulletin of the Section of Logic, Polish Academy of the Sciences, 13: 233–240, 1984.
R. K. Meyer, M. A. McRobbie, and N. D. Belnap. Linear analytic tableaux. In Peter Baumgartner, Reiner Hanle, and Joachim Posegga, editors, Proceedings of Tableaux ’85, 4th conference on Theorem Proving with Analytic Tableaux and Related Methods, St. Goar, volume 918 of Lecture Notes in Artificial Intelligence, pages 278–293. Springer, 1995.
H. Ono and Y. Komori. Logics without the contraction rule. The Journal of Symbolic Logic, 50: 169–201, 1985.
H. Ono. Semantics for substructural logics. In Peter Schroeder-Heister, editor, Substructural Logics, pages 259–291. Oxford University Press, 1993.
G. D. Plotkin and C. P. Stirling. A framework for intuitionistic modal logic. In J. Y. Halpem, editor, Theoretical Aspects of Reasoning About Knowledge, pages 399–406, 1986.
R. and V. Routley. The semantics of first degree entailment. Noûs, VI: 335–359, 1972.
R. Routley and R. K. Meyer. The semantics of entailment, I. In H. Leblanc, editor, Truth, Syntax and Semantics. North Holland, 1973.
A. Russo. Generalising propositional modal logics using labelled deductive systems. In Proceedings of FroCoS’96, 1996.
G. Sambin. The semantics of pretopologies. In Peter Schroeder-Heister, editor, Substructural Logics, pages 293–307. Oxford University Press, 1993.
A. K. Sympson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh, 1993.
A. Tarski. Fundamentale begriffe der methodologie der deduktiven wissenschaften, I. Monatshefte ftir Mathematik und Physik, 37: 361–404, 1930.
A. Tarski. Über einige fundamentale begriffe der metmathematik. Comptes Rendus des Séances de la Société des Sciences et des Lettres de Varsovie, 23: 22–29, 1930.
P. B. Thistlewaite, M. A. McRobbie, and B. K. Meyer. Automated Theorem Proving in Non Classical Logics. Pitman, 1988.
A. Urquhart. Semantics for relevant logic. The Journal of Symbolic Logic, 37: 159–170, 1972.
A. Urquhart. The undecidability of entailment and relevant implication. Journal of Symbolic Logic, 49: 1059–1073, 1984.
J. van Benthem, Language in Action: Categories, Lambdas and Dynamic Logic, North-Holland, Amsterdam, 1991.
G. Wagner. Logic programming with strong negation and inexact predicates. Journal of Logic and Computation, 1: 835–859, 1991.
H. Wansing. The Logic of Information Structures. Number 681 in Lecture Notes in Artificial Intelligence. Springer-Verlag, Berlin, 1993.
A. H. William. The formuale-as-types notion of construction. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logics, Lambda Calculus and Formalism. Academic Press, London, 1980.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
D’Agostino, M., Gabbay, D., Broda, K. (1999). Tableau Methods for Substructural Logics. In: D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J. (eds) Handbook of Tableau Methods. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-1754-0_7
Download citation
DOI: https://doi.org/10.1007/978-94-017-1754-0_7
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5184-4
Online ISBN: 978-94-017-1754-0
eBook Packages: Springer Book Archive