WhaleProver: first-order intuitionistic theorem prover based on the inverse method

DOI10.1007/978-3-319-74313-4_23zbMATH Open1461.68247OpenAlexW2783704968MaRDI QIDQ4989679FDOQ4989679

Authors: Vladimir Pavlov, Vadim Pak 

Publication date: 26 May 2021

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-74313-4_23

Recommendations

• Theorem prover for intuitionistic logic based on the inverse method
• The inverse method application for non-classical logics
• A resolution theorem prover for intuitionistic logic
• \(\mathsf{ileanTAP}\): an intuitionistic theorem prover
• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method

zbMATH Keywords

intuitionistic logictheorem provingautomated reasoningproof assistantsinverse methodILTP

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited In (1)

• Theorem prover for intuitionistic logic based on the inverse method

Uses Software

• WhaleProver

This page was built for publication: WhaleProver: first-order intuitionistic theorem prover based on the inverse method

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