The prime implicate trie (pi-trie) of a logical formula is a tree whose branches are labelled with the prime implicates of the formula.An algorithm that builds the pi-trie from a logical formula was introduced in [15]; it builds the trie recursively and makes extensive use of subsumption testing.A more efficient version in which the use of subsumption is reduced is presented in this article.The improved algorithm is illustrated with experiments.The algorithm naturally lends itself to selecting restricted sets-e.g.only positive prime implicates or only those of bounded length, both useful properties for some applications.Such restrictions can provide significant advantages in efficiency since the set of all prime implicates of a logical formula is typically exponential in size.

The reduced implicate trie is a data structure that was introduced in [12] as a target language for knowledge compilation. It has the property that, even when large, it guarantees that a query can be processed in time linear in the size of the query, regardless of the size of the compiled knowledge base. In this paper, the branches of a reduced implicate trie that correspond to prime implicates are characterized. A technique is developed for finding and marking nodes for which all descending branches correspond to non-prime implicates. This is extended to allow the discovery of prime implicate subsets of queries with a "yes" answer.

The reduced implicate trie, introduced in Murray and Rosenthal (2005, Vol. 3702 of Lecture Notes in Artifical Intelligence, pp. 231–244), is a data structure that may be used as a target language for knowledge compilation. It has the property that, even when large, it guarantees fast response to queries. Specifically, a query can be processed in time linear in the size of the query regardless of the size of the compiled knowledge base. The knowledge compilation paradigm typically assumes that the ‘intractable part’ of the processing be done once, during compilation. This assumption could render updating the knowledge base infeasible if recompilation is required. The ability to install updates without recompilation may therefore considerably widen applicability. In this article, several update operations not requiring recompilation are developed. These include disjunction, substitution of truth constants, conjunction with unit clauses, reordering of variables and conjunction with arbitrary clauses.

We consider means for adapting classical deduction techniques to multiple-valued logics. Some recent work in this area, including our own, utilizes signs (subsets of the set of truth values). In this paper we develop a language of signed formulas tha

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.

We consider the class of formulas on which the method of analytic tableaux was first shown to be intractable, and we show that with applications of the ordinary distributive law tableau methods admit linear time proofs for this class.

Path dissolution is an inferencing mechanism that generalizes the method of analytic tableaux. The main result presented is that every non-trivial step in any tableau proof can be speeded up with the application of dissolution techniques.

A graphical representation of quantifier-free predicate calculus formulas in negation normal form and a new rule of inference that employs this representation are introduced. The new rule, path resolution , is an amalgamation of resolution and Prawitz analysis. The goal in the design of path resolution is to retain some of the advantages of both Prawitz analysis and resolution methods, and yet to avoid to some extent their disadvantages. Path resolution allows Prawitz analysis of an arbitrary subgraph of the graph representing a formula. If such a subgraph is not large enough to demonstrate a contradiction, a path resolvent of the subgraph may be generated with respect to the entire graph. This generalizes the notions of large inference present in hyperresolution, clash-resolution, NC-resolution, and UR-resolution. A class of subgraphs is described for which deletion of some of the links resolved upon preserves the spanning property.