Dissolution

Publisher Website
Google Scholar
Abstract
Path dissolution, a rule of inference that operates on formulas in negation normal form and that employs a representation called semantic graphs is introduced. Path dissolution has several advantages in comparison wdh many other reference technologies. In the ground case, lt preserves equivalence and is strongly complete: Any sequence of dissolution steps applied exhaustively to a semantic grdph G will yield an equivalent linkless graph G. Furthermore, one need not (and cannot) restrict attention to conjunctive normal form (CNF) when employing dlssolutlon: A single application (even to a CNF formula) generally produces a non-CNF formula that is more compact than any of its CNF equivalents. Path dissolution is a global rule: as such, it is employed at the first order level differently from the way locally oriented techmques (such as resolution) are. Two methods for employing dissolution as an inference mechanism for first order logic are presented. Dissolution is related to our theory links mechanism, to the factoring of formulas with the distributive laws. and to analytic tableaux. Some preliminary experimental results are also reported.

This publication has 9 references indexed in Scilit: