Title
Logic programming with sequent systems: a linear logic approach
Abstract
The computational interest of SLD-resolution comes from its goal oriented strategy. One step of the computation consists in replacing the current goal (deterministically selected within the resolvent) by the body of a Horn clause (non deterministically selected in the program). This leads to a purely sequential computational model, where the whole computation is represented as a sequence of resolvents. We propose here an extension of Prolog in which the program clauses have multiple heads and which, at the same time, processes multiple current goals in parallel. The resulting computational model is well adapted to the implementation of concurrent systems, especially reactive systems where the computation is viewed as a perpetual interaction between the user(s) and the system. The natural framework for the description of our extension of Prolog is Linear Logic. However, we show here that the sequent system of propositional Classical Logic already contains the necessary tools for our purpose, especially the cut rule together with a Cut normalisation theorem. Further normalisation procedures (concerning the structural rules — Contraction, Weakening and Exchange — and directly inspired by Linear Logic) are required in Classical Logic to obtain the operational system that we propose.
Year
Venue
Keywords
1989
Proceedings of the international workshop on Extensions of logic programming
linear logic approach,logic programming,sequent system,reactive system,linear logic,operating system,classical logic,goal orientation,computer model
Field
DocType
ISBN
Computational logic,Horn clause,Programming language,Computer science,Substructural logic,Sequent,Logic family,Logic programming,Linear logic,Dynamic logic (modal logic)
Conference
3-540-53590-X
Citations 
PageRank 
References 
9
1.41
6
Authors
2
Name
Order
Citations
PageRank
Jean-Marc Andreoli176472.75
Remo Pareschi2601162.52