This project was previously supported by The Swedish Council for Engineering Sciences (TFR), and is now fully supported by the Wallenberg Foundation (WITAS).
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:
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:
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!
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.