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

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.

1 Introduction

Agents who interact with the physical world often encounter uncertainty in the environment. One strategy to deal with uncertainty is to capture it in declarative form. For example, consider a situation where in the coming days the weather will either be rain (R), snow (S), or sunny ($S^*$). One goal that a rational agent might have is to ensure it stays dry while outside (D). We can represent the initial state space ($\Gamma _0$), with its uncertainty w.r.t. weather conditions, as the formula $R \vee S \vee S^*$. The agent can then attempt to find a plan or sequence of actions that takes an agent from $\Gamma _0$ to a state space that satisfies its goal D.

Model-based automated planning has primarily focused on environments wherein complete state information is provided to the agent as a collection of facts. This is standardly enabled through the usage of the closed world assumption (CWA), which states that any fact not specified in the state description is assumed to be false. Model-based conformant planning extends this by replacing an individual state with a finite collection of states otherwise known as a belief state. Each state within the belief state is individually closed under CWA. We take this a step further in our work: we allow and handle uncertain situations that can be captured by a collection of arbitrary (potentially higher-order and modal) formulae. This allows us to not only plan over a finite set of states, but potentially over an infinite set in the quantified case. We allow for the usage of arbitrary theories, such as Peano Arithmetic, to consider problems that require complex actions to reach the goal. We achieve this by making use of automated reasoning within the planning process itself.

Automated planning through reasoning was first investigated by Green [20] in 1981. Work continued throughout the early 2000s, where the planning problem was represented using the event calculus [11, 30, 31, 43] and/or the situation calculus [13, 39, 42]. Model-based approaches, however, have gained more traction over the years due to efficient implementations such as Fast Downward [23] with strong heuristics like delete relaxation [4], lm-cut [24], cost partitioning [26], and potential heuristics [38]. Mikhail and Ryan recently developed a planner that makes use of both heuristic search and reasoning over the situation calculus [45]. We believe this direction deserves additional attention; however, we are primarily concerned with problems that require non-classical, specifically intensional,¹ reasoning. Examples of such problems arise in modeling misconceptions of beliefs between multiple agents; such modeling must for instance require sufficient expressivity to formalize the propositions that Agent 1 believes that Agent 2 believes that Agent 1 believes there is a stack of blocks that are to be unstacked, even when no such belief on the part of Agent 2 is veridical.²

In addition, we’re interested in looking beyond deductive logics and toward inductive ones to allow for careful treatment of information gathered and its likelihood [8, 9]. For example, one might wish to have an artificial agent assign a belief derived from perception a higher likelihood than a belief derived from agent communication. These are examples of issues that the relevant non-classical-logic community aims to tackle.

We introduce Spectra,³ a planner founded on automated reasoning. We designed Spectra to be logic agnostic, allowing one to plug in any logic that has an associated automated reasoner capable of determining entailment and question-answering. This allows the user to model the planning problem in a logic they’re accustomed to. We showcase Spectra with the non-classical, specifically intensional, cognitive calculi $\mathcal {DCC}$, a fragment of $\mathcal {DCEC}$ (which has been used in numerous prior papers and simulations; e.g. [18]). We provide an example of how Spectra with $\mathcal {DCC}$ can solve epistemic planning problems. Finally, we discuss how defeasible (= non-monotonic) logics can be used in our framework to create plans over a large range of uncertain scenarios.

2 Background and Related Work

Model-based automated classical planning can be captured by a propositional STRIPS model [12]. This is a tuple $\langle P, O, I, G \rangle$ where P is a finite set of ground atomic formulae, O is the finite set of operators, $I \subseteq P$ is the initial state, and G are the goals. Operators consist of preconditions $\texttt{Pre} \subseteq P$, add effects $\texttt{Add} \subseteq P$, and delete effects $\texttt{Del} \subseteq P$. Given a state $s \subseteq P$, an action is applicable iff $\texttt{Pre} \subseteq s$. After performing an action o on state s, the next state will be $(s - \texttt{Del} ) \cup \texttt{Add}$.

