×

NDK and natural reasoning. (English) Zbl 0990.03043

Chong, C. T. (ed.) et al., Proceedings of the 6th Asian logic conference, Beijing, China, May 20-24, 1996. Singapore: World Scientific. 285-309 (1998).
Summary: We study a revised version of NDK, a system of first-order predicate calculus formulated as a system of natural deduction where the rule of inference can be applied to any disjunctive component. NDK thus does not have axioms. NDK deductions are simpler than NK ones in many cases. Various features of classical proofs are investigated by taking the advantage of the formulation of NDK. The major result is a conversion algorithm of NDK deductions to NK-type deductions, which are regarded as more natural, preserving the logical structures.
For the entire collection see [Zbl 0970.00012].

MSC:

03F07 Structure of proofs
03B10 Classical first-order logic
PDFBibTeX XMLCite