Projection Computation in Knowledge Representation

Lecture in Winter Semester 2010/11
Tuesday 2.DS (9:20-10:50), Room INF 2026, Exercises and
Wednesday 4.DS (13:00-14:30), Room INF 2101, Lecture
The course language is English
Prerequisites are good knowledge of logics and of programming

Note: The exercises/lecture on Tuesday 21.12. and Wednesday 22.12. are cancelled

Course Description

Knowledge representation formalisms whose expressivity is included within first-order logic – such as propositional logic, first-order logic and many description logics – can be extended by constructs for second-order quantification, which are computationally processed by elimination. That is, computing for a given formula with such second-order constructs an equivalent formula that does not involve them. With this approach, many important techniques and operations in knowledge representation can be expressed, and even integrated within a single application. In particular, these include various forms of:

In the course, we develop a formal framework, study application patterns and survey computation methods. We do this first for propositional logic as a basis and later on consider first-order logic.


The exercises will involve the application of automated theorem proving systems and programming, where the suggested implementation language is Prolog. The exercises include formalising and proving properties of the semantic framework with assistance of an automated theorem proving system, devising small application examples with an automated system, and implementing preprocessors for SAT solvers and first-order provers.


The monograph [GSS08] by Gabbay, Schmidt and Szałas compiles many relevant results. The other references discuss particular issues.
Adnan Darwiche.
Decomposable negation normal form.
JACM, 48(4):608-647, 2001.
N. Eén and A. Biere.
Effective preprocessing in SAT through variable and clause elimination.
In Theory and Applications of Satisfiability Testing: 8th Int. Conf., SAT 2005, volume 3569 of LNCS, pages 61-75. Springer, 2005.
Thomas Eiter and Kewen Wang.
Semantic forgetting in answer set programming.
Artificial Intelligence, 172:1644-1672, 2008.
S. Ghilardi, C. Lutz, and F. Wolter.
Did I damage my ontology? A case for conservative extensions in description logics.
In KR'06, pages 187-197, 2006.
D. M. Gabbay, R. A. Schmidt, and A. Szałas.
Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications.
College Publications, London, 2008.
Jinbo Huang and Adnan Darwiche.
DPLL with a trace: From SAT to knowledge compilation.
In IJCAI-05, pages 156-162, 2005.
A. C. Kakas, R. .A. Kowalski, and F. Toni.
The role of abduction in logic programming.
In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5, pages 235-324. Oxford University Press, 1998.
Fangzhen Lin.
On strongest necessary and weakest sufficient conditions.
Artificial Intelligence, 128:167-175, 2000.
Jérôme Lang, Paolo Liberatore, and Pierre Marquis.
Propositional independence - formula-variable independence and forgetting.
JAIR, 18:391-443, 2003.
Christoph Wernhard.
Literal projection for first-order logic.
In Logics in Artificial Intelligence: 11th European Conference, JELIA 08, volume 5293 of LNAI, pages 389-402. Springer, 2008.
Christoph Wernhard.
Tableaux for projection computation and knowledge compilation.
In Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX 2009, volume 5607 of LNAI, pages 325-340. Springer, 2009.

Christoph Wernhard
Technische Universität Dresden
Phone: +49 (0)351 463 38345
Office: Room 2017, Nöthnitzer Straße 46, 01187 Dresden
Home Page at the Faculty