Alternatives to the STRIPS model include but are not limited to Functional STRIPS [15], ADL [35], and SAS$^+$ [2]. However, often the more compact representation of PDDL [21] is used. This allows declarative information to be captured through predicate logic as opposed to only propositional logic, along with other features such as conditional effects. However, due to the domain-closure assumption, this representation can be translated to an equivalent STRIPS problem with an exponential blowup of grounded operators compared to the lifted ones described with predicate logic. When using PDDL, a finite list of object labels Obj are provided. Formulae may include $\forall$ and $\exists$ statements; however, these get grounded to their propositional form. The domain-closure assumption takes all quantifiers and replaces them using the truth-functional expansion over the list of object labels Obj. That is, $\forall x~ P(x)$ is equivalent to

$$\begin{aligned} \bigwedge _{o \in Obj} P(o), \end{aligned}$$

and $\exists x~ P(x)$ is equivalent to

$$\begin{aligned} \bigvee _{o \in Obj} P(o). \end{aligned}$$

Conformant planning extends the STRIPS model by changing the initial state I to a finite set of possible initial states, often called a belief state in the literature [3]. Actions are then applicable at a given belief state b if it is applicable for all states $s \in b$. Similarly, a belief state b satisfies a goal G iff for all $s \in b$, $G \subseteq s$. In addition to CWA and domain-closure assumptions, classical model-based planning also carries the unique-name assumption and grounds all actions prior to search. This assumption states that for any two distinct object labels $o_1, o_2 \in Obj$, they do not refer to the same object; i.e., $obj(o_1) \ne obj(o_2)$. Before the search algorithm commences, a traditional classical model-based planner will ground all actions to their propositional form. Over the years, domains have been identified where the size of their grounded representations are too large to contain in device memory. [22, 28]. An alternate line of research that addresses this is lifted planning.

We use a fragment of the Deontic Cognitive Event Calculus ($\mathcal {DCEC}$) (see e.g. [7]) in order to showcase our planner solving epistemic tasks. $\mathcal {DCEC}$ is a quantified, multi-modal,,⁴ sorted cognitive-event calculus. Our fragment $\mathcal {DCC}$ disregards time and treats all timepoints as equivalent. The box labeled ‘$\mathcal {DCC}$ Signature’ shows the signature of our fragment. Cognitive operators here are only: Believes, Common-knowledge, Says, Perceives, and Knows. A sample reading of the formula

$$\begin{aligned} \textbf{B}(a, \textbf{S}(a, b, \textbf{P}(c,\phi ))) \end{aligned}$$

is “agent a believes that a says to agent b that agent c perceives $\phi$.” The formula $\forall x: \phi$ reads that $\phi$ holds for all bound variables x ranging over the domain of discourse. A subset of our inference schemata are shown in the box labeled ‘$\mathcal {DCC}$ Inference Schemata (Subset).’

Regarding related work, Soutchanski and Young [45] designed an automated planner that also performs a heuristic search guided by automated reasoning. Their work is specific to the situation calculus and instead of states, they transition over situations which are formulae in the situation calculus. The Planning Techniques and Action Languages (PLATAS) project integrates planning and the GOLOG action language by embedding the planning description language PDDL into GOLOG, which uses an extended version of the situation calculus [10].⁵ Our work differs in that our system is logic-agnostic, and our state spaces consist of a set of arbitrary formulae that may get added to and deleted in keeping with performed actions. Answer-set planning, recently surveyed in [46], translates planning problems to logic problems whose answer sets correspond to solutions or plans for the original planning problem. Instead of finding proofs that actions are applicable or that the goal is reached, answer-set planners find an answer set or logical model that corresponds to a solution. Approaches within answer-set planning typically require the grounding of predicates prior to search. For conformant problems, the number of states within a belief state may grow exponentially with the number of unknown predicates. In our work, it is often the case that the state space does not increase in size with the number of unknown formulae, since a tautology $\phi \vee \lnot \phi$ does not need to be included within a state space. Multiple techniques have been introduced to compile conformant planning problems into classical planning problems via a sound yet incomplete method [33], a complete method for a bounded contingent width [34], and a linear translation for problems of contingent width 1 [5]. All these methods require knowing ahead of time the contingent width of the problem, or in other words the maximum number of uncertain state variables that interact through conditional effects.

