**STSM WG4 (Pere Pardo)**

**Start Date: **2011-07-15

**End Date: **2011-10-15

**Host Institution: **Oxford University

**Host Country: **UK

**Home Institution: **IIIA-CSIC Barcelona

**Home Country: **Spain

**Description: **

We want to be able to combine planning with reasoning given by some logic, specially for the case of Dynamic Epistemic Logic (DEL). The motivation is to be able to argue in negotiation problems where the epistemic states of agents are relevant and epistemic actions exist.

For this, two alternative directions seem appropriate: (1) embed the logic into planning thus defining a new planning system (and prove search-theoretic properties of this new system); or (2) embed plan search techniques to a logic, e.g. reason fromgoals to the current state with dynamic operators standing for actions.

The idea is to research along either line above: for (1), define (a sub-class of) proofs as proof steps, i.e. valid plan steps

during plan refinement in the new planning system; for (2) define translation functions from planning problems into deduction problems in the corresponding logic (specially, translate planning actions into formulas involving dynamic operators standing for these actions). In either case, the results to be proved would consist in that the resulting framework or deduction problem has some nice properties in terms of (heuristic) search, (1) in the space of plans or (2) in the space of proofs. Finally, the idea is to apply these results to negotiation scenarios involving epistemic states of agents, where services to be exchanged are modeled by actions/dynamic operators.

STSM Report