Clausal intuitionistic logic II. tableau proof procedures

AbstractClausal intuitionistic logic is an extension of Horn-clause logic which permits the appearance of negations and embedded implications on the right-hand side of a rule, and interprets these new rules intuitionistically in a set of partial models. In this article the second of a pair, clausal intuitionistic logic, is shown to have a tableau proof procedure that generalizes Horn-clause refutation proofs. The proof procedures are explained by means of several detailed examples. Soundness and completeness theorems are stated and proven in full detail