Intuitionistic Socratic procedures
Tomasz Skura · Journal of Applied Non-Classical Logics · 2005
In the paper we study the method of Socratic proofs in the intuitionistic propositional logic as a reduction procedure. Our approach consists in constructing for a given sequent α a finite tree of sets of sequents by using invertible reduction rules of the kind: Δ is valid if and only if Δ1 is valid or... or Δn is valid. From such a tree either a Gentzen-style proof of α or an Aristotle-style refutation of α can also be extracted.