COSC 410 Assignment.

2 marks for a question from Dr Labuschagne.

2 marks for this question:

    Prove or disprove the following formula using the tableau method:

	( battery-good
	& wires-good
	& motor-good
	& ~ heavy-load
	=> load-moving
	)
	& battery-good
	& wires-good
	& ~ load-moving
	=> (~ motor-good
	   | heavy-load
	   )

    This is an example of a rule that you might have in a fault
    diagnosis program.

6 marks for one of two choices.

  Either

    Prove that the choice of which rule to apply in the tableau
    method has no effect on the correctness of the result, only
    on how long it takes us to get there

  Or

    Write a program to read a formula in elementary set theory,
    and to read an interpretation for the symbols, and to    
    evaluate the formula in that interpretation.

    The program will be run as
	seteval Formula-File Model-File
    or  java SetEvel Formula-File Model-File
    where Formula-File is the name of a file containing one formula,
    and Model-File is the name of a file containing values for all
    the variables in the formula (and perhaps other variables too).

    The syntax has been stripped to the bone to make parsing easy.

	set = capital-letter		set variable
	    | "(" set binary-operator set ")"

	binary-operatory = "+" 		union
	                 | "*"		intersection
	                 | "\"		difference

	test = element ":" set		set membership
	     | element "=" element	element equality
	     | set "=" set		set equality
	     | set "<" set		strict subset
	     
	element = small-letter

	formula = test
	        | "~" formula		not
	        | "[" formula logical-operator formula "]"

	logical-operator = "&"		not
	                 | "|"		or
	                 " ">"		implies

    Within a formula, white space characters are to be ignored.

	model = definition+

	definition = element "=" alphanumeric "\n"
	           | capital-letter "=" alphanumeric* "\n"

    The definitions in a model are in no particular order.
    Letters are just the ASCII a-z (small) and A-Z (capital).