Course Identification

Mathematics module: The Mathematics of Programming
20196251

Lecturers and Teaching Assistants

N/A

Course Schedule and Location

2019
First Semester
Tuesday, 11:00 - 12:15, WSoS, Rm 5
Tuesday, 13:00 - 14:00, WSoS, Rm 5
06/11/2018

Field of Study, Course Type and Credit Points

Science Teaching (non thesis MSc Track): Lecture; Obligatory; 4.00 points

Comments

N/A

Prerequisites

No

Restrictions

20
For students in the Rothschild-Weizmann program only

Language of Instruction

Hebrew

Attendance and participation

Obligatory

Grade Type

Numerical (out of 100)

Grade Breakdown (in %)

10%
20%
70%

Evaluation Type

Final assignment

Scheduled date 1

05/03/2019
N/A
-
Final assignment is due by March 5

Estimated Weekly Independent Workload (in hours)

3

Syllabus

Logic is the mathematical foundation of computer programming. There are two approaches to using logic directly to solve problems.

1. SAT solving: The problem is encoded as a formula in propositional logic and the SAT solver software searches for a satisfying interpretation, from which a solution to the problem is obtained.

2. Logic programming: A logic program is a set of formulas in first-order logic that expresses facts and rules about the problem. A goal asks the inference engine software to find a substitution that makes the goal true. This substitution give the solution to the problem.

The course will discuss the theoretical and practical aspects of problem solving using logic:

  1. Propositional logic: syntax, interpretations, semantic tableaux, soundness and completeness, clausal form, resolution, DPLL algorithm for SAT solving, solving problems using a SAT solver.
  2. First-order logic: syntax, interpretations, semantic tableaux, clausal form, Horn clauses, resolution, SLD-resolution, unification, writing a logic problem in Prolog.

Learning Outcomes

Upon successful completion of the course- students should be able to:

  1. Explain the theory of propositional logic and construct semantic tablueux for formulas.
  2. Describe the DPLL algorithm for SAT solving.
  3. Use a SAT solver to encode and solve problems.
  4. Explain the theory of first-order logic. 
  5. Describe the resolution algorithm for logic programming.
  6. Write a logic program in the Prolog language.

Reading List

Lecture notes will be posted and are required reading.

LearnSAT tutorial is available on the software's website.

The following books are optional:

  1. M. Ben-Ari. Mathematical Logic for Computer Science (Third Edition). Springer, 2012.
  2. Z. Scherz et al. Logic Programming (Prolog), Weizmann Institute of Science, 1997 (in Hebrew). Can be obtained from Tarbut laAm: https://stwww1.weizmann.ac.il/?page_id=3163.
  3. P. Blackburn, J. Bos, and K. Striegnitz. Learn Prolog Now. College Publications, 2006. (Available on the SWI-Prolog web site.)
  4. W.F. Clocksin and C.S. Mellish. Programming in Prolog. Springer, 1984.

Software

  1. LearnSAT: https://github.com/motib/LearnSAT
  2.  SWI-Prolog: http://www.swi-prolog.org/
     

Website

N/A