Connection Method

Origin. Wolfgang Bibel, "On Matrices with Connections" (Journal of the ACM 28(4), 1981, 633–645), with the book-length development in Automated Theorem Proving (Vieweg, Wiesbaden 1982; second edition 1987); independently Peter B. Andrews, "Refutations by Matings" (IEEE Transactions on Computers C-25, 1976, 801–807) and "Theorem Proving via General Matings" (Journal of the ACM 28(2), 1981, 193–214), where the method is stated for arbitrary sentences rather than normal forms. Elmar Eder, Relative Complexities of First Order Calculi (Vieweg, 1992), is the systematic comparison of the method with resolution and the sequent-based calculi. Jens Otten and Bibel's leanCoP ("leanCoP: lean connection-based theorem proving", Journal of Symbolic Computation 36, 2003, 139–161) made the calculus the basis of a family of compact provers.

Models. A proof is a set of connections, not a derivation. The formula is laid out as a matrix — clauses in one dimension, their literals in the other — and validity is a property of the paths through it: the formula is proved when every path contains a connection, a pair of complementary literals, from one spanning set. Where resolution saturates a clause set under an inference rule and tableaux grow a tree, the connection method checks a global condition on a fixed structure, and its search is goal-directed: each step extends the current path along a new connection. Andrews's general matings state the same condition on the structure of an arbitrary sentence, so no clausal, prenex, or other normal form is needed in principle, and Otten's non-clausal calculus (nanoCoP) keeps that generality in practice. A spanning mating is the information a closed tableau distributes across its branches: which literal pairs close them.

Formalism.

Matrix: a set of clauses displayed two-dimensionally; for a clausal formula, one clause per column. Non-clausal matrices nest: a matrix entry may itself be a matrix (Andrews 1981; Otten's non-clausal calculus).

Path: a set of literals containing exactly one literal from each clause. A matrix of n clauses with k literals each has kⁿ paths.

Connection: a pair {A, ¬A} of literals with the same predicate and opposite polarity, taken from different clauses.

Path condition (propositional): A clause set is unsatisfiable iff every path through its matrix contains a complementary connection. A set of connections is spanning iff every path contains at least one of its connections. Proof = a spanning set of connections; Andrews's term is a mating.

First-order case: Skolemization; clause copies (multiplicities μ) for quantifier duplication; a single substitution σ applied to the whole matrix. Path condition: some multiplicity and some σ make every path contain a connection complementary under σ. σ is computed by unification of the connected literals, simultaneously for all connections of the spanning set (rigid variables; see Unification.md). Andrews (1981): duplication may be restricted to outermost quantifiers without losing completeness.

Connection calculus (the search procedure): Start with a clause; extension steps connect an open literal to a literal in a new clause copy; reduction steps connect it to a literal on the current path. Clausal connection proofs are closed connection tableaux: clausal tableaux in which every attached clause contains a literal complementary to the literal it extends (see Tableaux.md). Iterative deepening over multiplicities gives completeness; backtracking over connection choices is the search cost (Otten, "Restricting Backtracking in Connection Calculi", AI Communications 23, 2010, 159–182).

Provers: leanCoP: the clausal calculus in a Prolog core of 333 bytes (v1.0) / 555 bytes (v2.0). ileanCoP (intuitionistic), MleanCoP (modal), nanoCoP (non-clausal; IJCAR 2016).

Symbols.

Metatheory. Bibel (1981) proved the characterization for clausal first-order matrices: a clause set is unsatisfiable iff for some multiplicity there is a spanning set of connections simultaneously complementary under one substitution. Andrews (1981) proved the corresponding theorem for general matings of arbitrary sentences, from a version of Herbrand's theorem, with the sharpening that quantifier duplication can be confined to outermost quantifiers. At the propositional level the path condition is a decision procedure; at first order the method is a semi-decision procedure, like every complete calculus for first-order validity. The clausal connection calculus coincides with connection tableaux and thereby with Loveland's model elimination ("Mechanical Theorem-Proving by Model Elimination", Journal of the ACM 15(2), 1968, 236–251), the identification worked out in Letz and Stenz, "Model Elimination and Connection Tableau Procedures" (Handbook of Automated Reasoning, Elsevier 2001, 2015–2114); Eder (1992) locates the method among resolution and the sequent calculi by simulation (see Resolution.md). Connection proofs, being cut-free and connected, can be forced to repeat subproofs, and Letz, Mayr and Goller ("Controlled integration of the cut rule into connection tableau calculi", Journal of Automated Reasoning 13, 1994, 297–337) reintroduced cut in controlled form to shorten them. Wallen (Automated Deduction in Nonclassical Logics, MIT Press 1990) extended the matrix characterization to intuitionistic and modal logics by adding prefix unification, which is what ileanCoP and MleanCoP implement.

Applies to. Automated theorem proving for classical first-order logic: the leanCoP family. Intuitionistic and modal theorem proving through Wallen's matrix characterizations. Machine-learned proof guidance, where the calculus's small state — a path, a substitution, a set of connections — made leanCoP the base of the learning-guided provers (plCoP: Zombori, Urban and Brown, 2020). Higher-order theorem proving, through matings in TPS (Andrews, Bishop, Issar, Nesmith, Pfenning and Xi, Journal of Automated Reasoning 16, 1996, 321–353).

Limitations. The substitution is rigid: one σ must close every connection at once, so a choice that closes one path can block another, and the search backtracks over unifications where resolution would simply keep both resolvents. Multiplicities are not known in advance — how many copies of each clause suffice is not computable — so completeness is reached by iterative deepening, and the calculus itself gives no bound. The number of paths is exponential in the number of clauses, and the spanning condition quantifies over all of them. Connectedness and cut-freeness together force repeated subderivations: a lemma used on two paths is proved twice unless cut is restored in the controlled form of Letz, Mayr and Goller. Equality has no native treatment, exactly as in resolution and tableaux: the axioms must be added or the calculus extended. And at first order a failed attempt returns no countermodel, since failure at a given multiplicity bounds nothing; only the propositional case reads an open path as a falsifying assignment.

© 2026 Lingenic LLC