Why is automated reasoning necessary?
Proofs can be long and (especially in areas like formal methods)
contain many routine and straight forward steps. It is therefore
desirable and practical to automate a large part of their construction.
Only a small fraction of users are able or willing to find proofs.
Finding proofs is often difficult and tedious. It is therefore useful
if computers can take on this task for us.
Finally, all of us are prone to make mistakes. In safety and security
critical systems, we may not be willing to tolerate such errors.
Computer assisted tools can increase our confidence in the correctness
of the systems.
Sponsored by:
