A Heuristic Proof Procedure for First-Order Logic

Keehang KWON  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E103-D   No.3   pp.549-552
Publication Date: 2020/03/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.2019FCL0003
Type of Manuscript: Special Section LETTER (Special Section on Foundations of Computer Science — Frontiers of Theory of Computation and Algorithm —)
Category: 
Keyword: 
proof procedures,  heuristics,  game semantics,  classical logic,  

Full Text: PDF(73.4KB)>>
Buy this Article




Summary: 
Inspired by the efficient proof procedures discussed in Computability logic [3],[5],[6], we describe a heuristic proof procedure for first-order logic. This is a variant of Gentzen sequent system [2] 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.