zbMATH — the first resource for mathematics

Herbrand constructivization for automated intuitionistic theorem proving. (English) Zbl 1435.68364
Cerrito, Serenella (ed.) et al., Automated reasoning with analytic tableaux and related methods. 28th international conference, TABLEAUX 2019, London, UK, September 3–5, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11714, 355-373 (2019).
Summary: 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.
For the entire collection see [Zbl 1428.68011].
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B20 Subsystems of classical logic (including intuitionistic logic)
03B35 Mechanization of proofs and logical operations
Full Text: DOI