Abstract | ||
---|---|---|
There is an increasing interest in the relation between logic and the changes involved in reasoning and, specifically, in plan generation. Up to now, several attempts in this direction have been made, either by embedding actions into a classical framework or by using nonstandard formalisms. We think that these attempts, though promising, miss their objectives, for a lack of a suitable logic, and that the effort must be pursued. In this paper, we show how to obtain a strong and clean correspondence between proofs and sequences of actions by using only Girard's linear logic, eliminating from the classical logic the structural rules which are not adapted to our purpose. A theorem is presented which expresses the new adequacy between proofs and actions. |
Year | DOI | Venue |
---|---|---|
1990 | 10.1016/0304-3975(93)90007-G | Theoretical Computer Science |
Keywords | Field | DocType |
linear logic,weed management | Modalities,Atomic formula,Discrete mathematics,Computer science,Sequent calculus,Formalism (philosophy),Linear logic,Completeness (statistics),Bounded function | Conference |
Volume | Issue | ISSN |
113 | 2 | Theoretical Computer Science |
ISBN | Citations | PageRank |
0-387-53487-3 | 34 | 2.57 |
References | Authors | |
7 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
M. Masseron | 1 | 90 | 5.88 |
Christophe Tollu | 2 | 126 | 57.12 |
Jacqueline Vauzeilles | 3 | 81 | 11.63 |