>> [CS656/556 Course Materials]
Mon Mar 3 14:43:01 PST 2003
656/556 2003 1w 04 Syntax
Assigned work due
Ex1.6.2b: Prove not(not p or not q) |- p and q using Natural
Deduction (Use book notation or course www site notation).
ch 1.3 ex1.7
wff ::= "well formed formula".
Exercises on parsing and syntax
parse some wffs
How I do syntax and other definitions
wff ::= atom | "(" "not" wff ")" | ..,
How far can BNF stretch?
Then t has type T and P(t) is true.
Definitions and logic.
Then E can substitute for t in any expression or wff.
In effect, the same as t::type(E), t=E.
Exercise on XBNF
Assigned work: Exercise 1e from Ex1.7 on page 43: draw and hand
in parse tree for: p -> (~q \/ (q -> p))
lab: look at
Write your XBNF exercise into a *.mth file
and convert to HTML and look at it.
If time look at paper "How far can EBNF stretch."
next: Holiday on Monday
Class on Wednsday