3 STRIPS-Inspired Planning over Automated Reasoning

Taking inspiration from STRIPS, we model our planning problem with actions having addition and deletion effects. The main difference is that we’re operating over state spaces as opposed to a single state. A planning-with-formulae (PwF) problem $\Pi$ is the tuple $\langle \mathcal {L}, \mathcal {A}, \Gamma _0, G \rangle$ where $\mathcal {L}$ is some logic, $\mathcal {A}$ is the set of lifted actions that take an agent from one state space to another, $\Gamma _0 \subset \mathcal {L}$ is the initial state space characterized by formulae from the logic, and $G \subset \mathcal {L}$ is a partial state space that represents a goal. Care must be taken to ensure that the initial state space is consistent; otherwise, for logics including the principle of explosion, the goal will be satisfied.

A lifted action $a \in \mathcal {A}$ is a tuple $\langle \chi , \texttt{Pre}, \texttt{Add}, \texttt{Del}, C \rangle$ where $\chi$ is a set of variables and $\texttt{Pre}$ a partial state space, parameterized by $\chi$ and required to be be satisfied in order for an action to be taken. $\texttt{Add}$ is the set of formulae, parameterized by $\chi$, that get added to the state space $\Gamma$ when the action is taken. $\texttt{Del}$ is the set of formulae, parameterized by $\chi$, that gets removed from the state space $\Gamma$ when the action is taken. Lastly, $C \in \mathbb {N}$ is the cost of the action, assumed to be 1 if left unspecified. A substitution is a mapping from a variable to a term. Let $Dom(\sigma )$ return the domain of a substitution $\sigma$. Then for a given action a, a substitution $\sigma$ is valid iff it has a mapping for all the variables in $\chi$ within the action. That is, $\forall v \in \chi (a), v \in Dom(\sigma )$. A ground action $ground (a, \sigma )$ from an action a and valid substitution $\sigma$ is the tuple $\langle \emptyset , \texttt{Pre}^\prime , \texttt{Add}^\prime , \texttt{Del}^\prime , C \rangle$. In this tuple, $\texttt{Pre}^\prime = \{ f\sigma \mid f \in \texttt{Pre}\}$. A similar formulation is defined for $\texttt{Add}^\prime$ and $\texttt{Del}^\prime$. We denote $a_g$ to be an arbitrary grounding of an action a. A state space $\Gamma$ satisfies a partial state space $\gamma$ iff $\Gamma \vdash \gamma$. A ground action $a_g$ is applicable in state space $\Gamma _t$ iff $\Gamma _t$ satisfies $\texttt{Pre}(a_g)$. If an applicable ground action $a_g$ is executed on state space $\Gamma _t$, then the next state space is $\Gamma _{t + 1} = (\Gamma _t - \texttt{del}(a_g)) \cup \texttt{add}(a_g)$. A solution to the PwF problem $\Pi$ is a plan $\pi = (a_1, \dots , a_n)$ that takes an agent from an initial state space to a state space that satisfies the goal, where each $a_i \in \pi$ is an applicable action.

There are two key points in this formulation where an automated reasoner is crucial; the first is in deciding whether or not a given state space $\Gamma _t$ satisfies the goal G. This is determined as an entailment check by an automated reasoner (e.g. $\Gamma _t \stackrel{?}{\vdash} G$). Secondly, we rely on the automated reasoner to find the set of applicable grounded actions $A_g$ for a given action a. This is equivalent to finding the set of substitutions $\sigma$ that when applied to our precondition, the grounded precondition holds under the current state space $\Gamma _t$. For an arbitrary $\sigma _i \in \sigma$, i.e. for all $f \in \texttt{Pre}(a)$, we have $\Gamma _t \vdash f \sigma _i$. It is possible that the size of $\sigma$ is empty or infinite depending on the theory used. If $\sigma$ is empty, then we are unable to apply any grounded actions from that particular lifted action. In the infinite case, we would need to place a bound on the length of $\sigma$ returned by the automated reasoner.

