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
Exercises
Literature
Downloads

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:

Restriction of knowledge bases to application relevant knowledge
Modularization of knowledge bases
Abduction
Intensional answers
Abstraction
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.

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 small examples.
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.

Exercises

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.

Literature

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):608-647, 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 61-75. Springer, 2005.
EW08: Thomas Eiter and Kewen Wang.
Semantic forgetting in answer set programming.
Artificial Intelligence, 172:1644-1672, 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 187-197, 2006.
GSS08: D. M. Gabbay, R. A. Schmidt, and A. Szałas.
Second-Order 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 IJCAI-05, pages 156-162, 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 235-324. Oxford University Press, 1998.
Lin00: Fangzhen Lin.
On strongest necessary and weakest sufficient conditions.
Artificial Intelligence, 128:167-175, 2000.
LLM03: Jérôme Lang, Paolo Liberatore, and Pierre Marquis.
Propositional independence - formula-variable independence and forgetting.
JAIR, 18:391-443, 2003.
Wer08: 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.
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 325-340. Springer, 2009.

Christoph Wernhard
Technische Universität Dresden
E-mail: christoph.wernhard@tu-dresden.de
Phone: +49 (0)351 463 38345
Office: Room 2017, Nöthnitzer Straße 46, 01187 Dresden
Home Page at the Faculty