The ILTP problem library for intuitionistic logic

DOI10.1007/s10817-006-9060-zzbMath1113.68093OpenAlexW2127391555MaRDI QIDQ877897

Jens Otten, Thomas Raths, 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)

Related Items

Practical Proof Search for Coq by Type Inhabitation, The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics, Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations, The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0, The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0, Unnamed Item, Goal-oriented proof-search in natural deduction for intuitionistic propositional logic, leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions), Intuitionistic Decision Procedures Since Gentzen, Optimization techniques for propositional intuitionistic logic and their implementation, Progress in the Development of Automated Theorem Proving for Higher-Order Logic, Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method, Fast decision procedure for propositional Dummett logic based on a multiple premise tableau calculus, Machine learning guidance for connection tableaux, Efficient SAT-based proof search in intuitionistic propositional logic, A tableaux calculus for default intuitionistic logic, 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

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The TPTP problem library. CNF release v1. 2. 1
• The axioms of constructive geometry
• Contraction-free sequent calculi for intuitionistic logic
• An Intuitionistic Predicate Logic Theorem Prover
• Automated Reasoning with Analytic Tableaux and Related Methods
• Automated Reasoning with Analytic Tableaux and Related Methods