A Multiple-Conclusion Meta-Logic

The theory of cut-free sequent proofs has been used to motivate and justify the design of a number of logic programming languages. Two such languages, Prolog and its linear logic refinement, Lolli [12], provide for various forms of abstraction (modules, abstract data types, higher-order programming) but lack primitives for concurrency. The logic programming language, LO (Linear Objects) [2] provides for conbut lacks abstraction mechanisms. In this paper we present Forum, a logic programming presentation of all of linear logic that modularly extends the languages Prolog, Lolli, and LO. Forum, therefore, allows specifications to incorporate both abstractions and concurrency. As a meta-language, Forum greatly extends the expressiveness of these other logic programming languages. To illustrate its expressive strength, we specify in Forum a sequent calculus proof system and the operational semantics of a functional programming language that incorporates such nonfunctional features as count...

• Type: Conference
• Year: 1994
• Where: LICS
• Authors: Dale Miller
• Keywords: Automated Reasoning, LICS 1994, Linear Logic, Linear Logic Refinement, Logic Programming Languages