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).