The paper introduces a semantics for the language of classical ΓΏrst order logic supplemented with the additional operators and l. This semantics understands formulas as tasks. An agent (say, a machine or a robot), working as a slave for its master (say, the user or the environment), can carry out the task ΓΏ if it can carry out any one of the two tasks ; ΓΏ, depending on which of them was requested by the master; similarly, it can carry out lx (x) if it can carry out (x) for any particular value for x selected by the master; an agent can carry out β ΓΏ if it can carry out ΓΏ as long as it has, as a slave (resource), an agent who carries out ; ΓΏnally, carrying out P, where P is an atomic formula, simply means making P true; in particular, β₯ is a task that no agent can carry out. When restricted to the language of classical logic, the meaning of formulas is isomorphic to their classical meaning, which makes our semantics a conservative extension of classical semantics.
This semantics can claim to be a formalization of the resource philosophy associated with linear logic, if resources are understood as agents carrying out tasks. The classical operators of our language correspond to the multiplicative operators of linear logic, while and l correspond to the additive conjunction and universal quantiΓΏer, respectively.
Our formalism may also have a potential to be used in AI as an alternative logic of planning and action. Its main appeal is that it is immune to the frame problem and the knowledge preconditions problem.
The paper axiomatically deΓΏnes a logic L in the above language and proves its soundness and completeness with respect to the task semantics in the following intuitive sense: L i can be carried out by an agent who has nothing but its intelligence (i.e. no physical resources or external sources of information) for carrying out tasks. This logic is shown to be semidecidable in the full language and decidable when the classical quantiΓΏer (but not l) is forbidden in it.