Title: Herbrand Constructivization for Automated Intuitionistic Theorem Proving
Abstract: We describe a new method to constructivize proofs based on Herbrand disjunctions by giving a practically effective algorithm that converts (some) classical first-order proofs into intuitionistic proofs. Together with an automated classical first-order theorem prover such a method yields an (incomplete) automated theorem prover for intuitionistic logic. Our implementation of this prover approach, Slakje, performs competitively on the ILTP benchmark suite for intuitionistic provers: it solves 1674 out of 2670 problems (1290 proofs and 384 claims of non-provability) with Vampire as a backend, including 800 previously unsolved problems.
Publication Year: 2019
Publication Date: 2019-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 1
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot