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
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:
- Restriction of knowledge bases to application relevant knowledge
- Modularization of knowledge bases
- Intensional answers
- Non-monotonic reasoning
- Logic programming.
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
- We formally work out a semantic framework based on classical logic
extended with a particular second-order operator, projection. The
elimination of this operator, projection computation, is closely
related to operations termed in the literature as forgetting,
second-order quantifier elimination, Boolean quantifier
elimination, and computation of uniform interpolants.
- We study application patterns of projection computation to tasks in
knowledge representation as listed above by means of concrete examples. A
prototype implementation of projection computation allows to experiment with
- We survey methods for projection computation – or the closely related
elimination of second-order quantifiers. The two prevalent approaches are
resolvent generation (the SCAN algorithm) and formula rewriting with the
Ackermann lemma (the DLS algorithm). Further recent approaches are based on
tableau construction, SAT solving and preprocessing, knowledge compilation,
answer set computation and description logic reasoning.
Decomposable negation normal form.
JACM, 48(4):608-647, 2001.
N. Eén and A. Biere.
Effective preprocessing in SAT through variable and clause
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
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.
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
JAIR, 18:391-443, 2003.
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.
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.
Technische Universität Dresden
Phone: +49 (0)351 463 38345
Office: Room 2017, Nöthnitzer Straße 46, 01187 Dresden
Page at the Faculty