The QET: Quantifier Elimination Techniques Project

This project was previously supported by The Swedish Council for Engineering Sciences (TFR), and is now fully supported by the Wallenberg Foundation (WITAS).

• Introduction to the Quantifier Elimination Techniques (QET) Project
• Quantifier Elimination Techniques and Applications
• The DLS Algorithm On-line Tool
• Selected Publications

Introduction

Research in formal knowledge representation in artificial intelligence has focused primarily on the use of 1st-order or propositional logic as a representation formalism and quite often pursued research agendas whose goal is to isolate well-behaved fragments of FOPC or PL with a potential for applying tractable inference mechanisms associated with these fragments.

Very little energy has been focused on the use of 2nd-order logic as a viable representation formalism, quite often for very good reasons. On the other hand, there are useful fragments of 2nd-order logic that provide a high-level of representational efficacy without necessarily opening the door to additional intractability.

Just as there are a number of techniques which reduce sentences in fragments of 1st-order logic to equivalent sentences in propositional logic via the application of quantifier elimination techniques, there are also quantifier elimination techniques which may be applied to reduce sentences in fragments of 2nd-order logic to equivalent sentences in 1st-order logic.

There are several gains to be made in pursuing research in this area:

• Representational Efficacy - Quantifying over properties or relations is a natural way to succinctly represent knowledge and is the rule rather than the exception in many natural human communication contexts and in describing higher-level cognitive tasks. Computer science is very much about the realm between 2nd-order and 1st-order languages. Examples abound in the areas of database query languages and inductive definitions, logic programming and temporal reasoning using tense logics.
• Inferential Efficiency - Where 2nd-order representations are used, one can often isolate fragments reducible to the 1st-order realm. The use of Circumscription in nonmonotonic reasoning is a case in point. When successful, this opens up the use of well established results for 1st-order logic which can be applied to 2nd-order representations.

Quantifier Elimination Techniques and Applications

The basis of our results begin with a Lemma from 1934 of Ackermann which describes a fragment of 2nd-order logic where existential quantifiers can be eliminated resulting in a logically equivalent 1st-order formula.

In recent years, we have strenghtened this result and applied the theoretical results to several applications in artificial intelligence and main stream database technology. We have also implemented several versions of the quantifier eleimination algorithms used in the applications and are currently pursuing the development of a database front-end language which uses the techniques and can be combined with commercial database systems.

The following applications of the techniques have been or are being investigated:

• [Circumscription] Circumscription is a nonmonotonic reasoning formalism proposed by John McCarthy. Quite often 2nd-order circumscription axioms are added to 1st-order theories to reason normatively or to close the extensions of specific relations in the theory. Our techniques can be used to reduce a reasonably broad class of circumscriptive theories to a logically equivalent 1st-order theory (or sometimes a fixpoint logic theory).
• [Databases] Our techniques can be used in a beneficial manner for the development of database query languages and the processing of queries. We have developed a technique for representing queries in a fragment of 1st-order logic which permits liberal use of quantification and use of classical negation without restriction to rule-based forms, yet guarantees efficient processing of queries. An implementation of these ideas is currently under way.
• [Planning] - The LCW (local closed world assumption ) is potentially useful when planning with incomplete information. We have used our techniques to extend a number of exisiting results in the literature by combining the standard elimination technique with techniques developed for database querying above.
• [Abduction, WSCs, SNCs] - We have recently developed techniques for computing the weakest sufficient and strongest necessary conditions for formulas in an expressive fragment of 1st-order logic using quantifier elimination techniques. The technique has potentially far reaching applications in the areas of theory approximation, generating abductive hypotheses, agent communication languages, and generating successor state axioms for action theories in the situation calculus.

The DLS Algorithm Tool

In 1996, the basic quantifier elimination algorithm (DLS algorithm) was implemented by Joakim Gustafsson as a student project. The implementation is server-based and can be used without downloading additional software. It has been moderately supported with occasional bug fixes. Since this is the basic algorithm, none of the new extensions are included such as reduction to fixpoint formulas or integration with commercial databases. The algorithm does support input of arbitary 2nd-order formulas (not all can be reduced!!) and has special interfaces for a number of alternative circumscription formalisms. To try out the algortihm, please proceed to

The DLS Algorithm Research Tool Home Page.

A revised version and new implementation of the basic DLS algorithm and new extensions is currently underway. Please stay tuned!

Selected Publications

This article describes a powerful application of the quantifier elimination techniques which can be used to automatically generate the weakest sufficient and strongest necessary conditions for a useful fragment of 1st-order logic. There are many applications which are described in the paper:

Computing Strongest Necessary and Weakest Sufficient Conditions of First-Order Formulas.
Doherty, P., Lukaszewicz, W., and Szalas, A.
Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI 2001), Seattle, Washington, USA, August 2001. Morgan Kaufmann Publishers, pages 145-151. [PDF]

An application of QET to efficient generation of Local-Closed World Assumptions for Planning.

Efficient Reasoning using the Local Closed-World Assumption.
Doherty, P., Lukaszewicz, W., and Szalas A.
Proceedings of the 9th International Conference on Artificial Intelligence: Methodology, Systems, and Applications (AIMSA 2000), Varna, Bulgaria, Sept 2000. Lecture Notes in Artificial Intelligence 1904, pages 49-58. [PDF]

This article describes an application of the quantifier elimination techniques to automatic generation of solutions to Smullyan style Knights and Knaves puzzles:

Meta-Queries on Deductive Databases.
Doherty P., Kachniarz A., and Szalas A.
Fundamenta Informatica, Issue 40(1), pages 17-30, 1999. [PDF]

In this article, we developed a logical query language for relational databases based on the "semi-Horn" fragment investigated in a previous article. This fragment captures all and only the PTIME queries to relational databases and has proved to be quite useful in applications:

Declarative PTIME Queries for Relational Databases using Quantifier Elimination.
Doherty, P., Lukaszewicz, W., and Szalas, A.
Journal of Logic and Computation, Issue 9(5), pages 737-758, 1999. [PDF]

This article describes a generalization of domain circumscription and an extension of the DLS algorithm used to reduce domain circumscription axioms:

General Domain Circumscription and its Effective Reductions.
Doherty, P., Lukaszewicz, W., and Szalas, A.
Fundamenta Informaticae, Issue 36(1), pages 1-33, 1998.

This is the most detailed published account of the DLS algorithm with proofs and many examples:

Computing Circumscription Revisited: A Reduction Algorithm .
Doherty, P., Lukaszewicz, W., and Szalas, A.
Journal of Automated Reasoning, Issue 18(3), pages 297-336, 1997.

In this article, we isolated an interesting fragment of 1st-order logic which we call "semi-Horn" formulas and we apply circumscription to this fragment. In this case, the elimination of quantifiers often results in reduction to fix-point formulas. This used an additional generalization of the Ackermann Lemma:

A Reduction Result for Circumscribed Semi-Horn Formulas.
Doherty, P., Lukaszewicz, W., and Szalas, A.
Fundamenta Informaticae, Issue 28(3,4), pages 261-272, 1996.

This is the first published article and provides a moderately detailed account of the DLS algorithm without proofs and includes a few examples:

Computing Circumscription Revisited: Preliminary Report.
Doherty, P., Lukaszewicz, W., and Szalas, A.
Proceedings of the 14th International Joint Conference on Artificial Intelligence, Volume 2, pages 1502-1508, 1996. Extended version appears in Journal of Automated Reasoning 1997.