SpringerLink
Log in

Spectra: An Expressive STRIPS-Inspired AI Planner Based on Automated Reasoning

(System Description)

  • Systems Description
  • Published:
KI - Künstliche Intelligenz Aims and scope Submit manuscript

Abstract

Research in automated planning traditionally focuses on model-based approaches that often sacrifice expressivity for computational efficiency. For artificial agents that operate in complex environments, however, frequently the agent needs to reason about the beliefs of other agents and be capable of handling uncertainty. We present Spectra, a STRIPS-inspired AI planner built atop automated reasoning. Our system is expressive, in that we allow for state spaces to be defined as arbitrary formulae. Spectra is also designed to be logic-agnostic, as long as an automated reasoner exists that can perform entailment and question-answering over it. Spectra can handle environments of unbounded uncertainty; and with certain non-classical logics, our system can create plans under epistemic beliefs. We highlight all of these features using the cognitive calculus \(\mathcal {DCC}\). Lastly, we discuss that under this framework, in order to fully plan under uncertainty, a defeasible (= non-monotonic) logic can be used in conjunction with our planner.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Algorithm 1
Fig. 1
Fig. 2

Similar content being viewed by others

Notes

  1. As a reminder, extensional logics are marked by the fact that semantic values of “inner” parts of formulae compositionally determine such values for these formulae. Hence if it’s false that a is a block, \(\lnot Block (a)\), then standard compositionality in first-order logic dictates that \(Block (a) \rightarrow Block (b)\) is true. In contrast, despite the fact that \(\lnot Block (a)\), it could be that Jones believes the opposite, i.e. \(\textbf{B}(j, Block (a))\). Efficient coverage of the fundamental distinction between extensional versus intensional logics is given in [14].

  2. A traditional “engine” of demands for such intensional expressivity from computational logics has been increasingly demanding versions of the false-belief task see e.g. [6]; and for apparently the first formalization and simulation of the task see [1].

  3. Code is available at https://github.com/rairlab/spectra.

  4. For every substantive cognitive verb in the human case (e.g., intends desires, says/communicates, perceives, the epistemic verbs (the class most relevant to the present paper), attends to, etc.), the approach of which this particular calculus is an example ultimately calls for a corresponding modal operator to be present.

  5. Readers unfamiliar with GOLOG can start with [27]. A number of interesting questions arise from comparison of PLATAS with our approach, for future analysis and engineering. We mention two very briefly: (1) As mentioned in [10], and discussed at some length lucidly in the complementary [41], in this line of work it is often desirable to consider restrictions in underlying declarative expressivity (e.g. to the PDDL fragment ADL). In contrast, we find such restrictions to be in considerable tension with human-level cognition, in planning. (2) An inferential backbone of resolution (GOLOG is written in Prolog) is in many ways incontestably advantageous, but we are guided by the fact that first-rate human deductive reasoning is almost invariably carried out in natural deduction, first invented for the extensional case in 1935 [16, 25].

  6. We have already indicated that such logics are known also as non-monotonic logics. As a reminder given for fuller context, deduction is monotonic; i.e., if \(\Phi \vdash \phi\) (which is to say that \(\phi\) can be proved deductively from \(\Phi\)), then for any formula \(\psi\), \(\Phi \cup \{\psi \} \vdash \phi\) holds. In stark contrast, non-monotonic logics, long created and implemented in AI (e.g. originally by Reiter and McCarthy [29, 40], with more expressive such logics more recently presented in [9, 37]) are such that new declarative information can invalidate what was earlier a valid inference. It may e.g. be rational to infer from Mr. Smith’s telling you that it’s raining that you should believe that it is, and you thus may believe it is; but if you then find out that Smith is a pathological liar under treatment for his condition, you will now ceteris paribus not believe that it’s raining.

  7. It was Simon, with Newell, who introduced to the world in 1956 the very first automated prover: LogicTheorist.

