Article ID Journal Published Year Pages File Type
423600 Electronic Notes in Theoretical Computer Science 2008 16 Pages PDF
Abstract

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.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics