UNSW
COMP4415
First-Order Logic

Session 1
2010


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. Finally, there will be one lecture on description logics.

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. Description logics are the basis of the "Semantic Web", and familiarity with these logics will be an advantage in understanding future developments of the WWW.

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.

Units of Credit

COMP4415 earns you 6 Units of Credit. This signifies 25% of a full-time study load for one semester, and involves 12 weeks × 3 hours/week of lectures, plus assignment work, as detailed below.

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, answer set programming in the non-monotonic logic section (if time permits), and an introduction to description logics.

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. The lecturers are:

Role Name E-Mail Phone
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
Monday 15:00 - 18:00 Australian School of Business, Room 118 (K-E12-118)
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 Michael Maher 01/03 - 22/03
  Mid-session Break   05/04 - 05/04
5-9 Predicate Logic Michael Maher 29/03 - 03/05
8 Anzac Day   26/04 - 26/04
10-12 Nonmonotonic Reasoning and Logic Programming Michael Maher 10/05 - 24/05
13 Introduction to Description Logic Michael Maher 31/05 - 31/05

Note that dates may be revised.

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 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, but there will usually be an assignment every week. 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 30%
Nonmonotonic Reasoning and Logic Programming 30%
Introduction to Description Logic 10%

This course may involve both undergraduate and postgraduate students. Postgraduate students will be held to a higher standard, and will sometimes receive extra or different assignment work.

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.

You should already have seen the Student Code of Conduct, but you should also make your self aware of the new Student Misconduct Procedures.

Textbook

Mordechai Ben-Ari -- Mathematical Logic for Computer Science (2nd edition), Springer.
Notes will be distributed for the non-monotonic reasoning section.


Michael Maher
23-02-2010