In addition to changes in the planning structure, Spectra relaxes a few of the commonly made assumptions in model-based automated planning. Spectra does not assume CWA, domain closure, or the unique-name assumption. Nor does Spectra require that all grounded actions are found in the beginning portion of the algorithm. Instead, Spectra relies on the question-answering algorithm to iteratively find applicable actions.

4 Implementation

Spectra is implemented using the programming language Java and it’s source code is available on GitHub (https://github.com/rairlab/spectra). Similar to model-based automated planners, we employ the $A^*$ search algorithm as our core loop in order to find K plans that solve the given PwF problem P. An item in our search space $\omega$ is a tuple $\langle \Gamma _t, \pi \rangle$, where $\Gamma _t$ is a state space and $\pi$ the plan to get the initial state space $\Gamma _0$ to $\Gamma _t$. We make use of a priority queue $\Omega$ consisting of tuples $\omega$. Each $\langle \Gamma _t, \pi \rangle \in \Omega$ is assigned a priority $h(\Gamma _t) + C(\pi )$, where h is the heuristic function over state spaces and C the cost function over plans. In our current implementation, we assign an uninformed heuristic over all state spaces, i.e. $\forall \Gamma , h(\Gamma ) = 0$. Future work will include identifying domain-independent heuristics that can apply over a wide range of logics. Given an admissible heuristic, the first plan we find will be optimal. However, the other generated plans may not be optimal due to duplicate pruning. $C(\pi )$ is the cost of a plan $\pi$, which is the sum of the cost of all actions within $\pi$, i.e.

$$\begin{aligned} C(\pi ) = \sum _{a \in \pi }C(a). \end{aligned}$$

Algorithm 1

$A^*$ Search Over PwF Problem

The core search procedure is specified in Algorithm 1. We perform an $A^*$ search over the transition space until either no more applicable actions can be performed, or the number of requested plans have been met. Viewing the core loop from the perspective of an arbitrary $\omega = \langle \Gamma _t, \pi _t \rangle \in \Omega$: We first check if the current state space $\Gamma _t$ satisfies our goal. This is equivalent to making a call to an automated reasoner to see if $\Gamma _t \vdash G$. If so, we add $\pi _t$—the plan to get from $\Gamma _0$ to $\Gamma _t$—to the list of found plans. Then for each lifted action $a \in A$, we find the set of applicable ground actions for the state space $\Gamma _t$. As described in Sect. 3, we rely on the question-answering algorithm of the automated reasoner to find a set $\sigma$ of valid substitutions for the given action. If $\sigma$ is non-empty, then for each $\sigma _i \in \sigma$ we ground the lifted action. With each grounded action, we compute a new $\omega$ consisting of our new state space $\Gamma _{t + 1}$ and the plan to get from the initial state space to $\Gamma _{t + 1}$; i.e. $\omega = \langle \Gamma _{t + 1}, \pi _t \cup \{ a_g \} \rangle$. This new $\omega$ gets added to the priority queue if $\Gamma _{t + 1}$ has not already been visited.

5 Cognitive Planning with $\mathcal {DCC}$

ShadowProver [19] is an automated reasoner over cognitive calculi such as $\mathcal {DCEC}$. It is under active development with support for entailment and enhanced question-answering. Again, herein we use the fragment $\mathcal {DCC}$ of $\mathcal {DCEC}$ in which the number of cognitive operators are reduced and all timepoints are identified. Consider the Grapevine domain from [32]. In this problem, a group of agents have a secret they may wish to communicate with each other. Agents in this environment can move freely between rooms and broadcast to everyone in the room their secret. The initial state of this problem specifies that agents only know their own secret. One possible goal is for an agent to propagate their secrets to a subset of agents. Let’s analyze an instance of this problem with $n = 3$ agents and $p = 2$ rooms. As before, each agent has their own secret, and no one except a believes a’s secret. Ignoring type predicates and unique-name axioms, the initial state space can be characterized as

$$\begin{aligned} \Gamma _0 = \{ at(a, p1), \lnot at(a, p2), at(b, p1), \lnot at(b, p2), at(c, p1) \\ \lnot at(c, p2), \textbf{B}(a, the(a)), \textbf{B}(b, the(b)), \textbf{B}(c, the(c)),\\ \lnot \textbf{B}(b, the(a)) \lnot \textbf{B}(c, the(a)) \} \end{aligned}$$

The goal for this problem includes three components: 1) agent b believes a’s secret; 2) c does not believe a’s secret; 3) agent a believes that agent b believes a’s secret. The partial state space G is then specified as:

