The ILLTP library for intuitionistic linear logic

MaRDI QIDQ5018490zbMATH OpenFDO

Authors Carlos Olarte, Elaine Pimentel, Giselle Reis, Valeria de Paiva

Publication date 20 December 2021

Full work available at URL https://arxiv.org/abs/1904.06850, http://eptcs.web.cse.unsw.edu.au/paper.cgi?LinearityTLLA2018.7

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• The ILTP problem library for intuitionistic logic
• Automated Reasoning with Analytic Tableaux and Related Methods
• The TPTP problem library
• The QMLTP problem library for first-order modal logics
• TPTP, TSTP, CASC, etc.

Cites work

• A formal framework for specifying sequent calculus proof systems
• A framework for proof systems
• A linear logical framework
• Algebra and Coalgebra in Computer Science
• An adequate compositional encoding of bigraph structure in linear logic with subexponentials
• Around classical and intuitionistic linear logics
• Automated Deduction – CADE-20
• Decision problems for propositional linear logic
• Efficient resource management for linear logic proof search
• Focusing and polarization in linear, intuitionistic, and classical logics
• scientific article; zbMATH DE number 3885321 (Why is no real title available?)
• scientific article; zbMATH DE number 1088191 (Why is no real title available?)
• scientific article; zbMATH DE number 1489627 (Why is no real title available?)
• scientific article; zbMATH DE number 1499088 (Why is no real title available?)
• scientific article; zbMATH DE number 1405458 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• Intuitionistic hybrid logic
• Linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• On concurrent behaviors and focusing in linear logic
• On the linear decoration of intuitionistic derivations
• Proof strategies in linear logic
• Resolution calculus for the first order linear logic
• Some Syntactical Observations on Linear Logic
• The ILTP problem library for intuitionistic logic
• The QMLTP problem library for first-order modal logics
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Twenty years of rewriting logic
• Typed multiset rewriting specifications of security protocols

Cited in

(5)

• ILLTP
• Resourceful program synthesis from graded linear types
• scientific article; zbMATH DE number 7455712 (Why is no real title available?)
• Automated Reasoning with Analytic Tableaux and Related Methods
• The ILTP problem library for intuitionistic logic

Describes a project that uses

Uses Software

• Lolli
• ILTP
• TPTP
• QMLTP
• Sympli
• linTAP
• llprover

This page was built for publication: The ILLTP library for intuitionistic linear logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5018490)