Semantics and Program Correctness

Course Code: 
Spring Semester
Credit Points: 

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.

Startup Growth Lite is a free theme, contributed to the Drupal Community by More than Themes.