Of course many details of the system had to be left to more specific lectures, but I hope you got the feeling that this is a usable system for doing proof checking for logics of great interest for computer science.
| By the falsum
rule, which is applied in the Absurd tactic, I may close the proof. The
system replies saying that the sub-tree is proved. This also concludes today's
lecture. Of course many details of the system had to be left to more specific lectures, but I hope you got the feeling that this is a usable system for doing proof checking for logics of great interest for computer science. |
|
