|
|
|
The
characteristics soundness and completeness of the program were proved by
establishing a series of lemmas. These lemmas use reasoning on a graph as
proof mechanism. I refer to my master thesis for more detail of these lemmas.
|
|
Besides giving a
proof of the soundness and completeness of the program, I was able to deduce
from this theory:
|
|
• an elegant proof of the found solutions (shown
in the demo)
|
|
• under certain conditions it is possible to
deduce a general rule (= procedure)
from a solution and its proof (shown in the demo).
|