Reasoning about types of action and agent capabilities
Chrysafis Hartonas · Logic Journal of IGPL · 2012
We present a logical system for reasoning about types of actions (processes) and about agent capabilities to execute types of actions. The syntax of the system is based on that of Propositional Dynamic Logic (PDL), though the semantics we define is different (interpreting process terms as types, i.e. sets of binary relations). The standard PDL syntax is extended with capabilities statements, as in the KARO framework, atomic process types specified as precondition-effect pairs, written as ϕ ⇒ ψ, as well as backwards possibility operators. The resulting system is shown (by filtration) to have a decidable satisfiability problem and a sound and complete Gentzen-style proof system is presented.