Theorem prover for intuitionistic logic based on the inverse method

DOI10.1134/S036176881801005XzbMath1455.68251OpenAlexW2789694236MaRDI QIDQ2216868

V. A. Pavlov, V. G. Pak

Publication date: 17 December 2020

Published in: Programming and Computer Software (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1134/s036176881801005x

zbMATH Keywords

inverse methodintuitionistic logicautomated theorem provingsoftware verificationILTP

Mathematics Subject Classification ID

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

Uses Software

• Coq
• Prover9
• Mace4
• ileanCoP
• JProver
• GitHub
• WhaleProver

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• What is the inverse method?
• The inverse method and tactics for establishing deducibility for a calculus with functional symbols
• Deduction search in calculi of general type
• Evaluating general purpose automated theorem proving systems
• The inverse method for establishing deducibility for logical calculi
• On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer
• Decidability of the Class E by Maslov’s Inverse Method
• A resolution theorem prover for intuitionistic logic
• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
• Automated Reasoning with Analytic Tableaux and Related Methods

This page was built for publication: Theorem prover for intuitionistic logic based on the inverse method