SOA-VBQP
SOA-VBQP
The Second-Order Approach and its Application to View-Based Query Processing
- Contact Christoph Wernhard
- http://cs.christophwernhard.com/projects/soa/
- since 2015
- funded by DFG
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 (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.
Proceedings Articles
The Boolean Solution Problem from the Perspective of Predicate Logic
In Clare Dixon, Marcelo Finger, eds., 11th International Symposium on Frontiers of Combining Systems, FroCoS 2017, volume 10483 of LNCS (LNAI), 333-350, 2017. Springer
Details
Approximating Resultants of Existential Second-Order Quantifier Elimination upon Universal Relational First-Order Formulas
In Patrick Koopmann, Sebastian Rudolph, Renate A. Schmidt, Christoph Wernhard, eds., Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017), volume 2013 of CEUR Workshop Proceedings, 82-98, 2017. CEUR-WS.org
Details
Towards Knowledge-Based Assistance for Scholarly Editing
In Thomas C. Hales, Cezary Kaliszyk, Stephan Schulz, Josef Urban, eds., 1st Conference on Artificial Intelligence and Theorem Proving, AITP 2016 (Book of Abstracts), 29-31, 2016
Details
The PIE system for Proving, Interpolating and Eliminating
In Pascal Fontaine, Stephan Schulz, Josef Urban, eds., 5th Workshop on Practical Aspects of Automated Reasoning (PAAR), volume 1635 of CEUR Workshop Proceedings, 125-138, 2016
Details
Knowledge-Based Support for Scholarly Editing and Text Processing
DHd 2016 – Digital Humanities im deutschsprachigen Raum: Modellierung – Vernetzung – Visualisierung. Die Digital Humanities als fächerübergreifendes Forschungsparadigma. Konferenzabstracts., 176-179, 2016. nisaba verlag
Details
Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications
In Hans de Nivelle, eds., Automated Reasoning with Analytic Tableaux and Related Methods: 24th International Conference, TABLEAUX 2015, volume 9323 of LLNCS (LNAI), 249-265, 2015. Springer
Details
Edited Proceedings
Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017)
Volume 2013 of CEUR Workshop Proceedings, 2017. CEUR-WS.org
Details
Technical Reports
Craig Interpolation and Access Interpolation with Clausal First-Order Tableaux
Technical Report, TU Dresden, volume 18-01, 2018. Knowledge Representation and Reasoning
Details
The Boolean Solution Problem from the Perspective of Predicate Logic – Extended Version
Technical Report, TU Dresden, volume 17-01, 2017. Knowledge Representation and Reasoning
Details
Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications (Extended Version)
Technical Report, TU Dresden, volume 15-04, 2015. Knowledge Representation and Reasoning
Details
Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic
Technical Report, TU Dresden, volume 15-05, 2015. Knowledge Representation and Reasoning
Details
Talks and Miscellaneous
Craig Interpolation and Query Reformulation with Clausal First-Order Tableaux
Poster presentation at TABLEAUX 2017, Brasilia, September 2017
Details
Some Fragments Towards Establishing Completeness Properties of Second-Order Quantifier Elimination Methods
Poster presentation at Jahrestreffen der GI Fachgruppe Deduktionssysteme, associated with CADE 25, August 2015
Details
