First Semester
Fri: 11:00 a.m. - 1:00 p.m., Room C1
Fri: 2:00 p.m. - 4:00 p.m., Room E2
Introduction [pdf]
Alan Turing (Wikipedia)
Computer chess (Wikipedia)
Shannon, C., "Programming a Computer for Playing Chess", Philosophical Magazine, 41 (314), 1950 [pdf]
Campbell, M., Hoane, A. J., Hsu, F., "Deep Blue", Artificial Intelligence, 134 (1-2), 2001 [pdf]
"Building Watson - A Brief Overview of the DeepQA Project", YouTube, 2011 [video]
"Final Jeopardy! and the Future of Watson", TED, 2011 [video]
Ferrucci, D., et al., "Building Watson: An Overview of the DeepQA Project", AI Magazine, 3 (31), 2010 [pdf]
Formal Logic [pdf]
Language, schemas and reasoning
Syllogism (ancient logic) (Wikipedia)
Lab 1: Finite State Automata [pdf]
"Parity Checker (as FSA)" [zip] (finite state automaton in Jess)
Finite State Automaton (Wikipedia)
Jess - the Rule Engine for the Java Platform (free software) [link]
Menken, M., Jess Tutorial, Vrije Universiteit, Amsterdam, 2002 [pdf]
Propositional Logic [pdf]
Boolean algebras, formal propositional language and its semantics, satisfiability, entailment
Decisions and Algorithms [pdf]
Decision problems, entailment as a satisfiability problem (i.e. refutation), computational complexity, Semantic Tableau
The Halting Problem (Wikipedia)
Big O Notation (Wikipedia)
The NP complexity class (Wikipedia)
Lab 2: Turing Machine [pdf]
Example: "Parity Checker (TM)" [zip] (Turing Machine in Jess)
Turing Machine (Wikipedia)
Lab 3: Semantic Tableau in Jess [pdf]
Semantic Tableau in Jess [zip]
Deductive Systems [pdf]
Deductive systems 'a la Hilbert', axioms, inference, derivations
Propositional Resolution [pdf]
Resolution as inference rule, propositional resolution by refutation
First-Order Logic [pdf]
First-Order semantic structures, language, validity
Semi-Decidability of First-Order Logic [pdf]
Prenex normal form, skolemization, Herbrand's theorem
First-Order Resolution [pdf]
Clausal form, unification, resolution method for first-order logic
Lab 4: The World of Lists in Prolog [pdf]
Re-definition of append/3 using the function cons/2 [pl]
Prolog examples are compatible with SWI-Prolog
(free software) [link]
SLD Resolution [pdf]
Horn clauses, SLD resolution, logic programming
Backtracking, cut and negation as failure in Prolog [pl]
Minimal Models, Logic Programs [pdf]
Herbrand models, minimal models, logic programming systems
Marco Piastra
The main forum for questions & answers about the course is on piazza.com (please sign-up)
Contact: marco.piastra@unipv.it
To be defined
Mordechai Ben-Ari. Mathematical Logic for Computer Science (3rd Edition). Springer, 2012
Lorenzo Magnani, Rosella Gennari. Manuale di logica. Guerini Scientifica, 1997
Artificial Intelligence: A Modern Approach (3rd Edition). Prentice Hall, 2009.