Stream: General

Topic: Intuitionistic proof search


view this post on Zulip 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: Aug 15 2022 at 04:16 UTC