© 1992 by Oxford University Press
Original Articles |
Logic Programming with Focusing Proofs in Linear Logic
E. C. R. C. GmbH Arabellastr. 17 D-8000 Munich
The deep symmetry of linear logic [18] makes it suitable for providing abstract models of computation, free from implementation details which are, by nature, oriented and non-symmetrical. I propose here one such model, in the area of logic programming, where the basic computational priciple is
Computation = Proof search
Proofs cinsidered here are those of the Gentzen style sequent calculus for linear logic. However, proofs in this system may be redundant, in that two proofs canbe syntactically different although identical up to some irrelevant reordering or simplification of the applications of the inferences rules. This leads to an untractable proof search where the search procedure is forced to make costly choices whch turn out to be irrelevant. To overcome this problem, a subclass of proofs, called the ‘focusing’ proofs, which is both complete (any derivable formla in linear logic has a focusing proof) and tractable (many irrelevant choices in the search are eliminated when aimed at focusing proofs) is identified. The main constraint underlying the specificatuon of focusing proofs has been to preserve the symmetry of linear logic, which is its most salient feature. In particular, dual connectives have dual properties with respect to focusing proofs
Then, a progrmming language, called LinLog, consisting of a fragment of linear logic, in which focussing proofs have a more compact form, is presented. Linlog deals with formulae which have a syntax similar to the of the definite clauses and goals of Horn logic, but the crucial difference here is that it allows clauses with multiple atoms in the head, connected by the ‘par’ (multiplicative disjuction). It is then shown that the syntyactic restriction induced by LinLog is not performed at the cost of any expressive power: a mapping from full linear logic to LinLog, preserving focusing proofs, and analogous to the normalization to clausal form for classical logic, is presented.
Keywords: Logic programming; sequent systems; proof normalization; linear logic; parallelism; concurrency.
CiteULike 
Connotea 
Del.icio.us What's this?
This article has been cited by other articles:
|
|
 |
|
  R. Dyckhoff and S. Lengrand Call-by-Value {lambda}-calculus and LJQ J Logic Computation, December 1, 2007; 17(6): 1109 - 1134. [Abstract] [Full Text] [PDF]
|
|