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

DOI10.1007/978-3-319-74313-4_23MaRDI QIDQ4989679zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(1)

• Theorem prover for intuitionistic logic based on the inverse method

Describes a project that uses

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)