Semantics of Concurrent Logic Programming as Uniform Proofs.
Paolo Volpe · 1994
We describe LC , a formalism based on the proof theory of linear logic, whose aim is to specify concurrent computations and whose language restriction (as compared to other linear logic language) provides a simpler operational model that can lead to a more practical language core. The LC fragment is proveded to be an abstract logic programming language, that is any sequent can be derived by uniform proofs. The resulting class of computations can be viewed in terms of multiset rewriting and is reminiscent of the computations arising in the Chemical Abstract Machine and in the Gamma model. The fragment makes it possible to give a logic foundation to existing extensions of Horn clause logic, such as Generalized Clauses, whose declarative semantics was based on an ad hoc construction. Programs and goals in LC can declaratively be characterized by a suitable instance of the phase semantics of linear logic. A declarative semantics, modeling answer substitutions, is associated to every LC p...