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
Key terms
	wff  ::= "well formed formula".
	tree
	subformula
	priorities
Questions?

Exercises on parsing and syntax
	parse some wffs
	
How I do syntax and other definitions
      XBNF handout 
	wff  ::= atom   |  "(" "not" wff ")"  |  ..,
How far can  BNF stretch?
	Syntax.
		t::=E.
	Abreviations.
		t::=a_long_descriptive_name.
	Descriptions.
		t::T,  P(t). 
			 Then t has type T and P(t) is true.
	Definitions and logic.
		t::=E. 
			Then E can substitute for t in any expression or wff.
			In effect, the same as t::type(E), t=E.


Exercise on XBNF
	http://www.csci.csusb.edu/dick/cs656/train.html

Assigned work:  Exercise 1e from Ex1.7 on page 43: draw and hand
	in parse tree for: p -> (~q \/ (q -> p))
	
lab: look at
	http://www.csci.csusb.edu/dick/maths/intro_ebnf.html
  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."
	http://www.csci.csusb.edu/dick/papers/rjb96x.xbnf.html

next: Holiday on Monday
	Class on Wednsday
	    Semantics

http://www.csci.csusb.edu/dick/cs656/class/05.html