No label defined (Q4934559)

The tableau calculus is a handy tool for classical propositional logic: the calculus produces, out of a given sequent, either its formal proof, or its refutation tree which exhibits a counter model. For intuitionistic logic, the usual calculus does not produce a counter model out of a non-proof. The author presents a new calculus, \(\text{TJ}^m\), and shows that it does. \(\text{TJ}^m\) has, besides the usual implication \(\to\), a new \(@> * >>\), and has a little unusual rules about them. Out of a non-proof, a *refutation tree is defined, a logic program is produced, and a new semantics is defined. After further elaborate modification, a connection with Kripke semantics is established. The author's proof and explanations are meticulous and ponderous. For the entire collection see [Zbl 0919.00040].