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.

翻译：根岑设计其自然演绎证明系统旨在“尽可能贴近实际推理”。确实，自然演绎证明与数学论证中逻辑推理的静态结构高度相似。然而，当需要支持证明搜索过程时，推理的不同特征就显得至关重要。PSF（证明搜索框架）试图自然且直接地捕捉这些特征。本文阐述了PSF的设计与元理论，并展示了其指定经典逻辑、直觉主义逻辑和线性逻辑中多种证明系统的能力。