$$\begin{aligned} G = \{ \textbf{B}(b, the(a)), \lnot \textbf{B}(c, the(a)), \textbf{B}(a, \textbf{B}(b, the(a))) \} \end{aligned}$$

The available actions are: left, right, share-both, share-single. We denote $p_1$ as the left room and $p_2$ as the right room. For an agent to move left, they must be in the right room; vice versa for the right action. For the share-both action, all agents must be in the same room. One agent then shares their secret, and both agents believe the secret, and the agent sharing believes that the other agents believe the secret. The action share-single is similar; however, the precondition is that one agent is not in the same room, and that agent does not gain a belief about the secret. We provide an example of how the share-single action would get encoded in Spectra in Fig. 1. Note that in the example we delete the negation of the added formulae in order to stay consistent. The Believes! keyword denotes the model operator $\textbf{B}$ within $\mathcal {DCC}$, and the predicate the represents the secret of the agent specified in its parameter. The figure does not provide a complete example, as one would need to add type restrictions as well as restrictions that all arguments are unique for that lifted action. Requesting $K = 2$ plans from Spectra provides the following two plans:

$$\begin{aligned} \pi _1 = ((\texttt{right}~a)~(\texttt{right}~b)~(\texttt{sharesingle}~a~b~c~p_2)) \end{aligned}$$

and

$$\begin{aligned} \pi _2 = ((\texttt{right}~c)~(\texttt{sharesingle}~a~b~c~p_1)). \end{aligned}$$

Fig. 1

Share-single action from grapevine

6 Planning Under Uncertainty

In the last example, we looked at a problem whose state space is equivalent to a single state. In this section, we discuss how to move beyond this restriction and consider state spaces that represent multiple possible states. This is equivalent to planning under uncertainty. To begin, let us put aside $\mathcal {DCC}$ and consider Spectra using a classical first-order-logic reasoner. What we discuss here will easily extend to the epistemic uncertainty case. So, consider the “safe problem” from the conformant planning literature [36]. In this problem, there is a closed safe and the agent has only one correct combination out of a collection thereof that can open that safe. At the outset of the problem, the agent does not know which one of these combinations is correct. Narrowing to an instance of this problem, consider two possible combinations $c_1$ and $c_2$. The initial state space of this problem is that one of the two combinations is correct. We can represent that as follows:

$$\begin{aligned} \Gamma _0 = \{ (correct(c_1) \wedge \lnot correct(c_2)) \vee (\lnot correct(c_1) \wedge correct(c_2)) \} \end{aligned}$$

There is one available action, try, which takes a combination and, if it’s correct, opens the safe. The try action is shown in Fig. 2. Note that the condition that the combination is correct is only specified in the addition effect. This is because for the action try to be applicable for a given state space $\Gamma _t$, all states $s \in \Gamma _t$ must satisfy the preconditions of try. Now imagine that the agent tried both combination $c_1$ and $c_2$ sequentially from the initial state. The updated state space is then:

