New Generation Computing

, 15:369 | Cite as

Globally linear connection method

  • Stefan Brüning
Regular Papers


To model in a formal system the remarkable ability of human agents to reason about situations, actions, and causality has always been a major research goal in Intellectics. Most of the work towards this goal is based on the situation calculus which, however, has the disadvantage that it requires either to state frame axioms or to use non-monotonic logic and a commonsense law of inertia. A deductive approach which does not show this disadvantage is the linear connection method whose key idea is to treat facts about a situation as resources which can be consumed and produced by actions. It was shown that this approach properly handles planning problems which only allow deterministic actions, i.e. actions which are not allowed to have several alternative effects. In this paper we extend and revise the linear connection method to overcome this restriction.


Automated Reasoning Theorem Proving Deductive Planning Linear Connection Method 


  1. 1).
    Allen, J., Hendler, J., and Tate, A.,Readings in Planning, Morgan Kaufmann, San Mateo, 1990.Google Scholar
  2. 2).
    Baker, A. B., “A Simple Solution to the Yale Shooting Problem,” inProceedings of the International Conference on the Principles of Knowledge Representation and Reasoning, pp. 11–20, 1989.Google Scholar
  3. 3).
    Bibel, W., “A Deductive Solution for Plan Generation,”New Generation Computing, 4, pp. 115–132, 1986.MATHGoogle Scholar
  4. 4).
    Bibel, W.,Automated Theorem Proving, second edition, Vieweg Verlag, 1987.Google Scholar
  5. 5).
    Brewka, G. and Hertzberg, J., “How to Do Things with Worlds — On Formalizing Actions and Plans,”Logic and Computation, 3, 5, pp. 517–532, 1993.MATHCrossRefMathSciNetGoogle Scholar
  6. 6).
    Brüning, S., Grosse, G., Hölldobler, S., Schneeberger, J., Sigmund, U., and Thielscher, M., “On Disjunction in Linear Logic Programming” (extended abstract), inProceedings of the Workshop on Linear Logic and Logic Programming (D. Miller, ed.),MS-CIS-92-80, University of Pennsylvania, School of Engineering and Applied Science, Computer and Information Science Department, pp. 53–59, 1992.Google Scholar
  7. 7).
    Brüning, S., Grosse, G., Hölldobler, S., Schneeberger, J., Sigmund, U., and Thielscher, M., “Disjunction in Plan Generation by Equational Logic Programming,” inBeiträge zum 7. Workshop Planen und Konfigurieren (A. Horz, ed.),Arbeitspapiere der GMD 723, pp. 18–26, January 1993.Google Scholar
  8. 8).
    Brüning, S., “Techniques for Avoiding Redundancy in Theorem Proving Based on the Connection Method,”Ph. D. thesis, TH Darmstadt, 1994.Google Scholar
  9. 9).
    Brüning, S., “Towards Efficient Calculi for Resource-Oriented Linear Deductive Planning,” inProceedings of the International Conference on Logic Programming and Automated Reasoning (F. Pfenning, ed.),volume 822 of Lecture Notes in Artificial Intelligence, Springer-Verlag, pp. 174–188, 1994.Google Scholar
  10. 10).
    Fikes, R. E. and Nilsson, N. J., “STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving,”Artificial Intelligence, 5, 2, pp. 189–208, 1971.CrossRefGoogle Scholar
  11. 11).
    Fronhöfer B. and Caferra, R., “Memorization of Literals: An Enhancement of the Connection Method,”Technical Report, Institut für Informatik, Technische Universität München, 1988.Google Scholar
  12. 12).
    Fronhöfer, B., “Linearity and Plan Generation,”New Generation Computing, 5, pp. 213–225, 1987.MATHCrossRefGoogle Scholar
  13. 13).
    Grosse, G., Hölldobler, S., and Schneeberger, J., “On Linear Deductive Planning,”Technical Report, AIDA-92-08, FG Intellektik, FB Informatik, TH Darmstadt, 1992. Accepted for publication in theJournal of Logic and Computation.Google Scholar
  14. 14).
    Grosse, G., Hölldobler, S., Schneeberger, J., Sigmund, U., and Thielscher, M., “Equational Logic Programming, Actions, and Change,” inProc. Joint International Conference and Symposium on Logic Programming JICSLP’92, 1992.Google Scholar
  15. 15).
    Hanks, S. and McDermott, D., “Default Reasoning, Nonmonotonic Logics, and the Frame Problem,” inNational Conference on Artificial Intelligence, pp. 328–333, 1986.Google Scholar
  16. 16).
    Hayes, P. J., “The Frame Problem and Related Problems in Artificial Intelligence,” inArtificial and Human Thinking (A. Eilithron and D. Jones, eds.), Jossey-Bass Publishers, 1983. Also published inReadings in Planning (J. Allen et al.), Morgan Kaufmann, San Moteo, 1990.Google Scholar
  17. 17).
    Hertzberg, J.,Planen: Einführung in die Planerstellungsmethoden der künstlichen Intelligenz, volume 65 of Reihe Informatik, BI-Wissenschaftsverlag, 1989.Google Scholar
  18. 18).
    Hölldobler, S. and Schneeberger, J., “A New Deductive Approach to Planning,”New Generation Computing, 8, pp. 225–244, 1990. A short version appeared in theProceedings of the German Workshop on Artificial Intelligence, Informatik Fachberichte 216, pp. 63–73, 1989.MATHGoogle Scholar
  19. 19).
    Hölldobler, S. and Thielscher, M., “Computing Change and Specificity with Equational Logic Programs,”Annals of Mathematics and Artificial Intelligence, special issue on Processing of Declarative Knowledge, 1994. To appear.Google Scholar
  20. 20).
    Letz, R., Schumann, J., Bayerl, S., and Bibel, W., “SETHEO — A High-Performance Theorem Prover for First-Order Logic,”Journal of Automated Reasoning, 8, pp. 183–212, 1992.MATHCrossRefMathSciNetGoogle Scholar
  21. 21).
    Letz, R., Mayr, K., and Goller, Ch., “Controlled Integrations of the Cut Rule into Connection Tableau Calculi,”Journal of Automated Reasoning, 13, 3, pp. 297–338, 1994, Special Issue on Automated Reasoning with Analytic Tableaux.MATHCrossRefMathSciNetGoogle Scholar
  22. 22).
    Letz, R., “First-Order Calculi and Proof Procedures for Automated Deduction,”Ph. D. thesis, TH Darmstadt, 1993.Google Scholar
  23. 23).
    Lifschitz, V., “On the Semantics of STRIPS,” inProc. of the Workshop on Reasoning about Actions and Plans (M. P. Georgeff and A. L. Lansky, eds.), Los Altos, Morgan Kaufmann, pp. 1–8, 1986.Google Scholar
  24. 24).
    Lifschitz, V., “Formal Theories of Action” (preliminary report), inInternational Joint Conference on Artificial Intelligence, Morgan Kaufmann Publishers, Inc., pp. 966–972, August 1987.Google Scholar
  25. 25).
    Loveland, D. W., “Mechanical Theorem Proving by Model Elimination,”Journal of the ACM, 15, pp. 236–251, 1986.CrossRefGoogle Scholar
  26. 26).
    Masseron, M., Tollu, C., and Vauzeilles, J., “Generating Plans in Linear Logic,”Pré-publication, 90–11, Centre Scientifique et Polytechnique, Universite Paris Nord, December 1990.Google Scholar
  27. 27).
    Masseron, M., Tollu, C., and Vauzielles, J., “Generating Plans in Linear Logic,” inFoundations of Software Technology and Theoretical Computer Science, LNCS, 472, Springer-Verlag, pp. 63–75, 1990.Google Scholar
  28. 28).
    McCarthy, J. and Hayes, P., “Some Philosophical Problems from the Standpoint of Artificial Intelligence,” inMachine Intelligence, vol. 4 (B. Meltzer and D. Michie, eds.), Edinburgh University Press, Edinburgh, pp. 463–502, 1969. Also published inReadings in Planning (J. Allen et al.), Morgan Kaufmann, San Mateo, 1990.Google Scholar
  29. 29).
    McCarthy, J., “Situations and Actions and Causal Laws,”Stanford Artificial Intelligence Project: Memo 2, 1963.Google Scholar
  30. 30).
    McCarthy, J., “Applications of Circumscription to Formalize Commonsense Knowledge,”Artificial Intelligence, 28, pp. 89–116, 1986.CrossRefMathSciNetGoogle Scholar
  31. 31).
    Schneeberger, J., “Plan Generation by Linear Deduction,”Ph. D. thesis, FG Intellektik, TH Darmstadt, 1992.Google Scholar
  32. 32).
    Siekmann, J. H., “An Introduction to Unification Theory,” inFormal Techniques in Artificial Intelligence, A Sourcebook (R. B. Banerji, ed.), Elsevier Science Publishers B. V., North-Holland, 1990.Google Scholar
  33. 33).
    Stickel, M. E., “A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler,”Journal of Automated Reasoning, 4, pp. 353–380, 1988.MATHCrossRefMathSciNetGoogle Scholar
  34. 34).
    Stickel, M. E., “A Prolog Technology Theorem Prover,” in10th International Conference on Automated Deduction (M. E. Stickel, ed.), Berlin, pp. 673–674, 1990.Lecture Notes in Artificial Intelligence, 449, Springer-Verlag.Google Scholar
  35. 35).
    Sussman, G. J.,A Computer Model of Skill Acquisition, Elsevier Publishing Company, 1975.Google Scholar
  36. 36).
    Thielscher, M.,Automatisierte Schliessen über Kausalbeziehungen mit SLDENF-Resolution, DISKI, Infix-Verlag, 1995. To appear.Google Scholar
  37. 37).
    Winslett, M., “Resoning about Action Using a Possible Models approach,” inProceedings of the AAAI National Conference on Artificial Intelligence, pp. 89–93, 1988.Google Scholar

Copyright information

© Ohmsha, Ltd. and Springer 1997

Authors and Affiliations

  • Stefan Brüning
    • 1
  1. 1.FG Intellektik, FB InformatikTechnische Hochschule DarmstadtDarmstadtGermany

Personalised recommendations