The ILTP problem library for intuitionistic logic

DOI10.1007/S10817-006-9060-ZMaRDI QIDQ877897zbMATH OpenOpenAlexFDO

Authors Thomas Raths, Jens Otten, Christoph Kreitz

Publication date 4 May 2007

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-006-9060-z

zbMATH Keywords

Automated Theorem Proving

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20)

Recommendations

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

Cites work

• An Intuitionistic Predicate Logic Theorem Prover
• Automated Reasoning with Analytic Tableaux and Related Methods
• Automated Reasoning with Analytic Tableaux and Related Methods
• Contraction-free sequent calculi for intuitionistic logic
• scientific article; zbMATH DE number 1614694 (Why is no real title available?)
• scientific article; zbMATH DE number 1765687 (Why is no real title available?)
• scientific article; zbMATH DE number 1770113 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• SATLIB: An online resource for research on SAT
• The axioms of constructive geometry
• The TPTP problem library. CNF release v1. 2. 1

Cited in

(25)

• The TPTP problem library. CNF release v1. 2. 1
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• Machine learning guidance for connection tableaux
• Efficient SAT-based proof search in intuitionistic propositional logic
• The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics
• Theorem prover for intuitionistic logic based on the inverse method
• A tableaux calculus for default intuitionistic logic
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• The QMLTP problem library for first-order modal logics
• Intuitionistic Decision Procedures Since Gentzen
• Disproving using the inverse method by iterative refinement of finite approximations
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications
• Automating theories in intuitionistic logic
• From Schütte’s Formal Systems to Modern Automated Deduction
• The ILLTP library for intuitionistic linear logic
• Practical Proof Search for Coq by Type Inhabitation
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
• Automated Reasoning with Analytic Tableaux and Related Methods
• General clauses for SAT-based proof search in intuitionistic propositional logic
• Two applications of logic programming to Coq
• Optimization techniques for propositional intuitionistic logic and their implementation
• Fast decision procedure for propositional Dummett logic based on a multiple premise tableau calculus

Describes a project that uses

Uses Software

• STRIP
• ILTP
• TPTP
• ileanCoP
• SATLIB
• JProver

This page was built for publication: The ILTP problem library for intuitionistic logic

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