An Intuitionistic Predicate Logic Theorem Prover

DOI10.1093/LOGCOM/2.5.619zbMath0786.03010OpenAlexW1981368022MaRDI QIDQ5285991

Dan Sahlin, Torkel Franzén, Seif Haridi

Publication date: 29 June 1993

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: http://urn.kb.se/resolve?urn=urn:nbn:se:ri:diva-21330

zbMATH Keywords

intuitionistic logiccut-free sequent calculusintuitionistic theorem prover

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (13)

The ILTP problem library for intuitionistic logic ⋮ An Evaluation-Driven Decision Procedure for G3i ⋮ Two loop detection mechanisms: A comparison ⋮ ileanTAP: An intuitionistic theorem prover ⋮ Goal-oriented proof-search in natural deduction for intuitionistic propositional logic ⋮ A logical characterization of forward and backward chaining in the inverse method ⋮ leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ A resolution theorem prover for intuitionistic logic ⋮ Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification ⋮ Optimization techniques for propositional intuitionistic logic and their implementation ⋮ On the modal logic K plus theories ⋮ Deciding intuitionistic propositional logic via translation into classical logic

This page was built for publication: An Intuitionistic Predicate Logic Theorem Prover