References

  1. Arkoudas K, Bringsjord S (2009) Propositional attitudes and causation. Int J Softw Inform 3(1):47–65

    Google Scholar 

  2. Bäckström C, Nebel B (1993) Complexity results for SAS+ planning. In: Bajcsy R (ed) Proceedings of the 13th international joint conference on artificial intelligence. Chambéry, France, August 28–September 3, 1993, Morgan Kaufmann. pp 1430–1435

  3. Bonet B, Geffner H (2000) Planning with incomplete information as heuristic search in belief space. In: Proceedings of the fifth international conference on artificial intelligence planning systems, pp 52–61

  4. Bonet B, Geffner H (2001) Planning as heuristic search. Artif Intell 129(1–2):5–33. https://doi.org/10.1016/S0004-3702(01)00108-4

    Article  MathSciNet  Google Scholar 

  5. Bonet B, Geffner H (2024) Flexible and scalable partially observable planning with linear translations. In: Brodley CE, Stone P (eds) Proceedings of the twenty-eighth AAAI conference on artificial intelligence, July 27–31, 2014, Québec City, Québec, Canada. AAAI Press, pp 2235–2241. https://doi.org/10.1609/AAAI.V28I1.9047

  6. Braüner T (2014) Hybrid-logical reasoning in the smarties and Sally-Anne tasks. J Logic Lang Inf 23:415–439

    Article  MathSciNet  Google Scholar 

  7. Bringjsord S, Govindarajulu NS (2023) Deontic cognitive event calculus (formal specification). https://www.cs.rpi.edu/~govinn/dcec.pdf

  8. Bringsjord S, Giancola M, Govindarajulu NS, Slowik J, Oswald J, Bello P, Clark M (2024) Argument-based inductive logics, with coverage of compromised perception. Front Artif Intell. https://doi.org/10.3389/frai.2023.1144569

    Article  Google Scholar 

  9. Bringsjord S, Govindarajulu N, Giancola M (2021) Automated argument adjudication to solve ethical problems in multi-agent environments. Paladyn J Behav Robot 12:310–335

    Article  Google Scholar 

  10. Claßen J, Röger G, Lakemeyer G, Nebel B (2012) PLATAS—integrating planning and the action language GOLOG. Künstliche Intell 26(1):61–67. https://doi.org/10.1007/S13218-011-0155-2

    Article  Google Scholar 

  11. Eppe M, Dylla F (2012) An epistemic planning system based on the event calculus. Tech. rep., Technical Report 033-11/2012. University of Bremen, Bremen

  12. Fikes RE, Nilsson NJ (1971) STRIPS: a new approach to the application of theorem proving to problem solving. Artif Intell 2(3–4):189–208. https://doi.org/10.1016/0004-3702(71)90010-5

    Article  Google Scholar 

  13. Finzi A, Pirri F, Reiter R et al (2000) Open world planning in the situation calculus. In: AAAI/IAAI, pp 754–760

  14. Fitting M (2015) Intensional Logic. In: Zalta E (ed) The Stanford encyclopedia of philosophy. https://plato.stanford.edu/entries/logic-intensional

  15. Geffner H (2000) Functional strips: a more flexible language for planning and problem solving. In: Minker J (ed) Logic-based artificial intelligence. The Springer international series in engineering and computer science, vol 597. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-1567-8_9

  16. Gentzen G (1935) Investigations into logical deduction. In: Szabo ME (ed) The collected papers of Gerhard Gentzen. North-Holland, Amsterdam, pp 68–131 (This is an English version of the well-known 1935 German version)

    Google Scholar 

  17. Giancola M (2023) Reasoning with cognitive likelihood for artificially-intelligent agents: formalization and implementation. Ph.D. thesis, Rensselaer Polytechnic Institute

  18. Govindarajulu N, Bringsjord S (2017) On automating the doctrine of double effect. In: Sierra C (ed) Proceedings of the twenty-sixth international joint conference on artificial intelligence (IJCAI-17). International joint conferences on artificial intelligence. pp 4722–4730. https://doi.org/10.24963/ijcai.2017/658

  19. Govindarajulu N, Bringsjord S, Peveler M (2019) On quantified modal theorem proving for modeling ethics. In: Suda M, Winkler S (eds) Proceedings of the second international workshop on automated reasoning: challenges, applications, directions, exemplary achievements (ARCADE 2019). Electronic proceedings in theoretical computer science, vol 311. Open Publishing Association, Waterloo, Australia, pp 43–49. http://eptcs.web.cse.unsw.edu.au/paper.cgi?ARCADE2019.7.pdf. The ShadowProver system can be obtained here: https://naveensundarg.github.io/prover/

  20. Green C (1981) Application of theorem proving to problem solving. Readings in artificial intelligence. Elsevier, Amsterdam, pp 202–222. https://doi.org/10.1016/B978-0-934613-03-3.50019-2

    Chapter  Google Scholar 

  21. Haslum P, Lipovetzky N, Magazzeni D, Muise C, Brachman R, Rossi F, Stone P (2019) An introduction to the planning domain definition language, vol 13. Springer, Cham. https://doi.org/10.1007/978-3-031-01584-7

    Book  Google Scholar 

  22. Haslum P et al (2011) Computing genome edit distances using domain-independent planning. In: Proc. SPARK workshop, pp 45–51

  23. Helmert M (2006) The fast downward planning system. J Artif Intell Res 26:191–246. https://doi.org/10.1613/jair.1705

    Article  Google Scholar 

  24. Helmert M, Domshlak C (2009) Landmarks, critical paths and abstractions: What’s the difference anyway? In: Gerevini A, Howe AE, Cesta A, Refanidis I (eds) Proceedings of the 19th international conference on automated planning and scheduling, ICAPS 2009, Thessaloniki, Greece, September 19–23, 2009. AAAI. http://aaai.org/ocs/index.php/ICAPS/ICAPS09/paper/view/735

  25. Jáśkowski S (1934) On the rules of suppositions in formal logic. Stud Log 1(1):5–32

    Google Scholar 

  26. Katz M, Domshlak C (2008) Optimal additive composition of abstraction-based admissible heuristics. In: Rintanen J, Nebel B, Beck JC, Hansen EA (eds) Proceedings of the eighteenth international conference on automated planning and scheduling, ICAPS 2008, Sydney, Australia, September 14–18, 2008, pp. 174–181. AAAI. http://www.aaai.org/Library/ICAPS/2008/icaps08-022.php

  27. Levesque H, Reiter R, Lespérance Y, Lin F, Scherl R (1997) GOLOG: a logic programming language for dynamic domains. J Log Program 31:59–83

    Article  MathSciNet  Google Scholar 

  28. Matloob R, Soutchanski M (2016) Exploring organic synthesis with state-of-the-art planning techniques. In: Proc. SPARK workshop, pp 52–61

  29. McCarthy J (1980) Circumscription—a form of non-monotonic reasoning. Artif Intell 13:27–39

    Article  MathSciNet  Google Scholar 

  30. Mueller ET (2009) Automating commonsense reasoning using the event calculus. Commun ACM 52(1):113–117. https://doi.org/10.1145/1435417.1435443

    Article  Google Scholar 

  31. Mueller ET, Sutcliffe G (2005) Reasoning in the event calculus using first-order automated theorem proving. In: FLAIRS conference, pp 840–841

  32. Muise C, Belle V, Felli P, McIlraith S, Miller T, Pearce A, Sonenberg L (2015) Planning over multi-agent epistemic states: a classical planning approach. In: Proceedings of the AAAI conference on artificial intelligence, vol 29

  33. Palacios H, Geffner H (2006) Compiling uncertainty away: solving conformant planning problems using a classical planner (sometimes). In: Proceedings, the twenty-first national conference on artificial intelligence and the eighteenth innovative applications of artificial intelligence conference, July 16–20, 2006, Boston, Massachusetts, USA. AAAI Press, pp 900–905. http://www.aaai.org/Library/AAAI/2006/aaai06-142.php

  34. Palacios H, Geffner H (2009) Compiling uncertainty away in conformant planning problems with bounded width. J Artif Intell Res 35:623–675. https://doi.org/10.1613/JAIR.2708

    Article  MathSciNet  Google Scholar 

  35. Pednault EPD (1989) ADL: exploring the middle ground between STRIPS and the situation calculus. In: Brachman RJ, Levesque HJ, Reiter R (eds) Proceedings of the 1st international conference on principles of knowledge representation and reasoning (KR’89). Toronto, Canada, May 15–18 1989. Morgan Kaufmann, pp 324–332

  36. Petrick, RP, Bacchus F (2002) A knowledge-based approach to planning with incomplete information and sensing. In: AIPS, vol 2, pp 212–222

  37. Pollock J (2001) Defasible reasoning with variable degrees of justification. Artif Intell 133:233–282

    Article  Google Scholar 

  38. Pommerening F, Helmert M, Röger G, Seipp J (2015) From non-negative to general operator cost partitioning. In: Bonet B, Koenig S (eds) Proceedings of the twenty-ninth AAAI conference on artificial intelligence, January 25–30, 2015, Austin, Texas, USA. AAAI Press, pp 3335–3341. https://doi.org/10.1609/AAAI.V29I1.9668

  39. Poole D (1996) A framework for decision-theoretic planning I: combining the situation calculus, conditional plans, probability and utility, pp 436–445

  40. Reiter R (1980) A logic for default reasoning. Artif Intell 13:81–132

    Article  MathSciNet  Google Scholar 

  41. Röger G, Helmert M, Nebel B (2008) On the relative ex- pressiveness of ADL and GOLOG: the last piece in the puzzle. In: Brewka G, Lang J (eds) Principles of knowledge representation and reasoning: proceedings of the eleventh international conference, KR 2008, Sydney, Australia, September 16–19, 2008. AAAI Press, pp 544–550. http://www.aaai.org/Library/KR/2008/kr08-053.php

  42. Schiffel S, Thielscher M (2006) Reconciling situation calculus and fluent calculus. In: AAAI, vol 6. pp 287–292

  43. Shanahan M (2000) An abductive event calculus planner. J Log Program 44(1–3):207–240. https://doi.org/10.1016/S0743-1066(99)00077-1

    Article  MathSciNet  Google Scholar 

  44. Simon HA (1956) Rational choice and the structure of the environment. Psychol Rev 63(2):129–138. https://doi.org/10.1037/h0042769

    Article  Google Scholar 

  45. Soutchanski M, Young R (2023) Planning as theorem proving with heuristics. ar**v preprint. https://doi.org/10.48550/ar**v.2303.13638

  46. Tran SC, Pontelli E, Balduccini M, Schaub T (2023) Answer set planning: a survey. Theory Pract Log Program 23(1):226–298. https://doi.org/10.1017/S1471068422000072

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgements

