This paper introduces predicate logic as it is used in various areas of software development and artificial intelligence, as well as Hoare logic and its use for program verification. Methods of reasoning in logic and automated theorem proving are discussed. In the laboratories, students learn to practice software verification using modern proof tool.
After passing this paper, students will be able to express properties of programs in propositional and predicate logic, to reason in logic, and to conduct program correctness proofs.
Weekly assignments will help to develop an understanding of the concepts of formal logic and its application, and introduce program verification using current proof and software development tools.
This paper contributes to the capabilities 1, 2, 4, 5, 6, 8, and 9 of the Software Engineering Graduate Profile.
COMP103 Introduction to Computer Science 1 and
(COMP235 Logic and Computation or
MATH258 Introduction to Discrete Mathematics)
Official Timetable Information
Some computer-based assignments will require verification during the tutorial following the assignment. Details will be provided when these assignments are handed out. Students are required attend and explain their solution to the lecturer on this occasion.
Students who fail to show for verification of an assignment will receive 0 marks for that assignment.
This is just a rough guideline, but on average students are expected to spend about 10 hours per week on reading, thinking, and doing assignments, in addition to attending the lectures and tutorials. That makes about 14 hours a week. Furthermore, students should expect to spend 30 hours in preparation of the final exam.
Huth, Michael and Ryan, Mark (2004) Logic in Computer Science, 2nd edition, Cambridge University Press.
The Linux computers in Computing Laboratory 6 (R G.18) can be used for the assignments.
This paper is assessed by weekly assignments that include a mixture of questions to be answered on paper and omputer-based exercises, and by the final exam.
The internal assessment/final examination ratio 1:1
Numerical marks will be used to grade assignments and exams, with detailed schedules provided with each assessment item. The weighted total of marks over all assessment items will determine the final grade based on the
University grading schedule.
An overall mark of 50% is required for a pass, with a minimum of 35% in the final exam.
Assignment submission deadlines are firm. Late submissions will not be accepted.
Assignment submission requirements will vary depending on the nature of the assignments, and specific instructions will be provided with each assignment. There will be electronic submissions through Moodle, plus paper components to be placed in a drop-in box.
Marked assignments will usually be returned to students during the tutorial following the submission deadline.
Follow this link for Academic Integrity information.
Follow this link for information on Performance Impairment.
Student Concerns and Complaints
Follow this link for Student Concerns and Complaints information.
Application for Extension
Follow this link for information on applying for an Extension.
Review of Grade
Follow this link for information on applying for a Review of Grade.
Your attention is drawn to the following regulations and policies, which are published in the University Calendar: