The Logic Of Tasks

Since the birth of linear logic, the topic of it and substructural logics has drawn the attention of many researchers. The philosophy behind linear logic is that formulas are viewed as resources, therefore, from the semantic point of view, linear logic is often called "resource logic". But this kind of resource philosophy has never been fully formalized.Making use of the technique of game semantics, G.Japaridze first introduced "the logic of tasks" in 1998, where formulas are understood as tasks. He gives the resource semantics for a language which extends the language of linear logic, though its theory is not perfect. In 2002, G.Japaridze introduced a semantics for the language of classical first order logic supplemented with the additional operators fl and 17, axiomatically defined a logic L* in the above language and proved its soundness and completeness, which can claim to be a formalization of the resource philosophy associated with linear logic. He believes the formalism may have a potentiality to be used in AI as an alternative logic of planning, because it is immune to the frame problem and the knowledge preconditions problem.However, the logic of tasks based on classical first order logic introduced by G.Japaridze is undecidable and the theorems in the logic L* are not given, which makes its application restrited. The aim of this paper is to develop the theory of the logic of tasks. It introduces a semantics for the language of classical prepositional logic supplemented with the additional operator , axiomatically defines a logic L, proves its soundness, completeness and decidability, and extensively works out its theorems. At the same time, the logic of tasks based on the classical first order logic is introduced and a new logic L', which is between the logic L and L* and is decidable, is established.In the first part, a semantics for the language of classical propositional logic supplemented with the additional operator is introduced, where formulas are understood as tasks.In the second part, a logic L is establised, whose axioms are all the theorems in classical propositional logic and rules of inference are Rule A and Rule R. The soundness, completeness and decidability of it are proven.In the third part, a sort of theorems in L and the definition of mimicking strategy are given.Lastly, the paper introduces the semantics for the language based on classical first order logic, proposes a logic L' by omiting classical quantifier V, and proves its decidability.