Neil V. Murray

TCS Journal 2004 Journal Article

Linearity and regularity with negation normal form

• Reiner Hähnle
• Neil V. Murray
• Erik Rosenthal

Proving completeness of NC-resolution under a linear restriction has been elusive; it is proved here for formulas in negation normal form. The proof uses a generalization of the Anderson–Bledsoe excess literal argument, which was developed for resolution. That result is extended to NC-resolution with partial replacement. A simple proof of the completeness of regular, connected tableaux for formulas in conjunctive normal form is also presented. These techniques are then used to establish the completeness of regular, connected tableaux for formulas in negation normal form.

KER Journal 1997 Journal Article

Logical methods for computational intelligence

• Grigoris Antoniou
• Neil V. Murray

Over the past years, two main approaches to computational intelligence have emerged: the symbolic and the non-symbolic approach. The perhaps most prominent methods of the symbolic approach are based on logic. Logical methods exhibit a series of desirable properties: [bull ] Transparent representation of meaning [bull ] Precise understanding of the meaning of statements (semantics). [bull ] Sound reasoning methods. [bull ] Explanation capabilities. A special session on logical methods for computational intelligence was held at the 3rd Joint Conference on Information Sciences. The field of computational logic is so broad that it is impossible to review the main developments in an article. Therefore, in the following we will restrict attention to two areas that turned out to be the focus of the special session: automated reasoning, and reasoning with incomplete and changing information.

LPAR Conference 1994 Conference Paper

On Anti-Links

• Bernhard Beckert
• Reiner Hähnle
• Anavai Ramesh
• Neil V. Murray

Abstract The concept of anti-link is defined, and useful equivalence-preserving operations on propositional formulas based on anti-links are introduced. These operations eliminate a potentially large number of subsumed paths in a negation normal form formula. The operations have linear time complexity in the size of that part of the formula containing the anti-link. These operations are useful for prime implicant/implicate algorithms because most of the computational effort in such algorithms is spent on subsumption checks.

TCS Journal 1994 Journal Article

On the relative merits of path dissolution and the method of analytic tableaux

• Neil V. Murray
• Erik Rosenthal

Path dissolution is an inferencing mechanism that generalizes the method of analytic tableaux. We present several results demonstrating that tableau deductions can be substantially speeded up with applications of dissolution technology. We also consider the class of formulas on which the method of analytic tableaux was first shown to be intractable and prove that, with the application of the ordinary distributive law, standard tableau methods admit linear time proofs for this class.

LPAR Conference 1993 Conference Paper

Non-Clausal Deductive Techniques for Computing Prime Implicants and Prime Implicates

• Anavai Ramesh
• Neil V. Murray

Abstract Several methods to compute the prime implicants and the prime implicates of a negation normal form (NNF) formula are developed and implemented. An algorithm PI is introduced that is an extension to negation normal form of an algorithm given by Jackson and Pais. The PI algorithm alone is sufficient in a computational sense. However, it can be combined with path dissolution, and it is shown empirically that this is often an advantage. None of these variations rely on conjunctive normal form or on disjunctive normal form. A class of formulas is described for which reliance on CNF or on DNF results in an exponential increase in the time required to compute prime implicants/implicates. The possibility of avoiding this problem with efficient structure preserving clause form translations is examined briefly and appears unfavorable.

IJCAI Conference 1989 Conference Paper

The Logic of Time Structures: Temporal and Nonmonotonic Features

• Mira Balaban
• Neil V. Murray

AAAI Conference 1987 Conference Paper

Path Dissolution: A Strongly Complete Rule of Inference

• Neil V. Murray

We introduce path dissolution, a rule of inference that operates on formulas in negation normal form. Path dissolution is strongly complete; i.e., it has the property that, given an unsatisfiable ground formula, any sequence of dissolution steps will produce the empty graph. This is accomplished by strictly reducing (at each step) the number of c-paths in the formula. Dissolution, unlike most resolution-based inference rules, does not directly lift into first-order logic; techniques for employing dissolution at the first order level are discussed.

IJCAI Conference 1985 Conference Paper

Path Resolution with Link Deletion

• Neil V. Murray
• Erik Rosenthal

AIJ Journal 1982 Journal Article

Completely non-clausal theorem proving

• Neil V. Murray

The proof procedure we describe operates on quantifier-free formulas of the predicate calculus which are not truth-functionally normalized in any way. The procedure involves a single inference rule called NC-resolution, and is shown to be complete. Completeness is also obtained for a simple restriction on the rule's application. Examples are given using NC-resolution to derive a logic program from its specification, and to ‘execute’ a program specification in its original form.