The Isabelle/Isar Reference Manual says in Section 12.5 that “`iprover`

performs intuitionistic proof search”. What exactly is meant by “intuitionistic proof search” here? Is it what is described in the paper *Proof Search in the Intuitionistic Sequent Calculus* by Natarajan Shankar or something else? I’m asking, since I want to know what class of problems `iprover`

can solve in a certain application context of mine.

Last updated: Aug 15 2022 at 04:16 UTC