A Heuristic Proof Procedure for Propositional Logic

TL;DR

This paper introduces a new heuristic called $nongshim$ that enhances invertible proof procedures for propositional logic, leading to a derived invertible sequent calculus that improves theorem proving efficiency.

Contribution

The paper presents a novel heuristic $nongshim$ and demonstrates its application in deriving an invertible sequent calculus for propositional logic.

Findings

$nongshim$ heuristic improves proof search efficiency

Derived invertible sequent calculus enhances theorem proving

Heuristic provides a new underlying principle for invertible procedures

Abstract

Theorem proving is one of the oldest applications which require heuristics to prune the search space. Invertible proof procedures has been the major tool. In this paper, we present a novel and powerful heuristic called $nongshim$ which can be seen as an underlying principle of invertible proof procedures. Using this heuristic, we derive an invertible sequent calculus\cite{Ketonen,Troe} from sequent calculus for propositional logic.