Technical Report WV-03-10 1 December 2003

Title: Technical Report WV-03-10 1 December 2003

Research Question: How can the proof search for first-order linear logic be structured to make it more amenable to operational semantics and proof-theoretic analysis?

Methodology: The researchers introduced a new system called G-Forum, which is a restriction of Miller's Forum system. This system only allows certain types of formulae, making the proofs more structured and easier to analyze.

Results: The researchers showed that G-Forum is equivalent to full first-order linear logic, despite the restrictions placed on the formulae. They also developed a cut elimination procedure for G-Forum, demonstrating that it has good proof-theoretic qualities.

Implications: The development of G-Forum has important implications for the field. It provides a more manageable system for studying the operational semantics of proofs, and it offers a new approach to proof-theoretic analysis. This could lead to advancements in the application of linear logic to domains like concurrency and planning.

Link to Article: https://arxiv.org/abs/0312002v1 Authors: arXiv ID: 0312002v1