Projection Computation in Knowledge Representation
Lecture in Winter Semester 2010/11
Tuesday 2.DS (9:2010:50), Room INF 2026, Exercises and
Wednesday 4.DS (13:0014: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 firstorder logic – such as
propositional logic, firstorder logic and many description logics –
can be extended by constructs for secondorder quantification, which are
computationally processed by elimination. That is, computing for a
given formula with such secondorder 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
 Abduction
 Intensional answers
 Abstraction
 Nonmonotonic 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 firstorder logic.
 We formally work out a semantic framework based on classical logic
extended with a particular secondorder operator, projection. The
elimination of this operator, projection computation, is closely
related to operations termed in the literature as forgetting,
secondorder 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
small examples.
 We survey methods for projection computation – or the closely related
elimination of secondorder 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.
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 firstorder provers.
The monograph [GSS08] by Gabbay, Schmidt
and Szałas compiles many relevant results. The other references discuss
particular issues.
 Dar01

Adnan Darwiche.
Decomposable negation normal form.
JACM, 48(4):608647, 2001.
 EB05

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 6175. Springer, 2005.
 EW08

Thomas Eiter and Kewen Wang.
Semantic forgetting in answer set programming.
Artificial Intelligence, 172:16441672, 2008.
 GLW06

S. Ghilardi, C. Lutz, and F. Wolter.
Did I damage my ontology? A case for conservative extensions in
description logics.
In KR'06, pages 187197, 2006.
 GSS08

D. M. Gabbay, R. A. Schmidt, and A. Szałas.
SecondOrder Quantifier Elimination: Foundations,
Computational Aspects and Applications.
College Publications, London, 2008.
 HD05

Jinbo Huang and Adnan Darwiche.
DPLL with a trace: From SAT to knowledge compilation.
In IJCAI05, pages 156162, 2005.
 KKT98

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 235324. Oxford University Press, 1998.
 Lin00

Fangzhen Lin.
On strongest necessary and weakest sufficient conditions.
Artificial Intelligence, 128:167175, 2000.
 LLM03

Jérôme Lang, Paolo Liberatore, and Pierre Marquis.
Propositional independence  formulavariable independence and
forgetting.
JAIR, 18:391443, 2003.
 Wer08

Christoph Wernhard.
Literal projection for firstorder logic.
In Logics in Artificial Intelligence: 11th European Conference,
JELIA 08, volume 5293 of LNAI, pages 389402. Springer, 2008.
 Wer09

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 325340. Springer, 2009.
Christoph Wernhard
Technische Universität Dresden
Email: christoph.wernhard@tudresden.de
Phone: +49 (0)351 463 38345
Office: Room 2017, Nöthnitzer Straße 46, 01187 Dresden
Home
Page at the Faculty