Discrete mathematics Yi li Software school Fudan University April 16, 2013
. . Discrete Mathematics Yi Li Software School Fudan University April 16, 2013 Yi Li (Fudan University) Discrete Mathematics April 16, 2013 1 / 17
Review Atomic tableaux o CST and properties
Review Atomic tableaux CST and properties Yi Li (Fudan University) Discrete Mathematics April 16, 2013 2 / 17
Outline Syntax and semantics Soundness theorem o Completeness theorem
Outline Syntax and semantics Soundness theorem Completeness theorem Yi Li (Fudan University) Discrete Mathematics April 16, 2013 3 / 17
Syntax Semantics Example Give you two Chinese characters“更衣”,What'sit mean o It means change clothes in modern Chinese o It means go to washroom in ancient chinese E xample Give an acronym "iP" what's it mean? o Internet protocol in network o Integer Programming in operation research o Interactive proof in complexity
Syntax & Semantics . Example . . Give you two Chinese characters “更衣”, what’s it mean? It means change clothes in modern Chinese. It means go to washroom in ancient Chinese. . Example . . Give an acronym ”IP”, what’s it mean? Internet Protocol in network. Integer Programming in operation research. Interactive proof in complexity. Yi Li (Fudan University) Discrete Mathematics April 16, 2013 4 / 17
Syntax Semantics ample Give you the following programming segments O in C, printf("Hello World! ) O in Java, system- print("Hello World! " o in C++, cout<<"Hello World! All of them just output Hello World! "on the screen
Syntax & Semantics . Example . . Give you the following programming segments: 1. in C, printf(”Hello World!”); 2. in Java, system.print(”Hello World!”); 3. in C++, cout<<”Hello World!”; All of them just output ”Hello World!” on the screen. Yi Li (Fudan University) Discrete Mathematics April 16, 2013 5 / 17
Syntax Semantics in PL What's syntax? o What's semantic? o What's relationship between them?
Syntax & Semantics in PL What’s syntax? What’s semantic? What’s relationship between them? Yi Li (Fudan University) Discrete Mathematics April 16, 2013 6 / 17
Soundness ample Consider Pierce law (A→B)→A)→A o Give its tableau proof o Give its truth table
Soundness . Example . . Consider Pierce Law ((A → B) → A) → A. Give its tableau proof. Give its truth table. Yi Li (Fudan University) Discrete Mathematics April 16, 2013 7 / 17
Sign Noncontradictory Path ample Given proposition(A→B)→(A→O)→(B→C, there is a truth valuation which make it false Consider the tableau with the root as F(A→B)→(A→C)→(B→O
Sign & Noncontradictory Path . Example . . Given proposition ((A → B) → (A → C)) → (B → C), there is a truth valuation which make it false. Consider the tableau with the root as F ((A → B) → (A → C)) → (B → C) Yi Li (Fudan University) Discrete Mathematics April 16, 2013 8 / 17
Soundness emma If v is a valuation that agrees with the root entry of a given tableau T given as UTn, then t has a path P every entry of which agrees with V
Soundness . Lemma . . If V is a valuation that agrees with the root entry of a given tableau τ given as ∪τn, then τ has a path P every entry of which agrees with V. Yi Li (Fudan University) Discrete Mathematics April 16, 2013 9 / 17
Soundness( Cont Theorem(Soundness) If a is tableau provable, then a is valid, i.e. Fa=Fa
Soundness(Cont.) . Theorem (Soundness) . . If α is tableau provable, then α is valid, i.e. ⊢ α ⇒⊨ α. Yi Li (Fudan University) Discrete Mathematics April 16, 2013 10 / 17