Introduction to the basic 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, properties of correctness and completeness.
Computational methods for formal proof discovery, applications to problems of logical implication and logical equivalence.