The Second-Order Approach
and its Application to
View-Based Query Processing –
Project Page

About the Project Publications and Systems Background Technology References

About the Project

In the project, an approach to logic-based knowledge processing, to be called here second-order approach, will be investigated. The idea is that expressive representation languages are, on the one hand, available to formulate applications in a very natural way, but on the other hand, are processed by reduction to poorer languages that are better suited for computation. Such reductions are made possible because the expressive language constructs are used in specific application contexts.

Proofs of concept for this approach have been given in the late 90s with the use of second-order quantifier elimination for computing circumscription, and recently with applications of uniform interpolation and forgetting (which can be expressed as second-order quantifier elimination) in description logics. The approach typically allows to trace concepts from the application area back to fundamental concepts of logic, indicating new application possibilities and parallels between areas that enable transfer and combination of techniques.

The project connects two lines of work that will stimulate each other:

  1. Concepts of a particular application area, view-based query processing, will be formally modeled with second-order operators.
  2. Computational methods will be developed that realize applications, on the basis of the formalization, essentially by elimination of second-order operators.

The basic idea of view-based query processing is to translate and decompose queries such that multiple agents with specialized knowledge bases and processing capabilities can contribute to answer computation. By its is close relation to definability, a general concept of logic, view-based query processing is well suited to the approach of the project. Central objectives of the project with respect to view-based query processing are semantic clarification of the involved concepts, availability of second-order operator elimination to compute query transformations, and generalization beyond databases.

With respect to computational methods, new techniques for second-order operator elimination will be developed, based on propositional logic – related to recent SAT preprocessors, based on first-order logic, and by taking specific formula patterns into account that occur in view-based query processing.

The results of the project should serve as an elaborate formal and automated foundation for a multitude of further applications that are suited for the second-order approach. These include, for example, variants of non-standard inferences, abductive reasoning, modularization of knowledge bases, non-monotonic reasoning, and reasoning about knowledge.

Publications and Systems

Techniques Related to Second-Order Quantifier Elimination

Abstract: Finding solution values for unknowns in Boolean equations was a principal reasoning mode in the Algebra of Logic of the 19th century. Schröder investigated it as Auflösungsproblem (solution problem). It is closely related to the modern notion of Boolean unification. Today it is commonly presented in an algebraic setting, but seems potentially useful also in knowledge representation based on predicate logic. We show that it can be modeled on the basis of first-order logic extended by second-order quantification. A wealth of classical results transfers, foundations for algorithms unfold, and connections with second-order quantifier elimination and Craig interpolation show up. Although for first-order inputs the set of solutions is recursively enumerable, the development of constructive methods remains a challenge. We identify some cases that allow constructions, most of them based on Craig interpolation, and show a method to take vocabulary restrictions on solution components into account.

Research on Methods for Second-Order Quantifier Elimination

