Constraint Learning for Non-confluent Proof Search

TL;DR

An initial constraint learning language for connection-driven search is iteratively refined to greatly reduce backtracking in practice, and may be useful for proof search in other non-confluent tableau calculi.

Abstract

Proof search in non-confluent tableau calculi, such as the connection tableau calculus, suffers from excess backtracking, but simple restrictions on backtracking are incomplete. We adopt constraint learning to reduce backtracking in the classical first-order connection calculus, while retaining completeness. An initial constraint learning language for connection-driven search is iteratively refined to greatly reduce backtracking in practice. The approach may be useful for proof search in other non-confluent tableau calculi.

Figures (2)

• Figure 1: The three inference rules of the clausal connection tableau calculus: start, reduction, and extension. In the start and extension rules, $C = L_1 \vee L_2 \vee \dots \vee L_n$ is a clause from the input set, with its variables renamed apart from the tableau. In the reduction and extension rules we require that $\sigma(\lnot{L}) = \sigma(L_1)$, i.e. $L$ and $L_1$ are connected (shown with dashed lines).
• Figure 2: Running example: a connection tableau built from clauses \ref{['eq:c1']}--\ref{['eq:c7']}.

Theorems & Definitions (7)

• definition 1: Simplified Constraint Language
• definition 2: Reasons for failed inferences
• definition 3: Reasons for stuck tableaux
• lemma 1: Termination
• lemma 2
• theorem 1: Completeness
• definition 4: Refined Constraint Language