Situational calculus, linear connection proofs and STRIPS-like planning: an experimental comparison. (English) Zbl 1412.68223
Migliolo, P. (ed.) et al., Theorem proving with analytic tableaux and related methods. 5th international workshop, TABLEAUX ’96, Terrasini, Palermo, Italy, May 15–17, 1996. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 1071, 193-209 (1996).
Summary: The paper presents implementations of two logical approaches to plan generation – Linear Connection Proofs and Situational Calculus – and analyses the reasons for their different computational performance. Both implementations are then compared with the planning system ucpop on a set of benchmarks. The interesting outcome is that the logical approaches compete rather well with ucpop and, in particular, with the exploitation of modern theorem proving technology as symbolic constraints, the performance of Situational Calculus is no longer completely disastrous.
For the entire collection see [Zbl 0939.00023].
For the entire collection see [Zbl 0939.00023].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68T27 | Logic in artificial intelligence |
References:
| [1] | A. Barrett and D. Weld. Partial-order planning: Evaluating possible efficiency gains. \(Artificial Intelligence\), 67(1):71-112, 1994. · Zbl 0807.68080 |
| [2] | W. Bibel. \(Automated Theorem Proving\). Vieweg, 1982. · Zbl 0492.68067 |
| [3] | W. Bibel. A Deductive Solution for Plan Generation. \(New Generation Computing\), 6:115-132, 1986. · Zbl 0624.68079 |
| [4] | W. Bibel, L. Fariñas del Cerro, B. Fronhöfer, and A. Herzig. Plan Generation by Linear Proofs: On Semantics. In D. Metzing, editor, \(GWAI'89, 13\)\^{}{th}\(German Workshop on Artificial Intelligence\), volume 216 of \(Informatik-Fachberichte\), pages 49-62, Schloß Eringerfeld, Geseke, Germany, September 1989. Springer, Berlin. |
| [5] | T. Bollinger. A Model Elimination Calculus for Generalized Clauses. In R. Reiter J. Mylopoulos, editor, \(IJCAI-91\), pages 126-131, August 1991. · Zbl 0745.68087 |
| [6] | B. Fronhöfer. Linearity and Plan Generation. \(New Gen. Computing\), 5:213-225, 1987. · Zbl 0654.68100 |
| [7] | B. Fronhöfer. Default Connections a Modal Planning Framework. In J. Hertzberg, editor, \(European Workshop on Planning (EWSP-91)\), pages 39-52, Bonn, March 18-19 1991. St.Augustin, Germany, LNAI 522, Springer. |
| [8] | B. Fronhöfer. Linear Proofs and Linear Logic. In D. Pearce and G. Wagner, editors, \(Logics in AI\), pages 106-125, Berlin, September 7-10 1992. JELIA’92, LNCS 633. · Zbl 0915.03030 |
| [9] | B. Fronhöfer. The action-as-implication paradigm: Formal systems and application. Habilitationsschrift, TU München, 1995. |
| [10] | Ch. Goller, R. Letz, K. Mayr, and J. Schumann. Setheo V3.2: Recent Developments. In Alan Bundy, editor, \(CADE'94\), pages 778-782, 1994. |
| [11] | C. Green. Application of Theorem Proving to Problem Solving. In \(IJCAI-1\), pages 219-239, 1967. |
| [12] | G. Große, S. Hölldobler, and J. Schneeberger. Linear Deductive Planning. Technical report, Intellektik, Informatik, TH Darmstadt, 1992. · Zbl 0854.68091 |
| [13] | G. Große, S. Hölldobler, J. Schneeberger, U. Sigmund, and M. Thielscher. Equational Logic Programming, Actions, and Change. In \(Proc. Joint International Conference and Symposium on Logic Programming JICSLP'92\), 1992. |
| [14] | S. Hölldobler and M. Thielscher. On logic, change, and specificity. Intellektik, Informatik, TH Darmstadt, 1992. |
| [15] | E. Jacopin. Classical AI Planning as Theorem Proving: The Case of a Fragment of Linear Logic. In \(AAAI Fall Syposium on ``Automated Deduction in Non Classical Logics”\), pages 62-66, Palo Alto, 1993. AAAI Press. |
| [16] | E. Jacopin. Construire des plans en utilisant le calcul des séquents pour un fragment de la logique linéaire. Tech. report, Laforia-IBP, Univ. P. et M. Curie, Paris, 1993. |
| [17] | R. Kowalski. \(Logic for Problem Solving\). North Holland, New York, 1979. · Zbl 0426.68002 |
| [18] | R. Letz, S. Bayerl, J. Schumann, and B. Fronhöfer. The Logic Programming Language LOP. Technical report, Technische Universität München, 1989. |
| [19] | R. Letz, K. Mayr, and C. Goller. Controlled Integration of the Cut Rule into Connection Tableau Calculi. \(JAR\), 13:297-337, 1994. · Zbl 0816.03005 |
| [20] | R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performance Theorem Prover. \(JAR\), 8(2):183-212, 1992. · Zbl 0759.68080 |
| [21] | V. Lifshitz. On the Semantics of STRIPS. In M.P. Georgeff and A.L. Lansky, editors, \(Workshop on Reasoning about Actions and Plans\), pages 1-8. Morgan Kaufmann, 1986. |
| [22] | M. Masseron, C. Tollu, and J. Vauzeilles. Generating Plans in Linear Logic. Technical Report 90-11, Université Paris Nord, Dép. de math. et informatique, December 1990. · Zbl 0758.03017 |
| [23] | J. McCarthy and P. Hayes. Some Philosophical Problems from the Stand-point of Artificial Intelligence. In B. Meltzer and D. Michie, editors, \(Machine Intelligence 4\), pages 463-502. Edinburgh University Press, 1969. · Zbl 0226.68044 |
| [24] | N. J. Nilsson. \(Principles of Artificial Intelligence\). Springer, 1982. · Zbl 0474.68094 |
| [25] | J.S. Penberthy and D. Weld. UCPOP: a sound, complete, partial order planner for ADL. In \(KR-92\), pages 103-114, October 1992. |
| [26] | D. Plaisted. The Search Efficiency of Theorem Proving Strategies. In Alan Bundy, editor, \(CADE'94\), pages 57-71, 1994. · Zbl 1433.68561 |
| [27] | R. Reiter. The frame problem in the situation calculus. In Vladimir Lifschitz, editor, \(Artificial Intelligence and Mathematical Theory of Computation\), pages 359-380. Academic Press, 1991. · Zbl 0755.68124 |
| [28] | J. Schneeberger and S. Hölldobler. A New Deductive Approach to Planning. \(New Generation Computing\), 8:225-244, 1990. · Zbl 0711.68026 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
