Proof Search and Counter Model of Positive Minimal Predicate Logic

This paper presents an algorithm of proof search for positive formulas in minimal predicate logic. It is based on the LJB deduction system introduced in [Dowek, G. and Y. Jiang, Eigenvariables, bracketing and the decidability of positive minimal predicate logic, Theoretical Computer Science 360 (2006), pp. 193–208]. The algorithm returns a deduction tree, and hence a proof, when the formula is provable, and a counter-model will be constructed when the formula is unprovable. The soundness and the completeness are proved.