$$\begin{aligned} \Gamma _2 = \Gamma _0 \cup \{ correct(c_1) \rightarrow open, correct(c_2) \rightarrow open\} \end{aligned}$$

Fig. 2

Action with Conditional Effect in Spectra

The alert reader might notice that $\Gamma _2$ satisfies the goal of opening the safe. This can be shown by proof-by-cases on the disjunctive formula and applying the appropriate modus ponens for each case.

6.1 The Use of Defeasible Reasoning

A challenge arises for our STRIPS-inspired model when we want to swap the valuation of an unknown formula $\phi$. More formally, suppose at a state space $\Gamma _t$ that $\phi$ is unknown; i.e. $\Gamma _t \not \vdash \phi$ and $\Gamma _t \not \vdash \lnot \phi$. Let’s consider that $\phi$ holds for some states s within $\Gamma _t$ and denote this set as $\Gamma _t^+$. The parallel, assume, holds for the negated case; the set here is $\Gamma _t^-$. Now assume that after we execute some applicable action, we want $\lnot \phi$ to hold in the next state space for all states in $\Gamma _t^+$, and $\phi$ to hold in the next state space for all states in $\Gamma _t^-$. How exactly can we model this? To make the formal challenge more concrete, consider an alternative to the safe problem from before. Three lockers A, B, C appear before the agent with a button to toggle whether locker A is locked or not. At the initial configuration there are two possibilities, either $\Gamma _{0, 0} = locked(A) \wedge locked(B) \wedge \lnot locked(C)$ or $\Gamma _{0, 1} = \lnot locked(A) \wedge locked(B) \wedge locked(C)$. Therefore, the initial state space $\Gamma _0 = \{ \Gamma _{0, 0} \vee \Gamma _{0, 1} \}$. Note from the initial state that the agent does not know whether the locker A is locked.

Note that in “real life” such epistemic indeterminacy with regard to binary conditions of devices and systems is far from uncommon. That is, humans are often forced to be rationally agnostic belief-wise when faced with wanting to know whether or not some system s has property R (i.e., a human sometimes must rationally believe neither R(s) nor $\lnot R(s)$), while at the same time having the ability to perform an action that will cause either R(s) or $\lnot R(s)$ to obtain. For example, when leaving his home in a rush for a crucial engagement, Smith activates the alarm system for it at an interior keypad. When he returns home he does not remember whether he activated the alarm or not. As in our safe scenario, his combination applied to an external keypad toggles the system on if off, and off if on, and he doesn’t recall what the indicator lights indicate on this external keypad. He must remain noncommittal after tapping in the combination, and resort to other approaches to relieve his agnosticism.

One approach to tackling the toggle action in the simpler safe challenge, which is better for technical exposition, is to use FOL to have the following effects added to the state space: (1) $locked(A) \rightarrow \lnot locked(A)$ and (2) $\lnot locked(A) \rightarrow locked(A)$. However, both of these effects together yield a contradiction by simple deduction.

To address the problem, we can use defeasible reasoning.⁶ Consider a defeasible logic such as $\mathcal {IDCEC}$ [9, 17]. The schema in the  $\mathcal {IDCEC}$ Belief Propagation box shows that beliefs are propagated forward in time as long as doing so doesn’t contradict any newer beliefs. At the initial state ($t = 0$), we can represent the state space as $\Gamma _0 = \{ B(a, 0, \Gamma _{0, 0} \vee \Gamma _{0, 1}) \}$. Then for the toggle action we can set the effects to: (1) $B(a, t, locked(A)) \rightarrow B(a, t + 1, \lnot locked(A))$ and (2) $B(a, t, \lnot locked(A)) \rightarrow B(a, t + 1, locked(A))$. These formulae are no longer contradictory and suitably capture the toggle action as the following noncommittal belief is entailed at the next time step:

