Semantics and Program Correctness

Course outline

Specialized concepts and techniques of First-Order Logic, emphasizing precise mathematical descriptions of concepts and applications thereof. Examination of the uses of theory to design algorithms for problems of logical equivalence, and to verify their correctness.

Coverage: Syntax and semantics of First-Order formulas. Notions of implication and logical equivalence, correlative notions of formal proof. Main proof systems for First-Order Logic. Selected special-purpose proof systems.

Properties of correctness and completeness of proof systems. Working knowledge of the main techniques for their study.

Basic and advanced computational methods for formal proof discovery, applications to problems of logical implication and logical equivalence.