POL WEB TUTOR
MENU
ABOUT THIS SITE
BUG WEBMASTER
EXAMPLE PROOF
HELP WITH PROOFS
-->[in new window]
MAIN MENU
WEB SITE BY ...
Proof Checker
Enter proof in the box at right
Rule Reminder List
------- Implicational Rules -------
MP: p->q, p :. q
MT: p->q, ~q :. ~p
DS: pvq, ~p :. q or pvq, ~q :. p
Simp: p.q :. p or q
Conj: p, q :. (p.q)
HS: p->q, (q->r) :. (p->r)
Add: p :. pvq or p :. qvp
CD: pvq, p->r, q->s :. rvs
------- Proof Procedures -------
CP: Assume p; get q :. p -> q
RAA: Assume p (or ~p); get q.~q :. ~p (or p)
------- Equivalence Rules -------
DN: p :: ~~p
EX: (p.q)->r :: p->(q->r)
Com: p.q :: q.p or pvq :: qvp
Dist: p.(qvr) :: (p.q)v(p.r)
Dist: pv(q.r) :: (pvq).(pvr)
As: pv(qvr) :: (pvq)vr
As: p.(q.r) :: (p.q).r
Re: p :: p.p or p :: pvp
DeM: ~(p.q) :: ~pv~q or ~(pvq) :: ~p.~q
ME: p<->q :: (p->q).(q->p)
ME: p<->q :: (p.q)v(~p.~q)
Cont: p->q :: ~q->~p
MI: p->q :: ~p v q
------- Quantifier Rules -------
UI: (x)Fx :. Fc
EG: Fc :. ($x)Fx
EI: ($x)Fx :. Fc (restricted)
UG: Fc :. (x)Fx (restricted)
QN (1): ~($x)Fx :: (x)~Fx or ~(x)Fx :: ($x)~Fx
QN (2): ~($x)~Fx :: (x)Fx or ~(x)~Fx :: ($x)Fx
------- Identity Rules --------
LL: x=y, f(x) :. f(y)
ID: :. x=x
SM: x=y :. y=x or ~x=y :. ~y=x
© Logic Pedallers and McGraw-Hill 2012 –
[Program run on 490276.oasistravelhk.tech -- debugging info shown below]
cookie : pageout=; path=/; expires=Wed, 27-Nov-2024 08:38:12 GMT