UNSW
COMP4415
First-Order Logic

Session 1
2008


Contents

Objectives

This course is a rigorous introduction to the logics that have been shown to be useful for knowledge representation and a wide range of reasoning in formal computer science, particularly artificial intelligence and proving the correctness of algorithms. The first part covers propositional logic. We start with the semantics of propositional logic, i.e. the formal meaning of logic formulas, and the formal meaning of logical consequence. Then we consider different ways of doing formal inference in propositional logic. In each case we discuss the soundness and completeness of an inference system. A system is sound in which all conclusions drawn are correct. It is complete if it is able to draw all correct conclusions. The second part of the course covers predicate logic (or first-order logic), which can be seen as an extension of propositional logic: everything expressed in propositional logic can also be expressed in predicate logic, but not the other way around. We start with the semantics of predicate logic and then cover different ways of doing formal inference in predicate logic. The third part of the course covers logic programming and nonmonotonic reasoning. We'll have a look at the theoretical basis of logical programming and then move on to discuss practical logic programming languages. Nonmonotonic reasoning is the formalisation of the idea of "defaults", which are used informally to jump to reasonable conclusions in the absence of information.

Learning Outcomes

Students will develop a deeper and more rigorous understanding of propositional and first-order logic, which are already touched on in other courses. This may be particularly helpful to studies of program analysis and verification, relational database theory, algorithms and complexity, and digital logic. Logic formalisms are the lingua franca of much of computer science, and so understanding these logics contributes to students ability to work within the global community. Non-monotonic logics formalize situations where knowledge is incomplete and can change over time. Studies of these logics will also develop an appreciation of the effects of changes in knowledge.

Throughout the course, students will be developing analytical skills as they investigate the underpinnings of logical systems they are already acquainted with, and see a similar development of unfamiliar logics. This provides a basis for students to design a logical system to suit specific requirements, although this activity will not be performed within this course. The skills developed should also help in the design of other formalisms. Through multiple assignments students will develop problem-solving skills, especially in the analysis of knowledge representation formalisms.

Required Knowledge

The handbook entry requires COMP2411 or COMP3121 as pre-requisite for this course. However, this requirement is not based on the content of the courses per se. Rather it reflects a requirement for a certain level of mathematical maturity that can be expected from someone who successfully completes such courses. The main specific knowledge requirement is a familiarity with, and an understanding of, Boolean algebra and Boolean operators.

Recent Revisions -- Course Evaluation and Development

As a result of student comments, the course contents have been revised slightly to strengthen study of computational aspects of the logics. Revisions include discussion of Binary Decision Diagrams for propositional logic, and answer set programming in the non-monotonic logic section (if time permits). There has also been a change of textbook to one with fewer typographical errors. From 2008, the length of a semester is reduced to 12 teaching weeks, but this will not affect the course content.

Organisation & Schedule

The course will consist of one three-hour lecture per week during session.

Lecturer and Contact Information

The lecturer-in-charge for this course is Michael Maher. All lecturers are

Role Name E-Mail Phone
Lecturer Alfredo Gabaldon alfredo@cse.unsw.edu.au 8306 0461
Lecturer-in-charge Michael Maher mmaher@cse.unsw.edu.au 8306 0462
Students with academic questions and/or problems relating to this course should contact the lecturer-in-charge, preferably by email, at mmaher@cse.unsw.edu.au. Questions about specific topics covered in the course should be addressed to the lecturer presenting that topic.

All lecturers have offices in the L5 Building (223 Anzac Parade). To get access to L5, go to reception on the fourth floor, and ask the receptionist to contact the person you have come to see. It is strongly advisable to make an appointment, either by email, or during class, before coming to see a lecturer.

Students are also advised to check the web page of the course frequently:

http://www.cse.unsw.edu.au/~cs4415
as many of the common problems you're experiencing may have already been resolved.

Lectures

The lecture times are:

Day Time Location
Thursday 15:00 - 18:00 Hut D10, Room G01 (K-D10-G01)
If you do not attend lectures, then it is your responsibility to discover any announcements and/or supplemental information that's given.

Current outline (this is flexible and will be subject to minor changes):
Block Topic Lecturer Dates
1-4 Propositional logic Alfredo Gabaldon 13/03 - 10/04
5-9 Predicate Logic Alfredo Gabaldon / Michael Maher 17/04 - 15/05
10-12 Nonmonotonic Reasoning and Logic Programming Michael Maher 22/05 - 05/06

Assignments

Assignments give you the chance to practice what you have learnt. Assignments are a very important part of this course and constitute the sole means of assessment. There is no exam for this course. Therefore it is essential that you attempt them yourself.

To maximise the learning benefits from doing assignments, it is essential that you start work on assignments early. Do not leave your assignments until the last minute. Assignments must be submitted on time, to allow discussion in class of issues arising from the assignment. If a lecturer relaxes this requirement, the maximum available mark for a late assignment is reduced by 10% per day that it is late.

Assessment

There will be assignments on each of three topics covered in the course. The number of assignments may differ from topic to topic, and will be determined by the lecturer(s) of that topic. The marks for assignments associated with each topic will be weighted roughly proportional to the number of lectures devoted to that topic.

The assessable topics of the course are given below. This is subject to some change over the course of the semester. Any change will be announced in class and on the course web page.

Topic Mark
Propositional Logic 30%
Predicate Logic 40%
Nonmonotonic Reasoning and Logic Programming 30%

Exams

There is no exam for this course.

Plagiarism

All work submitted for assessment must be your own work. Assignments must be completed individually. We regard copying of assignments, in whole or part, as a very serious offence. We may use plagiarism detection software to search for multiply-submitted work. Be warned that:

Collaborative work in the form of ``think tanking'' is encouraged, but students are not allowed to derive solutions together as a group during such discussions. Students are also warned not to send solution fragments of the assignments to each other in any form (e.g. as email or listings). In addition, copying/purchasing of solutions that is available on the web is also not permitted. Students who are singled out during our regular plagiarism sweep will be dealt with according to School Policy:
http://www.cse.unsw.edu.au/~studentoffice/policies/yellowform.html.
(see also http://www.cse.unsw.edu.au/help/doc/primer/node42.html)
Where required, follow-up interviews will be conducted by a Panel to decide on an appropriate course of action (if any). The decisions of the panel will be final.

Students are strongly advised to protect their work. Do not leave your terminal/computer unattended, or leave printouts at the printer for others to take.

Textbook

Mordechai Ben-Ari -- Mathematical Logic for Computer Science (2nd edition), Springer.


Michael Maher
08-02-2008