论文标题
命题逻辑的启发式证明程序
A Heuristic Proof Procedure for Propositional Logic
论文作者
论文摘要
定理证明是最古老的应用程序之一，需要启发式方法才能修剪搜索空间。可逆的证明程序一直是主要工具。在本文中，我们提出了一种名为$ nongshim $的小说且强大的启发式方法，可以看作是可逆性证明程序的基本原则。使用这种启发式，我们从命题逻辑中得出了可逆的序列cculus \ cite {ketonen，troe}。
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.
