《 deduction proof system imps home page自然演绎证明系统小鬼主页课件》由会员分享，可在线阅读，更多相关《 deduction proof system imps home page自然演绎证明系统小鬼主页课件（12页珍藏版）》请在金锄头文库上搜索。
1、Natural Deduction System for First Order Logic,Student: Wei Lei Instructor: W. M. Farmer Department of Computing and Software McMaster University, Hamilton, CA,Contents,Natural Deduction Natural Deduction Proof Rules of First Order logic Axioms of Natural Deduction System Reference,Natural Deduction
2、,Natural deduction was invented by G. Gentzen in 1934. The idea was to have a system of derivation rules that as closely as possible reflect the logical steps in an informal rigorous proof. For each connective there is an introduction rule (except conjunction, which has two) which can be seen as a d
3、efinition of which conditions must be satisfied for the proposition to be true. Natural Deduction tries to follow the natural style of reasoning. Most of the proof consists of forward reasoning, i.e. deriving conclusions, deriving new conclusions from these conclusions, etc. Occasionally hypotheses
4、are introduced or dropped.A derivation is a tree where the nodes are the rules and the leafs are the assumptions of the derivation. The root of the tree is the conclusion of the derivation. An assumption may be discharged by a rule in the derivation; that an assumption A is discharged in a derivatio
5、n is denoted by A.,Natural Deduction Proof,Definition. A natural deduction proof is a finite tree whose leaves are formula (over the alphabet ,) and which is built by using the rules.Example: p q, r |= p rProof: p qep rip r,Rules of First Order logic,If we have a derivation of B from the assumption
6、A, we may derive AB and discharge the assumption A:A I BA BGiven derivations of A B and A, we can conclude B:A B A E BFor conjunction, the introduction rule tells us that if we have derivations of Aand B, then we can conclude A B:A B I A B,Rules of First Order logic,There are two elimination rules f
7、or conjunction: A BE1 AA B E2 B We can infer a disjunction if we know one of the disjuncts. Hence there are two introduction rules for the disjunction:A V I1 A V BB V I2 A V B,Rules of First Order logic,The elimination rule for disjunction is slightly more complicated to formulate. We must make use
8、of the fact that we know AVB but not necessarily which of A and B it is that holds.A B A V B C CVE C Rules for :A A A I E A ,Rules of First Order logic,Rules for :A B A BE1 E2 AB BAABBAI A B Rules for :A AA B E BB I A B,Rules of First Order logic,Rules for :x: X P(x) x is a new object of type XE Px:
9、=t P(X) I x: X P(x)The notation Px := t means intelligent replacement.Also we have rules for equality: Equality reflexivity Equality replacement,Axioms of Natural Deduction System,Example of an axiomatic system of natural deduction Name Of System: AS Let A,B denote statements. Undefined terms: , Axi
10、om(conjunction C): A,B; therefore A B Axiom(simplification1 S1): A B; therefore A Axiom(simplification2 S2): A B; therefore B Axiom(double negation1 DN1): ( A); therefore A Axiom(double negation2 DN2): A; therefore ( A) Axiom(Conjunctive Syllogism CS): A,(A B); therefore B Definition: A V B = ( A B)
11、 Definition: If A then B = (A B) Definition: A if only if B = (if A then B) (if B then A)Notice that the axioms were not framed using any of the definitions.,Axioms of Natural Deduction System,Whether or not AS is complete.That is, the question as to whether or not AS contains enough axioms in order
12、 for a reasoning agent to figure out all possible natural deductions (memory limitations aside), can be raised. If the answer is yes, then the system is said to be complete. It turns out that AS is complete, but proving so is rather difficult.,Reference,i John M. Anderson and Henry W.Johnstone, Jr.
13、Natural Deduction, The Logical Basis of Axiom Systems. Wadsworth publishing company, inc. Belmont, California:1962ii Dirk van Dalen. Logic and Structure. Third Edition. Springer-Verlag Berlin Heidelberg, New York:1997iii Hans de Nivelle. Natural Deduction for First-Order Logic. vi BrainyEncyclopedia Natural deduction,
