Natural deduction with general elimination rules
Natural deduction with general elimination rules
复制标题
具有一般淘汰规则的自然演绎
DOI：
--
复制
发表时间：
2001
影响因子：
0.3
通讯作者：
J. Plato
中科院分区：
文献类型：
--
作者：
J. Plato
通过对自然演绎法中推导的同构分析，揭示了通常自然演绎法中隐含的12种可转换性。给出了类似于析取消去的合取和蕴涵消去规则的一般公式。通过置换转换的规范化现在适用于所有情况。正规形式的推导有所有消去规则的主要前提作为假设。任何顺序的转换终止。
The structure of derivations in natural deduction is analyzed through isomorphism with a suitable sequent calculus, with twelve hidden convertibilities revealed in usual natural deduction. A general formulation of conjunction and implication elimination rules is given, analogous to disjunction elimination. Normalization through permutative conversions now applies in all cases. Derivations in normal form have all major premisses of elimination rules as assumptions. Conversion in any order terminates.