An Intuitionistic Predicate Logic Theorem Prover
From MaRDI portal
Recommendations
- A resolution theorem prover for intuitionistic logic
- \(\mathsf{ileanTAP}\): an intuitionistic theorem prover
- A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic
- fCube: an efficient prover for intuitionistic propositional logic
- A proof-search procedure for intuitionistic propositional logic
Cited in
(43)- Intuitionistic logic according to Dijkstra's calculus of equational deduction
- A circumscriptive theorem prover
- A family of goal directed theorem provers based on conjunction and implication. I
- An improved refutation system for intuitionistic predicate logic
- Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
- Inhabitants of intuitionistic implicational theorems
- Theorem proving for intensional logic
- The propositional formula checker HeerHugo
- Subformula linking for intuitionistic logic with application to type theory
- A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic
- Theorem prover for intuitionistic logic based on the inverse method
- Automata theory approach to predicate intuitionistic logic
- Theorem proving for untyped constructive -calculus: Implementation and application
- Quantifier handling issues in computer-oriented intuitionistic calculi
- A note on the independence of premiss rule
- Predicate Elimination for Preprocessing in First-Order Theorem Proving
- An evaluation-driven decision procedure for G3i
- A history-based theorem prover for intuitionistic propositional logic using global caching: IntHistGC system description
- Intuitionistic Decision Procedures Since Gentzen
- scientific article; zbMATH DE number 4164169 (Why is no real title available?)
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- An Evaluation Based Theorem Prover
- scientific article; zbMATH DE number 4072441 (Why is no real title available?)
- scientific article; zbMATH DE number 4094866 (Why is no real title available?)
- A note on the existence property for intuitionistic logic with function symbols
- scientific article; zbMATH DE number 52087 (Why is no real title available?)
- A Proof-theoretic Analysis of Goal-directed Provability
- scientific article; zbMATH DE number 1770113 (Why is no real title available?)
- Two loop detection mechanisms: a comparison
- \(\mathsf{ileanTAP}\): an intuitionistic theorem prover
- A resolution theorem prover for intuitionistic logic
- Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
- fCube: an efficient prover for intuitionistic propositional logic
- Deciding intuitionistic propositional logic via translation into classical logic
- \textsc{Minlog}: a minimal logic theorem prover
- Automated Reasoning with Analytic Tableaux and Related Methods
- Dynamic logic as a uniform framework for theorem proving in intensional logic
- On the modal logic K plus theories
- Machine-checked meta-theory of dual-tableaux for intuitionistic logic
- A general proof rule for procedures in predicate transformer semantics
- The ILTP problem library for intuitionistic logic
- A logical characterization of forward and backward chaining in the inverse method
- Optimization techniques for propositional intuitionistic logic and their implementation
This page was built for publication: An Intuitionistic Predicate Logic Theorem Prover
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5285991)
