Valeria Correa Vaz De Paiva
University of Birmingham
Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well-established method for measuring their performance. However, the availability of such libraries for non-classical logics is very limited. In this work we propose a library for benchmarking Girard's (propositional) intuitionistic linear logic. For a quick bootstrapping of the collection of problems, and for discussing the selection of relevant problems and understanding their meaning as linear logic theorems, we use translations of the collection of Kleene's intuitionistic theorems in the traditional monograph "Introduction to Metamathematics". We analyze four different translations of intuitionistic logic into linear logic and compare their proofs using a linear logic based prover with focusing. In order to enhance the set of problems in our library, we apply the three provability-preserving translations to the propositional benchmarks in the ILTP Library. Finally, we generate a comprehensive set of reachability problems for Petri nets and encode such problems as linear logic sequents, thus enlarging our collection of problems.
Keywords intuitionistic linear logic  petri nets  provers
Categories (categorize this paper)
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

 PhilArchive page | Other versions
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Resolution Calculus for the First Order Linear Logic.Grigori Mints - 1993 - Journal of Logic, Language and Information 2 (1):59-83.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Completeness Results for Linear Logic on Petri Nets.Uffe Engberg & Glynn Winskel - 1997 - Annals of Pure and Applied Logic 86 (2):101-135.
The Completeness of Linear Logic for Petri Net Models.K. Ishihara & K. Hiraishi - 2001 - Logic Journal of the IGPL 9 (4):549-567.
Full Intuitionistic Linear Logic.Martin Hyland & Valeria de Paiva - 1993 - Annals of Pure and Applied Logic 64 (3):273-291.
On the Unity of Logic.Jean-Yves Girard - 1993 - Annals of Pure and Applied Logic 59 (3):201-217.
The Logic of Bunched Implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
Reflections on “Difficult” Embeddings.Andreja Prijatelj - 1995 - Journal of Philosophical Logic 24 (1):71 - 84.
On an Intuitionistic Logic for Pragmatics.Gianluigi Bellin, Massimiliano Carrara & Daniele Chiffi - 2018 - Journal of Logic and Computation 50 (28):935–966..
Temporal Gödel-Gentzen and Girard Translations.Norihiro Kamide - 2013 - Mathematical Logic Quarterly 59 (1-2):66-83.
A Mixed Λ-Calculus.Marie-Renée Fleury & Myriam Quatrini - 2007 - Studia Logica 87 (2-3):269-294.


Added to PP index

Total views
40 ( #240,467 of 2,344,159 )

Recent downloads (6 months)
40 ( #16,452 of 2,344,159 )

How can I increase my downloads?


My notes