Discrete mathematics Yi Li Software school Fudan universit June4,2013
. . Discrete Mathematics Yi Li Software School Fudan University June 4, 2013 Yi Li (Fudan University) Discrete Mathematics June 4, 2013 1 / 17
Review o Tableau proof o Complete systematic tableaux
Review Tableau Proof Complete Systematic Tableaux Yi Li (Fudan University) Discrete Mathematics June 4, 2013 2 / 17
utline o Soundness Completeness o Compactness
Outline Soundness Completeness Compactness Yi Li (Fudan University) Discrete Mathematics June 4, 2013 3 / 17
Tableau proof amp dle Consider a sentence GyR(, y)v P(, y))A(VXR(x,x). There is a model A
Tableau Proof . Example . . Consider a sentence (∃y)(¬R(y, y) ∨ P(y, y)) ∧ (∀x)R(x, x). There is a model A. Yi Li (Fudan University) Discrete Mathematics June 4, 2013 4 / 17
Soundness emma If T= UTn is a tableau from a set of sentences s with root Fa, then any L-structure A that is a model of SUnna can be extended to one agreeing with every entry on some path P through T. Recall that A agrees with Ta(Fa) if a is true(false) in A Theorem(Soundness) If there is a tableau proof r of a from S, then Sa
Soundness . Lemma . . If τ = ∪τn is a tableau from a set of sentences S with root Fα, then any L-structure A that is a model of S ∪ {¬α} can be extended to one agreeing with every entry on some path P through τ .( Recall that A agrees with Tα(Fα) if α is true(false) in A.) . Theorem (Soundness) . . If there is a tableau proof τ of α from S, then S |= α. Yi Li (Fudan University) Discrete Mathematics June 4, 2013 5 / 17