|| Timetable || Calendar & Slides || Lab Assignments || Web Resources || Additional Readings ||







Computational Logic



Professor:Pablo R. Fillottrani




Bachelor & Master in Computer Science
Faculty of Computer Science
Free University of Bozen/Bolzano

---

Timetable
2nd. Semester 2005-2006


Lectures: Mon-Wed 8:30-10:30, Room E420

Labs: Mon 14:00-16:00, Room E411

Office Hours: Thu 16:00-18:00, Room 226 Post building

---

Calendar & Slides

• 1. 20/2/2006: Computational Logic: the science -- Propositional Logic I (syntax, semantics)
• 2. 22/2/2006 Propositional Logic II (computational properties, calculi)
• 3. 27/2/2006: Propositional Logic III (algorithms, propositional logic programming)
• 4. 1/3/2006: Applying propositional logic: SATPLAN
• 5. 6/3/2006: First Order Logic I (syntax, substitution calculus)
• 6. 8/3/2006: First Order Logic II (semantics)
• 7. 13/3/2006: First Logic III (normal forms, calculi, properties)
• 8. 15/3/2006: Sorted FOL, Equational Logic
• 9. 20/3/2005: Constraint (Logic) Programming
• 10. 22/3/2005: Nonmonotonic Reasoning I (Default Logic, Circumscription)
• 11. 27/3/2006: Nonmonotonic Reasoning II (Formalizations of negation as failure)
• 12. 29/3/2006: Applying Nonmonotonic Reasoning: Action Languages

---

Lab Assignments

• 1. 20/2/2006: Assignment 1: Propositional Logic
• 2. 27/2/2006: Assignment 2: Resolution
• 3. 6/3/2006: Assignment 3: SATPLAN
• 4. 13/3/2006: Assignment 4: FOL
• 5. 20/3/2006: Assignment 5: Equational Logic, Constraint Programming
• 6. 27/3/2006: Review of corrected solutions to assignments

---

Web Resources

• Logics and Logic Programming
  • From natural language to first order logic
  • The Logical Foundations of Computer Science and Mathematics
  • Default Logic
  • Circumscription
  • Foundations of Logic Programming
• LATEX and math typesetting
  • The Not So Short Introduction to Latex 2e
  • AMS-TeX
  • Latex for Logicians
• Prolog
  • SWI Prolog
  • Ciao Prolog
  • program to transform formulas in CNF
• Automated Theorem Provers
  • SATLIB: collection of SAT solvers and benchmarks
  • MiniSat
  • Otter
  • SPASS
  • FDPLL
  • Darwin
  • The E Equational Theorem Prover
• Answer Set Provers
  • SMODELS
  • DLV

---

Additional Readings

• Definitional Transformation Technique
• Transformation to CNF
• Foundations of Logic Programming
• Constraint Handling Rules

---

||Top|| Timetable || Slides || Assignments || Web Resources || Additional Readings ||