ISIS-1101 FORMAL DEDUCTION TOOLS

A course on Logic. It is peculiar because it uses a special deductive calculus based on equational logic (rewriting and equals-by-equals text replacement). It is important to follow strictly proof formats in order to justify rigorously every deduction step. Additionally, semantics for non-repetitive instructions of an imperative programming language are studied. Sets and integers are studied as applications of the logical approach as specific logical theories. At the end of the course, the student ability to model and specify real situations should be better, especially regarding program specification. He / She should reason, understand, criticize, and develop formal proofs, and verify simple programs (non-repetitive instructions).

Credits

3