Logic of execution: An outline

Abstract

Logic of Execution is a logical framework of executing sentences, and it is aimed to provide a logical basis of concurrency and parallelism. We use

to express that the success of execution of A produces the success of execution of B. We assume that an execution of a statement will fall into one of success,failure and pending. We consider a set of executional operators: [;] (sequential execution), [+] (disjunctive execution), [V] (execution by non-deterministic choice), [&] (conjunctive execution), [|] (concurrent execution), [#] (parallel execution), [¬] (negation) and [C] (completion). A deductive system of Logic of Success of Execution is given in a propositional level. On the basis of this Logic of Execution how to execute propositional sentences is discussed,giving a set of executional rules for a sentence composed from the logical connectives. From the standpoint of the traditional logics the logic of execution has the 2-level structures:

• (1) the logical framework of execution for the executional operators, and

• (2) the framework to execute logical sentences ; that is, a set of rules to transform a logical sentence into a formula of the logic of execution.

The logic of execution is more expressible than Girard's Linear Logic, since it treats various modes of execution, including [V],[|] and [#]. Some remarks are given in connection with the traditional logics, and some topics for future study are also mentioned.