Forum(ID:5031/for074)

Linear Logic specification language

"Forum is a presentation of all of higher-order linear logic that makes it into a logic programming language"
References:
  • Miller, D. "A multiple-conclusion meta-logic" view details
          in Abramsky, S. editor, Ninth Annual Symposium on Logic in Computer Science, Paris, France, July 1994. IEEE Computer Society Press. view details
  • Chirimar, J. Proof Theoretic Approach to Specification Languages. PhD thesis, Department of Computer and Information Science, University of Pennsylvania, 1995. view details
          in Abramsky, S. editor, Ninth Annual Symposium on Logic in Computer Science, Paris, France, July 1994. IEEE Computer Society Press. view details
  • Miller, D. A Multiple-Conclusion Meta-Logic. Theoretical Computer Science 165(1): 201-232 (1996). view details
          in Abramsky, S. editor, Ninth Annual Symposium on Logic in Computer Science, Paris, France, July 1994. IEEE Computer Society Press. view details
  • Christian Urban "Forum and its Implementation" MPhil thesis St. Andrews 1997 view details Abstract: Miller presented Forum as a specification logic: Forum extends several existing logic programming languages, for example Lambda-Prolog, LO and Lolli. The crucial change in Forum is the extension from single succedent sequents, as in intuitionistic logic, to multiple succedent sequents, as in classical logic, with a corresponding extension of the notion of uniform proof.
    Forum uses the connectives of linear logic. Languages based on linear logic offer extra expressivity (in comparison with traditional logic languages), but also present new implementation challenges. One such challenge is that of context management, because the multiplicative linear connectives `times', `par' and `lollipop' require context splitting. Hodas and Miller presented a solution (the IO model) to this in 1991 for the language Lolli based on minimal linear logic. This thesis presents a technique which is an adaptation of the aforementioned approach for the language Forum and following a suggestion of Miller that the `?' constant be treated as primitive in order to avoid looping problems arising from its use as a derived symbol. Cervesato, Hodas and Pfenning have presented a technique for managing the `top' constant, dividing each input context into a "slack'' part and a "strict'' part; the main novel contribution of this thesis is to modify this technique, by dividing instead the output context. This leads to a proof system with fewer rules (and consequent ease of implementation) but enhanced performance, for which we present some experimental evidence.
          in Abramsky, S. editor, Ninth Annual Symposium on Logic in Computer Science, Paris, France, July 1994. IEEE Computer Society Press. view details
    Resources