Catalogue of Artificial Intelligence Techniques


Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML

Natural Deduction

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:


& & AB

& B





The rule on the left is that to eliminate the

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 (A in this case). Natural deduction is sound and complete.



Add Comment

No comments.