Deductive Formation of Recursive Workflows

Abstract

We present an action theory with the power to represent recursive plans and the capability to reason about and synthesize recursive workflow control structures. In contrast with the software verification setting, reasoning does not take place solely over predefined data structures, and neither is there a process specification available in recursive form. Rather, specification takes the form of goals, and domain structure takes the form of a physical application setting containing objects. For this reason, well-founded induction is employed for its suitability for practical action domains where recursive structures must be described or inferred. Under this method, termination of the synthesized recursive workflow is a property that follows automatically. We show how a general workflow recursive construct is added to an action language that is then augmented with induction. This formalism is then transformed in a way amenable to automated reasoning. We demonstrate the method with a particular example specified in the theory, and then extracted from a proof constructed by the SNARK first-order theorem prover.

Keywords: Artificial Intelligence, Artificial Intelligence Center, AIC, workflow, recursive plans, theorem proving, well-founded induction, resolution, action theory, program extraction, termination