Skip to main content
SpringerLink
Log in

Goal-Oriented Deductions

  • Chapter
Book cover Handbook of Philosophical Logic

Part of the book series: Handbook of Philosophical Logic ((HALO,volume 9))

Abstract

The topic of this chapter is to present a general methodology for automated deduction inspired by the logic programming paradigm. The methodology can and has been applied to both classical and non-classical logics. It comes without saying that the landscape of non-classical logics applications in computer science and artificial intelligence is now wide and varied, and this Handbook itself is a witness this fact. We will survey the application of goaldirected methods to classical, intuitionistic, modal, and substructural logics. For background information about these logical systems we refer to other chapters of this Handbook and to [Fitting, 1983; Anderson and Belnap, 1975; Anderson et al., 1992; Gabbay, 1981; Troelstra, 1969; Dummett, 2001; Restall, 1999] . Our treatment will be confined to the propositional level.1

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Bibliography

  1. M. Abadi and Z. Manna. Temporal logic programming. Journal of Symbolic Computation, 8, 277–295, 1989.

    Article  Google Scholar 

  2. J. M. Andreoli. Logic programming with focusing proofs in linear logic. Journal Logic and Computation, 2, 297–347, 1992.

    Article  Google Scholar 

  3. J. M. Andreoli and R. Pareschi. Linear objects: logical processes with built in inheritance. New Generation Computing, 9, 445–474, 1991.

    Article  Google Scholar 

  4. A. R. Anderson and N. D. Belnap. Entailment, The Logic of Relevance and Necessity, Vol. 1. Princeton University Press, New Jersey, 1975.

    Google Scholar 

  5. A. R. Anderson, N. D. Belnap and J. M. Dunn. Entailment, The Logic of Relevance and Necessity, Vol. 2. Princeton University Press, New Jersey, 1992.

    Google Scholar 

  6. M. Baldoni, L. Giordano and A. Martelli. A modal extension of logic programming, modularity, beliefs and hypothetical reasoning. Journal of Logic and Computation, 8, 597–635, 1998.

    Article  Google Scholar 

  7. D. Basin, S. Matthews and L. Viganò. Labelled propositional modal logics: theory and practice. Journal of Logic and Computation, 7, 685–717, 1997.

    Article  Google Scholar 

  8. D. Basin, S. Matthews and L. Viganà. A new method for bounding the complexity of modal logics. In Proceedings of the Fifth Gödel Colloquim, pp. 89–102, LNCS 1289, Springer-Verlag, 1997.

    Google Scholar 

  9. D. Basin, S. Matthews and L. Viganò. Natural deduction for non-classical logics. Studia Logica, 60, 119–160, 1998.

    Article  Google Scholar 

  10. A. W. Bollen. Relevant logic programming, Journal of Automated Reasoning, 7, 563–585, 1991.

    Article  Google Scholar 

  11. K. Došen. Sequent systems and grupoid models I. Studia Logica, 47, 353–385, 1988.

    Article  Google Scholar 

  12. K. Došen. Sequent systems and grupoid models II. Studia Logica, 48, 41–65, 1989.

    Article  Google Scholar 

  13. M. Dummett. Elements of Intuitionism, Oxford University Press, (First edn. 1977), second edn., 2001.

    Google Scholar 

  14. J. M. Dunn. Relevance logic and entailment. In Handbook of Philosophical Logic, vol III, D. Gabbay and F. Guenthner, eds. pp. 117–224. D. Reidel, Dordercht, 1986.

    Google Scholar 

  15. R. Dyckhoff. Contraction-free sequent calculi for intuitionistic logic, Journal of Symbolic Logic, 57, 795–807, 1992.

    Article  Google Scholar 

  16. K. Eshghi and R. Kowalski. Abduction compared with negation by failure. In Proceedings of the 6th ICLP, pp. 234–254, Lisbon, 1989.

    Google Scholar 

  17. L. Farinas del Cerro. MOLOG: a system that extends Prolog with modal logic. New Generation Computing, 4, 35–50, 1986.

    Article  Google Scholar 

  18. K. Fine. Models for entailment, Journal of Philosophical Logic, 3, 347–372, 1974.

    Article  Google Scholar 

  19. M. Fitting. Proof methods for Modal and Intuitionistic Logic, vol 169 of Synthese library, D. Reidel, Dorderecht, 1983.

    Google Scholar 

  20. M. Fitting. First-order Logic and Automated Theorem Proving. Springer-Verlag, 1990.

    Book  Google Scholar 

  21. D. M. Gabbay. Semantical Investigations in Heyting’s Intuitionistic Logic. D. Reidel, Dordrecht, 1981.

    Google Scholar 

  22. D. M. Gabbay. N-Prolog Part 2. Journal of Logic Programming, 251–283, 1985.

    Google Scholar 

  23. D. M. Gabbay. Modal and temporal logic programming. In Temporal Logics and their Applications, A. Galton, ed. pp. 197–237. Academic Press, 1987.

    Google Scholar 

  24. D. M. Gabbay. Algorithmic proof with diminishing resources. In Proceedings of CSL ’90, pp. 156–173. LNCS vol 533, Springer-Verlag, 1991.

    Google Scholar 

  25. D. M. Gabbay. Elements of algorithmic proof. In Handbook of Logic in Theoretical Computer Science, vol 2. S. Abramsky, D. M. Gabbay and T. S. E. Maibaum, eds., pp. 307–408, Oxford University Press, 1992.

    Google Scholar 

  26. D. M. Gabbay, Labelled Deductive Systems (vol I), Oxford Logic Guides, Oxford University Press, 1996.

    Google Scholar 

  27. D. M. Gabbay. Elementary Logic, Prentice Hall, 1998.

    Google Scholar 

  28. D. M. Gabbay and F. Kriwaczek. A family of goaldirected theorem-provers based on conjunction and implication. Journal of Automated Reasoning, 7, 511–536, 1991.

    Article  Google Scholar 

  29. D. M. Gabbay and N. Olivetti. Algorithmic proof methods and cut elimination for implicational logics — part I, modal implication. Studia Logica, 61, 237–280, 1998.

    Article  Google Scholar 

  30. D. Gabbay and N. Olivetti. Goal-directed proof-procedures for intermediate logics. In Proc. of LD ’98 First International Workshop on Labelled Deduction, Freiburg, 1998.

    Google Scholar 

  31. D. M. Gabbay, N. Olivetti and S. Vorobyov. Goal-directed proof method is optimal for intuitionistic propositional logic. Manuscript, 1999.

    Google Scholar 

  32. D.M. Gabbay and N. Olivetti. Goal-directed proof theory, Kluwer Academic Publishers, Applied Logic Series, Dordrecht, 2000.

    Google Scholar 

  33. D. M. Gabbay and U. Reyle. N-Prolog: an Extension of Prolog with hypothetical implications, I. Journal of Logic Programming, 4, 319–355, 1984.

    Article  Google Scholar 

  34. D. M. Gabbay and U. Reyle. Computation with run time Skolemisation (N-Prolog, Part 3). Journal of Applied Non Classical Logics, 3, 93–128, 1993.

    Article  Google Scholar 

  35. J. H. Gallier. Logic for Computer Science, John Wiley, New York, 1987.

    Google Scholar 

  36. D. Galmiche and D. Pym. Proof-Search in type-theoretic languages. To appear in Theoretical Computer Science, 1999.

    Google Scholar 

  37. L. Giordano, A. Martelli and G. F. Rossi. Extending Horn clause logic with implication goals. Theoretical Computer Science, 95, 43–74, 1992.

    Article  Google Scholar 

  38. L. Giordano and A. Martelli. Structuring logic programs: a modal approach. Journal of Logic Programming, 21, 59–94, 1994.

    Article  Google Scholar 

  39. J. Y. Girard. Linear logic. Theoretical Computer Science 50, 1–101, 1987.

    Article  Google Scholar 

  40. R. Goré. Tableaux methods for modal and temporal logics. In Handbook of Tableau Methods, M. D’Agostino et al., eds. Kluwer Academic Publishers, 1999.

    Google Scholar 

  41. R. Hähnle and P. H. Schmitt. The liberalized δ-rule in free-variables semantic tableaux. Journal Automated Reasoning, 13, 211–221, 1994.

    Google Scholar 

  42. J. Harland and D. Pym. The uniform proof-theoretic foundation of linear logic programming. In Proceedings of the 1991 International Logic Programming Symposium, San Diego, pp. 304–318, 1991.

    Google Scholar 

  43. J. Harland. On Goal-Directed Provability in Classical Logic, Computer Languages, pp. 23:2–4:161–178, 1997.

    Article  Google Scholar 

  44. J. Harland and D. Pym. Resource-distribution by Boolean constraints. In Proceedings of CADE 1997, pp. 222–236, Springer Verlag, 1997.

    Google Scholar 

  45. A. Heudering, M. Seyfried and H. Zimmerman. Efficient loopcheck for backward proof search in some non-classical propositional logics. In (P. Miglioli et al. eds.) Tableaux 96, pp. 210–225. LNCS 1071, Springer Verlag, 1996.

    Google Scholar 

  46. J. Hodas. Logic programming in intuitionistic linear logic: theory, design, and implementation. PhD Thesis, University of Pennsylvania, Department of Computer and Information Sciences, 1993.

    Google Scholar 

  47. J. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110, 327–365, 1994.

    Article  Google Scholar 

  48. J. Hudelmaier. Decision procedure for propositionaln-prolog. In (P. Schroeder-Heister ed.) Extensions of Logic Programming, pp. 245–251, Springer Verlag, 1990.

    Google Scholar 

  49. J. Hudelmaier. An On log n-space decision procedure for intuitionistic propositional logic. Journal of Logic and Computation, 3, 63–75, 1993.

    Article  Google Scholar 

  50. J. Lambek. The mathematics of sentence structure, American Mathematics Monthly, 65, 154–169, 1958.

    Article  Google Scholar 

  51. C. I. Lewis. Implication and the algebra of logic. Mind, 21, 522–531, 1912.

    Article  Google Scholar 

  52. C. I. Lewis and C. H. Langford. Symbolic Logic, The Century Co., New York, London, 1932. Second edition, Dover, New York, 1959.

    Google Scholar 

  53. P. Lincoln, P. Scedrov and N. Shankar. Linearizing intuitionistic implication. In Proceedings of LICS ’91, G. Kahn ed., pp. 51–62, IEEE, 1991.

    Google Scholar 

  54. J. W. Lloyd, Foundations of Logic Programming, Springer, Berlin, 1984.

    Book  Google Scholar 

  55. D. W. Loveland. Near-Horn prolog and beyond. Journal of Automated Reasoning, 7, 1–26, 1991.

    Article  Google Scholar 

  56. D. W. Loveland. A comparison of three Prolog extensions. Journal of Logic Programming, 12, 25–50, 1992.

    Article  Google Scholar 

  57. A. Masini. 2-Sequent calculus: a proof theory of modality. Annals of Pure and Applied Logics, 59, 115–149, 1992.

    Google Scholar 

  58. F. Massacci. Strongly analytic tableau for normal modal logics. In Proceedings of CADE ’94, LNAI 814, pp. 723–737, Springer-Verlag, 1994.

    Google Scholar 

  59. L. T. McCarty. Clausal intuitionistic logic. I. Fixed-point semantics. Journal of Logic Programming, 5, 1–31, 1988.

    Article  Google Scholar 

  60. L. T. McCarty. Clausal intuitionistic logic. II. Tableau proof procedures. Journal of Logic Programming, 5, 93–132, 1988.

    Article  Google Scholar 

  61. M. A. McRobbie and N. D. Belnap. Relevant analytic tableaux. Studia Logica, 38, 187–200, 1979.

    Article  Google Scholar 

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

    Article  Google Scholar 

  63. D. A. Miller. Abstract syntax and logic programming. In Logic Programming: Proceedings of the 2nd Russian Conference, pp. 322–337, LNAI 592, Springer Verlag, 1992.

    Chapter  Google Scholar 

  64. G. Nadathur. Uniform provability in classical logic. Journal of Logic and Computation, 8, 209–229,1998.

    Article  Google Scholar 

  65. P. W. O’Hearn and D. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5, 215–244, 1999.

    Article  Google Scholar 

  66. N. Olivetti. Algorithmic Proof-theory for Non-classical and Modal Logics. PhD Thesis, Dipartimento di Informatica, Universita’ di Torino, 1995.

    Google Scholar 

  67. H. Ono. Semantics for substructural logics. In P. Schroeder-Heister and K. Došen(eds.) Substructural Logics, pp. 259–291, Oxford University Press, 1993.

    Google Scholar 

  68. H. Ono. Proof-theoretic methods in non-classical logics-an introduction. In (M. Takahashi et al. eds.) Theories of Types and Proofs, pp. 267–254, Mathematical Society of Japan, 1998.

    Google Scholar 

  69. D. Prawitz. Natural Deduction. Almqvist & Wiksell, 1965.

    Google Scholar 

  70. D. J. Pym and L. A. Wallen. Investigation into proof-search in a system of first-order dependent function types. In Proc. of CADE ’90, pp. 236–250. LNCS vol 449, Springer-Verlag, 1990.

    Google Scholar 

  71. G. Restall. An introduction to substructural logics. Routledge, to appear, 1999.

    Google Scholar 

  72. A. Russo. Generalizing propositional modal logics using labelled deductive systems. In (F. Baader and K. Schulz, eds.) Frontiers of Combining Systems, pp. 57–73. Vol. 3 of Applied Logic Series, Kluwer Academic Publishers, 1996.

    Google Scholar 

  73. D. Sahlin, T. Franzén, and S. Haridi. An intuitionistic predicate logic theorem prover. Journal of Logic and Computation, 2, 619–656, 1992.

    Article  Google Scholar 

  74. P. Schroeder-Heister and K. Došen(eds.) Substructural Logics. Oxford University Press, 1993.

    Google Scholar 

  75. N. Shankar. Proof search in the intuitionistic sequent calculus. In Proc. of CADE’ll, pp. 522–536. LNAI 607, Springer Verlag, 1992.

    Google Scholar 

  76. R. Statman. Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9, 67–72, 1979.

    Article  Google Scholar 

  77. P. B. Thistlewaite, M. A. McRobbie and B. K. Meyer. Automated Theorem Proving in Non Classical Logics, Pitman, 1988.

    Google Scholar 

  78. R. Turner. Logics for Artificial Intelligence, Ellis Horwood Ltd., 1985.

    Google Scholar 

  79. A. S. Troelstra. Principles of Intuitionism. Springer-Verlag, Berlin, 1969.

    Google Scholar 

  80. A. Urquhart. The semantics of relevance logics. The Journal of Symbolic Logic, 37, 159–170, 1972.

    Article  Google Scholar 

  81. A. Urquhart. The undecidability of entailment and relevant implication. The Journal of Symbolic Logic, 49, 1059–1073, 1984.

    Article  Google Scholar 

  82. D. Van Dalen. Intuitionistic logic. In Handbook of Philosophical logic, Vol 3, D. Gabbay and F. Guenther, eds. pp. 225–239. D. Reidel, Dorderecht, 1986.

    Google Scholar 

  83. L. Viganò. Labelled Non-classical Logics. Kluwer Academic Publishers, 2000. to appear.

    Google Scholar 

  84. L. A. Wallen, Automated Deduction in Nonclassical Logics, MIT Press, 1990.

    Google Scholar 

  85. H. Wansing. Sequent Calculi for normal propositional modal logics. Journal of Logic and Computation, 4, 125–142, 1994.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. King’s College London, UK

    Dov Gabbay

  2. Università di Torino, Italy

    Nicola Olivetti

Authors
  1. Dov Gabbay
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nicola Olivetti
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. King’ College, London, UK

    D. M. Gabbay

  2. Centrum für Informations- und Sprachverarbeitung, Ludwig-Maximilians-Universität, München, Germany

    F. Guenthner

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer Science+Business Media Dordrecht

About this chapter

Cite this chapter

Gabbay, D., Olivetti, N. (2002). Goal-Oriented Deductions. In: Gabbay, D.M., Guenthner, F. (eds) Handbook of Philosophical Logic. Handbook of Philosophical Logic, vol 9. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0464-9_4

Download citation

  • DOI: https://doi.org/10.1007/978-94-017-0464-9_4

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-90-481-6055-6

  • Online ISBN: 978-94-017-0464-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation