Axiomatic constraint systems for proof search modulo theories

TL;DR

This paper introduces an abstract framework for proof search in first-order logic that uses theory-specific constraints instead of substitutions, enabling modular and sound proof procedures across different theories.

Contribution

It provides a sequent calculus with meta-variables for constraints, along with soundness, completeness, and an axiomatisation for theory-specific constraint propagation.

Findings

Framework supports modular proof search over theories

Soundness and completeness proven for the calculus

Component interface for concrete reasoner implementations

Abstract

Goal-directed proof search in first-order logic uses meta-variables to delay the choice of witnesses; substitutions for such variables are produced when closing proof-tree branches, using first-order unification or a theory-specific background reasoner. This paper investigates a generalisation of such mechanisms whereby theory-specific constraints are produced instead of substitutions. In order to design modular proof-search procedures over such mechanisms, we provide a sequent calculus with meta-variables, which manipulates such constraints abstractly. Proving soundness and completeness of the calculus leads to an axiomatisation that identifies the conditions under which abstract constraints can be generated and propagated in the same way unifiers usually are. We then extract from our abstract framework a component interface and a specification for concrete implementations of background reasoners.