Constraint Learning for Non-confluent Proof Search

TL;DR

This paper introduces a constraint learning approach to reduce backtracking in non-confluent tableau proof search, maintaining completeness and improving efficiency in classical first-order logic.

Contribution

It presents a novel constraint learning method that effectively minimizes backtracking in non-confluent tableau calculi without losing completeness.

Findings

Significant reduction in backtracking observed in experiments.

Constraint learning approach maintains proof search completeness.

Potential applicability to 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.