自然演绎:一种形式逻辑中的证明系统,用一组直观的推理规则(如“引入/消去”规则)来从前提出发推导结论,常用于命题逻辑与谓词逻辑的证明与教学。(也常译作“自然推演”。)
/ˈnætʃ(ə)rəl dɪˈdʌkʃən/
Natural deduction is a method for proving logical arguments.
自然演绎是一种用来证明逻辑论证的方法。
In the course, we used natural deduction to derive the conclusion from several premises, step by step, using introduction and elimination rules.
在这门课中,我们用自然演绎把几个前提一步步推导出结论,运用了引入规则和消去规则。
natural 来自拉丁语 naturalis(“自然的、符合天性/本性的”),deduction 来自拉丁语 deducere(“引出、推导”)。合在一起的术语 natural deduction 指一种“更贴近人类日常推理习惯”的演绎证明风格;该体系在 20 世纪由逻辑学家 Gerhard Gentzen(根岑) 等人系统化发展。