Appendex 4 A List of Inference Rules and Their Utility Examples

Page 1

LIST OF INFERENCE RULES

1. FOR PROPOSITIONAL LOGIC ........ LOGIC

2. FOR PREDICATIVE LOGIC .......... ALS,EXIST,ALIM EXIM,ARRN,FLW,ORD, DMOR,CNST,(FUNF)

3. FOR EQUALITY ......... EQ,(EQPT)

4. FOR SUBSTITUTION ......... SUBST,EQPT,FUNF

EXAMPLES

---LOGIC---

a1: A or B by .....

a2: not A by .....

a3: B imp C by .....

-----------------------------

a4: C by LOGIC(a1,a2,a3);

a1: A or not A by LOGIC;

---ALS---

a1: (All x)(f(x)) by .....

-----------------------------

a2: f(a) by ALS(a1);

a1: (All x)(All y)(f(x,y)and y(a)) by .....

----------------------------------------------

a2: f([c=d],B(k))and B(k)(a) by ALS(a1);

a1: (All x)(All y)(u(x,y)) by .....

-------------------------------------

a2: u((All y)(t(y)),True) by ALS(a1);

a1: (All x)(f(x) imp g(x)) by .....

a2: f(a) by .....

--------------------------------------

a3: g(a) by ALS(a1,a2);

a1: (All x)(All y)(k and b(x,y) imp s(x,y)) by .....

a2: k and b(t(u)),m) by .....

------------------------------------------------------

a3: s(t(u),m) by ALS(a1,a2);

---EXIST----

a1: f(a) by .....

-------------------

a2: (Exist x)(f(x)) by EXIST(a1);

a1: f([c=d],B(k))and B(k)(a) by .....

----------------------------------------

a2: (Exist x)(Exist y)(f(x,y)and y(a)) by EXIST(a1);