Catalogue of Artificial Intelligence Techniques
Categories: Inference and Reasoning
Author(s): Dave Plummer
Natural deduction is a formal inference system which is said naturally to mirror the way in which humans reason. A natural deduction system consists of rules of inference eliminating and introducing each of the connectives and quantifiers of the Predicate Calculus. There are twelve rules which may be used to infer conclusions. Two examples of such rules are given below:
connective and that on the right to introduce it. Proofs are trees, the leaves representing the assumptions, and the root, the conclusion that has been deduced from those assumptions. In natural deduction we can assume temporarily certain formulae, and then `discharge' them later in the proof, using certain of the deduction rules. The
introduction rule above is an example of a rule discharging an assumption ( in this case). Natural deduction is sound and complete.
- Tennant, N., Natural Logic
, Edinburgh University Press, Edinburgh, 1978, reprinted with corrections, 1990