Wolfgang Jeltsch (Jan 14 2022 at 19:12): Wolfgang Jeltsch (Jan 14 2022 at 19:12):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: Dec 21 2024 at 12:33 UTC