Time and place: TTh 2-3:30, BUR 224.

Instructor:
Vladimir
Lifschitz
(vl@cs.utexas.edu)

Office hours: T 11-12 and by appointment,
MAI 2010.

TA:
Fangkai Yang
(fkyang@cs.utexas.edu)

Office hours: F 3-4 and by appointment,
MAI 2004.

Prerequisite: Graduate standing.

Grading will be based on class participation.

- John McCarthy, What is artificial intelligence?
- John McCarthy, Programs with common sense
- Wikipedia articles on
- Vladimir Lifschitz, Leora Morgenstern and David Plaisted, Knowledge representation and classical logic
- Gerhard Brewka, Ilkka Niemelä and Mirosław Truszczyński, Nonmonotonic reasoning
- Logical notation in disguise:
- Franz Baader, Ian Horrocks and Ulrike Sattler, Description logics
- Peter Clark and Bruce Porter, KM user's manual
- Patrick Blackburn and Johan Bos, An introduction to computational semantics

- Wikipedia article on Prolog
- Henry Kautz and Bart Selman, Planning as satisfiability
- Carla Gomes, Henry Kautz, Ashish Sabharwal and Bart Selman, Satisfiability solvers
- Vladimir Lifschitz, What is answer set programming?
- Vladimir Lifschitz, Thirteen definitions of a stable model
- Michael Gelfond, Answer sets
- Martin Gebser, Ronald Kaminski, Benjamin Kaufmann, Max Ostrowski, Torsten Schaub and Sven Thiele, User's guide to CLINGO
- Examples of graphs:
- 2011 Answer Set Programming Competition
- Stuart Shapiro, The Job Puzzle: a challenge for logical expressibility and automated reasoning
- Raphael Finkel, Victor Marek and Miroslaw Truszczynski, Constraint Lingo: towards high-level constraint programming
- Timo Soininen and Ilkka Niemela, Developing a declarative rule language for applications in product configuration
- Martin Gebser, Ronald Kaminski, Benjamin Kaufmann and Torsten Schaub, Challenges in answer set solving
- Vladimir Lifschitz, Answer set programming and plan generation
- Monica Nogueira, Marcello Balduccini, Michael Gelfond, Richard Watson and Matthew Barry, An A-Prolog decision support system for the Space Shuttle

- The Davis-Putnam-Logemann-Loveland procedure
- Reducing graph coloring to SAT
- First-order formulas
- Entailment
- Need for an infinite universe
- Intelligent retrieval from a database, Part 1
- Intelligent retrieval from a database, Part 2
- Intelligent retrieval from a database, Part 3
- Program completion
- Intelligent retrieval from a database, Part 4
- Prolog
- SLDNF Resolution
- Transitive closure
- Answer set solvers
- Second-order logic
- Stable models of positive programs, Part 1
- Stable models of positive programs, Part 2
- General definition of a stable model
- Fages' theorem
- The language of CLINGO: choice, intervals, assignments, constant names
- Logic programs with constraints
- The language of CLINGO: cardinality expressions
- Grounding and search
- New Year's Eve party
- Hamiltonian cycles
- Schur numbers
- Who owns the fish?
- Definition C
- Sudoku and Hitori
- Packing
- Blocks World