Homework 1
Objectives
Objectives
Starting file
“Success is the ability to go from one failure to another with no loss of enthusiasm.” Winston Churchill
Objectives Write some ACL2s functions against given requirements Practice using and understanding ACL2s’ contract system Form groups and working rela...
Induction makes you feel guilty for getting something out of nothing … but it is one of the greatest ideas of civilization. – Herbert Wilf
To prove a thing is not enough; you have to seduce people to accept it. – Friedrich Nietzsche
“Contrariwise,’ continued Tweedledee, ‘if it was so, it might be; and if it were so, it would be; but as it isn’t, it ain’t. That’s logic.” –Lewis Carroll...
It is reasonable to hope that the relationship between computation and logic in the next century will be as fruitful as that between calculus and physics ...
[Proofs] are this crazy contact between an imaginary, nonphysical world and biologically evolved creatures. We did not evolve to do this. – Simon DeDeo
– Randall Munroe, xkcd