Catalogue of Artificial Intelligence Techniques

   

Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML

Connection Calculus

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 AB,BCAC

, is represented as the matrix:

AB¯ BC¯ (A¯ C)

where A¯ indicates that the occurrence of A 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, A,C¯,A¯ is one path, A,C¯,C another. A,A¯ and C,C¯ are connections on these paths. The basic characterisation of consequence (or validity) on which the connection calculus rests is that an entailment ΓA holds (i.e., A 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 A,A¯ ,B,B¯

and C,C¯ 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).


References:


Comments:

Add Comment

No comments.