Technical Report WV-03-10 1 December 2003

From Simple Sci Wiki
Revision as of 14:59, 24 December 2023 by SatoshiNakamoto (talk | contribs) (Created page with "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 showe...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigation Jump to search

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

Retrieved from "https://simplesci.org/index.php?title=Technical_Report_WV-03-10_1_December_2003&oldid=2928"