A system of inference based on proof search: an extended abstract

TL;DR

This paper introduces PSF, a proof search framework that models inference features for various logic systems, aiming to better support proof search processes compared to traditional natural deduction.

Contribution

The paper presents PSF, a novel framework that captures inference features for proof search across multiple logic systems, with formal design and metatheoretical analysis.

Findings

PSF can specify classical, intuitionistic, and linear logic proof systems.

The framework's design aligns with natural reasoning processes.

Metatheory confirms PSF's robustness and flexibility.

Abstract

Gentzen designed his natural deduction proof system to ``come as close as possible to actual reasoning.'' Indeed, natural deduction proofs closely resemble the static structure of logical reasoning in mathematical arguments. However, different features of inference are compelling to capture when one wants to support the process of searching for proofs. PSF (Proof Search Framework) attempts to capture these features naturally and directly. The design and metatheory of PSF are presented, and its ability to specify a range of proof systems for classical, intuitionistic, and linear logic is illustrated.