Catalogue of Artificial Intelligence Techniques
Aliases: Clause Graph Resolution, Connection Graph
Keywords: conjunctive normal form, connection calculus, disjunctive normal form, literals, path-checking, refutation
Categories: Theorem Proving
Author(s): Lincoln Wallen
The connection calculus is a proof system for first-order classical Predicate Calculus based on the notion of a matrix. The method is due to Wolfgang Bibel (1981) and grew out of an analysis of more standard sequent and tableau methods. A similar method of `matings' was developed independently by Peter Andrews in 1981. A formula or entailment of the first-order predicate calculus can be displayed as a (nested) two-dimensional matrix. For example, the entailment
, is represented as the matrix:
where indicates that the occurrence of is negative, i.e., inside an odd number of explicit or implicit negation signs. The matrix is made up of three columns, the first two of which themselves are matrices with one column and two rows. The third matrix has two columns and one row. Ignoring the brackets and reading horizontal separation as conjunction and vertical separation as disjunction we have the conjunctive normal form of the original entailment. (We could just as easily work with the disjunctive normal form by attempting to refute the entailment rather than prove it.) The paths through this matrix are lists of literals that contain exactly one element from each column of the matrix, and a connection is a pair of literals on a path that are complementary (i.e., identical atoms but complements with respect to negation). In our example, is one path, another. and are connections on these paths. The basic characterisation of consequence (or validity) on which the connection calculus rests is that an entailment holds (i.e., is a logical consequence of the formulae of ) if and only if every path through the matrix representation of the entailment contains a complementary connection. This is a version of Gentzen's Hauptsatz for the logic. In our example, the connections ,
and are said to span the matrix because every path through it contains a connection from this (three element) set of connections. The entailment therefore holds. Various so-called path-checking algorithms have been designed that simulate resolution strategies, and to take extra advantage of the form of the matrix (see Bibel 1982). In the presence of quantifiers complementarity of connections is calculated by a unification algorithm as in standard . The method extends to classical type theory (see Andrews' work) and non-classical logics (Wallen's 1990 book).
- Wallen, L.A., Automated proof search in non-classical logics
, MIT Press, Cambridge, Mass. and London, 1990.