$$\begin{aligned} B(a, 1, (\lnot locked(A) \wedge locked(B) \wedge locked(C)) \vee \\ (locked(A) \wedge locked(B) \wedge locked(C))) \end{aligned}$$

7 Discussion and Conclusion

The extension from states with predicates to state spaces with arbitrary formulae catalyzes several challenges. The first is that the problem modeler must take care not to introduce any contradictions in the PwF problem. This is an issue conveniently absent from the STRIPS model, as the user does not specify any negated predicates (as those are assumed via CWA). If contradictions do exist in the PwF model, then for many logics, the goal would be satisfied for any arbitrary contradictory state space. This is due to explosion, from falsum, anything follows. The second challenge is that the computational properties of Spectra are heavily reliant on the underlying automated reasoner. For example, if the underlying automated reasoner is undecidable for entailment and question-answering for a given logic, then Spectra will be incomplete. Such undecidability, in human-level planning, which presumably is a level that must ultimately be reached (or exceeded), is common and irrepressible. Even undergraduate students are routinely required to find proofs of formulae in not only first-order logic and other more expressive extensional logics (e.g. second-order logic), but in quantified modal logics as well. When they are tasked with performing actions that reach these goals, they are embodying the daunting challenge that, in our planning paradigm, Spectra faces.

Of course, this situation gives rise to the question as to how, with undecidability having to be part of what our engineering must factor in, performance is assessed/measured. In our current implementation, we rely on pragmatic time bounds for calls to the automated reasoner. A result returned under the bound for a timer is clear success, because that bound is set for applications at hand. No result before the expiration of the timer is failure, and something else must be tried. This approach is none other than what AI founder and nobelist Herbert Simon famously introduced under the banner “satisficing” as an approach to both human and AI planning and deciding (e.g. see [44]).⁷

Importantly, undecidability does not in any way stop engineering designed to mitigate it. Accordingly, when using Spectra with a monotonic logic, we for instance include optimizations to reduce the number of calls to the automated reasoner. For example, if we have cached that $\Gamma _1 \vdash \phi$, then we assume for an arbitrary $\Gamma _2$ that $\Gamma _1 \cup \Gamma _2 \vdash \phi$. Also, consider we have cached that $\Gamma _1 \not \vdash \phi$. Then for $\Gamma _2 \subseteq \Gamma _1$, we assume that $\Gamma _2 \not \vdash \phi$. Of course, in addition, predictably, our engineering in service of reasoner-based planning in the face of undecidability includes making use, whenever possible, of automated reasoners for decidable fragments of both first-order logic and propositional modal logics; details here are beyond present scope, but see [19].

Formulae in Spectra are treated strictly syntactically when updating state spaces. This is because in general consistency and redundancy checks are (again) undecidable for an arbitrary logic. Future work includes adding an additional layer which is able to perform quick (potentially incomplete) consistency and redundancy checks for a wide range of logics. For example, when deleting $A \wedge B$, this layer can additionally check for $B \wedge A$ and delete this. While this may not hold for logics in general, a wide class of logics share first-order semantics, which we can provide a default layering over. Additionally, in work described herein, we presented an uninformed heuristic $h(\Gamma ) = 0$ for all state spaces $\Gamma$. Future work includes investigating heuristics that can hold for a wide range of logics.

To briefly recap, we presented Spectra, a logic-agnostic AI planner based on automated reasoning. We discussed how the extension from states with predicates to state spaces with arbitrary formulae enables high-expressivity processing and captures uncertainty in the PwF problem. We additionally discussed how using non-classical, intensional reasoners such as ShadowProver over $\mathcal {DCC}$ allows Spectra to create complex cognitive plans, such as ones with epistemic goals. Lastly, we discussed how defeasible logics in conjunction with Spectra can be used to solve a larger class of conformant planning problems. Future work also includes incorporating a perception model into Spectra. And the authors are particularly interested in using inductive reasoning to capture the adjudication of competing arguments an agent might need to face, as a way to carry out sophisticated defeasible reasoning in service of planning.