Abstract: For relational monadic formulas (the Löwenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, forgetting and projection, always succeeds. The decidability proof for this class by Behmann from 1922 explicitly proceeds by elimination with equivalence preserving formula rewriting. We reconstruct Behmann's method, relate it to the modern DLS elimination algorithm and show some applications where the essential monadicity becomes apparent only at second sight. In particular, deciding ALCOQ knowledge bases, elimination in DL-Lite knowledge bases, and the justification of the success of elimination methods for Sahlqvist formulas.

Abstract: For relational monadic formulas (the Löwenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, projection and forgetting – operations that currently receive much attention in knowledge processing – always succeeds. The decidability proof for this class by Heinrich Behmann from 1922 explicitly proceeds by elimination with equivalence preserving formula rewriting. Here we reconstruct the results from Behmann's publication in detail and discuss related issues that are relevant in the context of modern approaches to second-order quantifier elimination in computational logic. In addition, we give a summary as well as a commented register of further relevant material in unpublished manuscripts by Behmann and in his correspondence, especially with Wilhelm Ackermann.

Remark: This is a 100-pages report centered around those works by Behmann that concern second-order quantifier elimination. It includes relevant extracts (supplied with English translations) and English summaries of so far unpublished German manuscripts by Behmann and of his correspondence with Ackermann and others that are archived in Behmann's Nachlass. The material is accompanied by an extensive technical and historial discussion. Some of the material seems also to be relevant in a broader context of the history of methods of computational logic and in the specific context of investigating the early history of resolution.

Abstract: We present some preliminary results which should be useful in the development of second-order quantifier elimination methods for which success can be shown based on semantic properties of the input formulas. The basic tools are Tarski's characterization of definability as validity and Craig's interpolation to compute definienda, which succeeds in case of definability.

The PIE Environment for First-Order-Based Proving, Interpolating and Eliminating

Abstract: The PIE system aims at providing an environment for creating complex applications of automated first-order theorem proving techniques. It is embedded in Prolog. Beyond actual proving tasks, also interpolation and second-order quantifier elimination are supported. A macro feature and a LaTeX formula pretty-printer facilitate the construction of elaborate formalizations from small, understandable and documented units. For use with interpolation and elimination, preprocessing operations allow to preserve the semantics of chosen predicates. The system comes with a built-in default prover that can compute interpolants.

KBSET – Knowledge-Based Support for Scholarly Editing

KBSET is a prototype system resulting from an interdisciplinary collaboration with the objective of investigating possibilities to support of scholarly editing (Editionswissenschaft). The system will applied in a large such project, a comprehensive scholarly edition of the correspondence of Swiss polymath Johann Georg Sulzer (1720-1779), coordinated at Martin-Luther-Universität Halle-Wittenberg. Originally, KBSET has been developed independently of the “Second-Order Approach” project. However, since some of the issues addressed in the project, in particular view-based access to large knowledge bases, turned out quite relevant for such a system, it has been decided to use KBSET as a platform for experiments with the logic-based techniques developed in the project in an actual application context with users from another scientific discipline. Other envisaged areas of for experiments in the context of scholarly editing and in Digital Humanities in general concern the combination of specifications provided by users (editors), fragments of natural language text, and formalized knowledge, which requires various forms of extraction, combination, and completion of pieces of information. From a logic point of view, key techniques there are circumscription and logic-based approaches to modularization, both of which can be formally based on second-order quantifier elimination.

Abstract: We investigate possibilities to utilize techniques of computational logic for scholarly editing. Semantic Web technology makes large relevant knowledge bases such as GND, GeoNames, Yago and DBpedia available in form of logic formulas, but there are several further roles of logic languages in machine supported scholarly editing. Important issues that arise will be discussed. This includes integrating automatically inferred and explicitly provided knowledge to incorporate advanced semantics related techniques like named entity recognition. We consider high quality support at all phases involved in the process of scholarly editing, loose coupling of object text and markup by external annotations, representation of epistemic status, and utilizing inferred access patterns for external knowledge bases. An implemented free software prototype system, called KBSET, is described.

Abstract: We investigate possibilities to utilize techniques of computational logic for scholarly editing. Semantic Web technology already makes relevant large knowledge bases available in form of logic formulas. There are several further roles of logic-based reasoning in machine supported scholarly editing. KBSET, a free prototype system, provides a platform for experiments.

Background Technology

This section gives an overview on the background technology of the project. References are suggested that may be useful as introductions to the respective areas for interested non-specialists.

Second-Order Quantifier Elimination

Second-order quantifier elimination means to compute for a given formula with second-order quantification, such as the quantification upon predicate q in

∃q (∀x px ∨ qx) ∧ (∀x ¬qx ∨ rx),

an equivalent first-order formula such as, for the above example

∀x px ∨ rx.

The investigation of second-order quantifier elimination goes back to Boole (1815-1864), Peirce (1839-1914) and Schröder (1841-1902) (see [Cra08]). For propositional formulas and first-order formulas with only unary predicates, general methods that succeed on all inputs can be given, whose developed accompanied early investigations of modern first-order logic by Löwenheim (1878-1957), Skolem (1887-1963) and Behmann (1891-1970). Ackermann (1896-1962) systematically investigated second-order quantifier elimination in the mid-1930s.

In computer science it came to attention in the 1990s through investigations in modal logics and the computation of circumscription.The main algorithms are based on techniques developed by Ackermann. Since the late 2000s it received further interest in the context of logic-based knowledge representation with description logics, where it is the core technique to semantically extract knowledge about a subvocabulary (e.g. the predicates p and r in the above example). Forgetting, uniform interpolation, and projection are variants of second-order quantifier elimination used in that context. Also the notion of conservative extension, the basis of recent semantic-based approaches to knowledge base modularization, can be expressed with second-order quantification and processed with elimination.

The Davis-Putnam method from about 1960 for determining propositional satisfiability, which underlies modern CDCL SAT solving methods, can be understood as based on eliminating propositional variables – or nullary atoms. In modern SAT solvers restricted forms of elimination are directly applied in pre- and in-processing [EB05], complementary to the core control regime of CDCL. Formulas of second-order logic can be useful to express semantic characterizations of processing techniques for propositional formulas, which often preserve second-order equivalences [Phi01].

Automated First-Order Theorem Proving

Automated first-order theorem proving is not just applied to prove theorems in mathematics, but also, probably motivated by the program of formalizing common sense initiated in the late 1950s by McCarthy, as a general knowledge processing mechanism. Deductive databases, generalizations of the well-known relational databases, logic programming and reasoning in description logics for knowledge representation might be viewed as spin-offs of automated theorem proving.

Prolog as Implementation Technology

Prolog is a logic programming language based on associating a flow of control with formulas of first-order logic in a restricted syntactic form. Unlike other logic programming approaches such as answer set programming it is a full general-purpose programming language, allowing many techniques known from other programming languages. Like LISP, the first prominent AI programming language, Prolog has a uniformly structured syntax that allows to directly read-in and print-out data structures – such as formulas in some logic or in Prolog itself – and to specify procedures operating on them by means structural recursion with term patterns. The built-in support for unification and depth-first search are useful as building blocks for manipulating first-order formulas.

SWI Prolog is a robust and portable implementation with efficient interfaces to modern Semantic Web formats such as RDF.

View-Based Query Processing and Definability

In many scenarios it is useful to evaluate a query expressed in some user vocabulary in two steps: it is first rewritten and decomposed to suit available repositories and processing engines, which then perform the actual processing. Many ways to rewrite queries can be considered abstractly as second-order quantifier elimination: The query in the user vocabulary is conjoined with formulas representing background knowledge and mappings to the repositories and processing languages. Second-order quantifier elimination then effects forgetting about the symbols that are not from the repository and processing layer.

Some cases of query rewriting can also be understood as finding a definiens of the given query that is in terms of the target layer vocabulary and with respect to a formula that expresses background knowledge and mappings. Interpolation provides a way to compute such definienda, essentially by a translation to validity. For first-order logic, this technique succeeds in principle whenever a definiens in the target vocabulary exist, analogously to determining validity. By Craig's interpolation theorem [Cra57], if a first-order formula F entails another one G, then there is a third first-order formula H, called an interpolant of the first two, which only contains symbols occurring in both, F and G, is entailed by F and entails G, in symbols:

F ⊨ H ⊨ G.

Such an interpolant can be extracted from a proof that F entails G or, equivalently, that F → G is valid. Based on the computation of interpolants, definientia in a given vocabulary can be computed, that is, for given formulas F and G[x], where [x] indicates that x possibly occurs as free individual variable in the formula, a third formula H[x] in the given vocabulary is found such that

F ⊨ ∀x G[x] ↔ H[x],

whenever a formula meeting the conditions stated on H[x] exists.

References

[Ack35a]
Wilhelm Ackermann. Untersuchungen über das Eliminationsproblem der mathematischen Logik. Mathematische Annalen, 110:390-413, 1935.
[Ack35b]
Wilhelm Ackermann. Zum Eliminationsproblem der mathematischen Logik. Mathematische Annalen, 111:61-63, 1935.
[Beh22]
Heinrich Behmann. Beiträge zur Algebra der Logik, insbesondere zum Entscheidungsproblem. Mathematische Annalen, 86(3-4):163-229, 1922.
[Bib92]
Wolfgang Bibel. Deduktion – Automatisierung der Logik. Oldenbourg, 1992.
[Bib93]
Wolfgang Bibel. Deduction: Automated Logic. Academic Press, 1993.
[BtCT14]
Michael Benedikt, Balder ten Cate, and Efthymia Tsamoura. Generating low-cost plans from proofs. In PODS'14, pages 200-211. ACM, 2014.
[CGLV07]
Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, and Moshe Y. Vardi. View-based query processing: On the relationship between rewriting, answering and losslessness. Theoret. Comp. Sci., 371(3):169-182, 2007.
[Chu56]
Alonzo Church. Introduction to Mathematical Logic, revised edition, Princeton University Press, 1956.
[CL73]
Chin-Linag Chang and Richard Char-Tung Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.
[CM03]
William Clocksin and Christopher S. Mellish. Programming in Prolog. Springer, 5th edition edition, 2003.
[Cra08]
William Craig. Elimination problems in logic: A brief history. Synthese, (164):321-332, 2008.
[Cra57]
William Craig. Linear reasoning. A new form of the Herbrand-Gentzen theorem. The J. of Symbolic Logic, 22(3):250-268, 1957.
[DŁS97]
Patrick Doherty, Witold Łukaszewicz, and Andrzej Szałas. Computing circumscription revisited: A reduction algorithm. J. Autom. Reason., 18(3):297-338, 1997.
[EB05]
Niklas Eén and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. In SAT'05, volume 3569 of LNCS, pages 61-75. Springer, 2005.
[Fit96]
Melvin Fitting. First-Order Logic and Automated Theorem Proving, Second Edition. Springer, 1996.
[GO92]
Dov Gabbay and Hans Jürgen Ohlbach. Quantifier elimination in second-order predicate logic. In KR'92, pages 425-435. Morgan Kaufmann, 1992.
[GSS08]
Dov M. Gabbay, Renate A. Schmidt, and Andrzej Szałas. Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. College Publications, 2008.
[Kow14]
Robert Kowalski. History of logic programming. In Dov Gabbay and John Woods, editors, Computational Logic, volume 9, (Jörg Siekmann, editor) of History of Logic, pages 523-569. Elsevier, 2014.
[KW16a]
Jana Kittelmann and Christoph Wernhard. Knowledge-based support for scholarly editing and text processing. In DHd 2016 – Digital Humanities im deutschsprachigen Raum: Modellierung – Vernetzung – Visualisierung. Die Digital Humanities als fächerübergreifendes Forschungsparadigma. Konferenzabstracts, pages 176-179. nisaba verlag, 2016.
[KW16b]
Jana Kittelmann and Christoph Wernhard. Towards knowledge-based assistance for scholarly editing. In AITP 2016 (Book of Abstracts), 2016.
[O'K90]
Richard A. O'Keefe. The Craft of Prolog. The MIT Press, 1990.
[Mar07]
Maarten Marx. Queries determined by views: Pack your views. In PODS'07, pages 23-30. ACM, 2007.
[NSV10]
Alan Nash, Luc Segoufin, and Victor Vianu. Views and queries: Determinacy and rewriting. TODS, 35(3), 2010.
[Phi01]
Tobias Philipp. Certificates for Parallel SAT Solver Portfolios with Clause Sharing and Inprocessing. In GCAI 2016, volume 41 of EPiC, pages 24-38.
[RV01]
A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning, volume I and II. Elsevier Science, 2001.
[Tar35]
Alfred Tarski. Einige methologische Untersuchungen zur Definierbarkeit der Begriffe. Erkenntnis, 5:80-100, 1935.
[TW11]
David Toman and Grant Weddell. Fundamentals of Physical Design and Query Compilation. Morgan and Claypool, 2011.
[Wer15a]
Christoph Wernhard. Heinrich Behmann's contributions to second-order quantifier elimination from the view of computational logic. Technical Report Knowledge Representation and Reasoning 15-05, Technische Universität Dresden, 2015.
[Wer15b]
Christoph Wernhard. Second-order quantifier elimination on relational monadic formulas – A basic method and some less expected applications. In TABLEAUX 2015, volume 9323 of LNCS (LNAI), pages 249-265. Springer, 2015.
[Wer15c]
Christoph Wernhard. Second-order quantifier elimination on relational monadic formulas – A basic method and some less expected applications (extended version). Technical Report Knowledge Representation and Reasoning 15-04, Technische Universität Dresden, 2015.
[Wer15d]
Christoph Wernhard. Some fragments towards establishing completeness properties of second-order quantifier elimination methods. Poster presentation at Jahrestreffen der GI Fachgruppe Deduktionssysteme, associated with CADE-25, 2015.
[Wer16a]
Christoph Wernhard. The PIE system for Proving, Interpolating and Eliminating. In PAAR 2016, volume 1635 of CEUR Workshop Proceedings, pages 125-138, 2016
[Wer17a]
Christoph Wernhard. The Boolean Solution Problem from the Perspective of Predicate Logic In FroCoS 2017, LNCS (LNAI), Springer, 2017 (to appear).
[Wer17b]
Christoph Wernhard. The Boolean Solution Problem from the Perspective of Predicate Logic – Extended Version Technical Report Knowledge Representation and Reasoning 17-01, Technische Universität Dresden, 2017.

Contact: info@christophwernhard.com