The authors would like to thank Naveen Sundar Govindarajulu for develo** the initial version of Spectra that used the first-order reasoner Snark (as well as, for some applications, ShadowProver; this was enabled in no small part by AFOSR and ONR, support to Bringsjord and Govindarajulu for which we are most grateful). This paper was supported in part by a fellowship award to Rozek under contract FA9550-21-F-0003 through the National Defense Science and Engineering Graduate (NDSEG) Fellowship Program, sponsored by the United States of America’s Air Force Research Laboratory (AFRL), the Office of Naval Research (ONR), and the Army Research Office (ARO). Additionally, the authors are greatly indebted to ONR and AFOSR for the initial development of Spectra, for the continued support of the automated reasoner ShadowProver, and to both organizations for longstanding support of r &d in automated reasoning, planning, and logic-based learning. Finally, perspicacious feedback from three anonymous reviewers, and from the editors, was extremely helpful, and we give our thanks to them.

Author information

Authors and Affiliations

  1. Rensselaer Polytechnic Institute (RPI), Troy, USA

    Brandon Rozek & Selmer Bringsjord

Authors
  1. Brandon Rozek
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Selmer Bringsjord
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Brandon Rozek.

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Rozek, B., Bringsjord, S. Spectra: An Expressive STRIPS-Inspired AI Planner Based on Automated Reasoning. Künstl Intell (2024). https://doi.org/10.1007/s13218-024-00847-8

Download citation

  • Received:

  • Accepted:

  • Published:

  • DOI: https://doi.org/10.1007/s13218-024-00847-8

Search

Navigation