Credits and Contact Hours

3 credits, 43 hours

Course Instructor Name

Dr. Buthainah Al-Kazemi

Textbook

The Deductive Foundations of Computer Programming, Zohar Manna and Richard Waldinger

Logic for Computer Science, Foundation of Automotive Theory Proving by Jean H. Gallier

Catalog Description

This course will present in detail the propositional calculus, predicate calculus, induction, theories with equality, relations, and groups. The deductive tableaux method will be presented and used with propositional and predicate logics as proof method. Use of mathematical logic in describing specifications and designs and prove its correctness. Conversion between English and symbolic presentation.

Prerequisite

CpE-203, CpE-363

Specific Goals for the Course

Upon successful completion of this course, students will be able to:

Translate an English statement into logic and vice versa. (Student outcomes: 1)

Learn deductive tableaux's rules (rewriting, splitting, resolution, quantifier elimination rules, and equivalence rules). (Student outcomes: 1)

Judge if a given system implementation satisfies the system specification. (Student outcome: 1)

Determine whether a goal can be reached given a set of assumptions by using the inference rules and deductive tableaux. (Student outcomes: 1)

Prove a goal under a theory using its theorem. (Student outcomes: 1)

Design a system and prove that its correctness using deductive tableaux. (Student outcomes: 1)

Use some logic software such as DC Proof. (Student outcomes: 1)

Topics to Be Covered

Propositional Logic

Predicate Logic

Axiomatic Theories: Foundations

Theories with Induction: Nonnegative Integers

Applications in Hardware Design