Long Normal Form Proof Search and Counter-Model Generation

Abstract This paper describes an algorithm of proof search for implicational formula in intuitionistic logic. It is based on a natural deduction style formulation of long normal form of simply typed λ-calculus. The algorithm returns a deduction tree, which becomes a proof if the formula is provable. When the formula is unprovable, a counter-model is constructed by identifying the repeated nodes in the deduction tree. Simplicity of the model construction is due to long normal form. The completeness of the algorithm is proved.