Concurrent inference through dual transformation.

Bittencourt, G

This paper presents two somewhat independent results and sketches a mechanism that could tie these results together to form an automated theorem proving method. The first point is a correct and complete inference method for first-order logic based on the transformation between conjunctive and disjunctive canonical normal forms. This method, although apparently very inefficient, presents interesting properties, such as not presenting external inference rules. The second point is a concurrent algorithm for dual transformation. This algorithm is presented in a general framework that can be specialized to model several formal systems. Finally, based on the representation adopted to define the algorithm, a dual transformation theorem proving method is sketched.Key words: first-order logic, dual transformation, inference, knowledge representation

INFERENCE (Logic); ARTIFICIAL intelligence; INFORMATION theory; ALGORITHMS; FIRST-order logic

Logic Journal of the IGPL, 1998, Vol 6, Issue 6, p795

1367-0751

Academic Journal

10.1093/jigpal/6.6.795