Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
423600 | Electronic Notes in Theoretical Computer Science | 2008 | 16 Pages |
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