Strict Standards: Non-static method DB::connect() should not be called statically, assuming \$this from incompatible context in /group/project/aicat/web/lib/database.php on line 32

Strict Standards: Non-static method DB::parseDSN() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB.php on line 520

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB.php on line 557

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /group/project/aicat/web/lib/database.php on line 34

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /group/project/aicat/web/lib/database.php on line 92

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1009

Strict Standards: Non-static method DB::isManip() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 2200

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /group/project/aicat/web/lib/database.php on line 97

Strict Standards: Non-static method DB::connect() should not be called statically, assuming \$this from incompatible context in /group/project/aicat/web/lib/database.php on line 32

Strict Standards: Non-static method DB::parseDSN() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB.php on line 520

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB.php on line 557

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /group/project/aicat/web/lib/database.php on line 34
Catalogue of Artificial Intelligence Techniques

# Catalogue of Artificial Intelligence Techniques

View Maths as: Images | MathML

Strict Standards: Non-static method DB::isManip() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 2200

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1217

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1666

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB.php on line 1387

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1683

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /group/project/aicat/web/lib/database.php on line 113

Strict Standards: Non-static method DB::isManip() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 2200

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1217

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1666

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB.php on line 1387

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1683

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /group/project/aicat/web/lib/database.php on line 113

Strict Standards: Non-static method DB::isManip() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 2200

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1217

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1666

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB.php on line 1387

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1683

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /group/project/aicat/web/lib/database.php on line 113

Strict Standards: Non-static method DB::isManip() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 2200

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1217

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1666

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB.php on line 1387

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1683

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /group/project/aicat/web/lib/database.php on line 113

## 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 $A\to B,B\to C⊢A\to C$

, is represented as the matrix:

$\genfrac{}{}{0}{}{A}{\overline{\underset{}{B}}}\text{}\genfrac{}{}{0}{}{B}{\overline{\underset{}{C}}}\text{}\left(\overline{\underset{}{A}}\text{}C\right)$

where $\overline{\underset{}{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,\overline{\underset{}{C}},\overline{\underset{}{A}}$ is one path, $A,\overline{\underset{}{C}},C$ another. $A,\overline{\underset{}{A}}$ and $C,\overline{\underset{}{C}}$ are connections on these paths. The basic characterisation of consequence (or validity) on which the connection calculus rests is that an entailment $\Gamma ⊢A$ holds (i.e., $A$ is a logical consequence of the formulae of $\Gamma$ ) 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,\overline{\underset{}{A}}$ ,$B,\overline{\underset{}{B}}$

and $C,\overline{\underset{}{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:

Strict Standards: Non-static method DB::isManip() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 2200

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1217

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1666

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB.php on line 1387

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1683

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /group/project/aicat/web/lib/database.php on line 113

• Wallen, L.A., Automated proof search in non-classical logics , MIT Press, Cambridge, Mass. and London, 1990.

Strict Standards: Non-static method DB::isManip() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 2200

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1217

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1666

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB.php on line 1387

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /usr/share/pear/DB/common.php on line 1683

Strict Standards: Non-static method DB::isError() should not be called statically, assuming \$this from incompatible context in /group/project/aicat/web/lib/database.php on line 113