A Heuristic Proof Procedure for First-Order Logic

TL;DR

This paper introduces a game-inspired heuristic proof procedure for first-order logic, based on a variant of Gentzen sequent calculus, emphasizing proof strategies as winning games and offering a new deductive system with proven soundness and completeness.

Contribution

It presents a novel game-based heuristic proof system for first-order logic, including a new deductive system LKg and its optimized variant LKg', with formal proofs of soundness and completeness.

Findings

LKg is sound and complete for first-order logic.

The game-based approach enables more deterministic proof search.

LKg' offers optimizations improving proof efficiency.

Abstract

Inspired by the efficient proof procedures discussed in {\em Computability logic} \cite{Jap03,Japic,Japfin}, we describe a heuristic proof procedure for first-order logic. This is a variant of Gentzen sequent system and has the following features: (a)~ it views sequents as games between the machine and the environment, and (b)~ it views proofs as a winning strategy of the machine. From this game-based viewpoint, a poweful heuristic can be extracted and a fair degree of determinism in proof search can be obtained. This article proposes a new deductive system LKg with respect to first-order logic and proves its soundness and completeness. We also discuss LKg', a variant of LKg with some optimizations added.