SOA-VBQP
SOA-VBQP
Der Second-Order Ansatz und dessen Anwendung in der Sicht-basierten Anfrageverarbeitung
- Kontaktperson Christoph Wernhard
- http://cs.christophwernhard.com/projects/soa/
- seit 2015
- finanziert durch DFG
Im Projekt wird ein Ansatz zur Logik-basierten Wissensverarbeitung untersucht, der hier Second-Order Ansatz genannt werden soll. Die Idee ist, dass ausdrucksstarke Repräsentationssprachen einerseits verfügbar sind, um Anwendungen auf sehr natürliche Art zu formulieren, andererseits aber durch Reduktion auf schwächere Sprachen verarbeitet werden, die sich besser zur Berechnung eignen. Solche Reduktionen werden durch die Verwendung der ausdrucksstarken Sprachkonstrukte in spezifischen Anwendungskontexten ermöglicht.
Proofs of Concept für diesen Ansatz wurden in den späten 90er Jahren mit dem Einsatz der Elimination von Quantoren zweiter Stufe zur Zirkumskriptionsberechnung und in letzter Zeit mit Anwendungen der uniformen Interpolation (die sich als Elimination von Quantoren zweiter Stufe ausdrücken lässt) in Beschreibungslogiken vorgelegt. Der Ansatz erlaubt es typischerweise, Konzepte aus dem Anwendungsbereich auf grundlegende Konzepte der Logik zurückzuführen und damit neue Anwendungsmöglichkeiten sowie Parallelen zwischen Gebieten, die den Austausch und die Kombination von Techniken ermöglichen, aufzuzeigen.
Das Projekt verbindet zwei Arbeitslinien, die sich gegenseitig anregen: (1) Konzepte aus einem bestimmten Anwendungsbereich, der Sicht-basierten Anfrageverarbeitung, werden formal mit Operatoren zweiter Stufe modelliert. (2) Berechnungsmethoden werden entwickelt, die Anwendungen auf Grundlage der Formalisierung und im Wesentlichen durch Elimination von Operatoren zweiter Stufe realisieren.
Grundidee der Sicht-basierten Anfrageverarbeitung ist, Anfragen zu übersetzen und zu zerlegen, so dass mehrere Agenten mit spezialisierten Wissensbasen und Verarbeitungsfähigkeiten zur Antwortberechnung beitragen können. Sicht-basierte Anfrageverarbeitung ist durch den engen Bezug zu Definierbarkeit, einem allgemeinen Konzept der Logik, für den Ansatz des Projekts gut geeignet. Projektziele bezüglich der Sicht-basierten Anfrageverarbeitung sind semantische Klärung der beteiligten Konzepte, Erschließung der Elimination von Operatoren zweiter Stufe zur Berechnung von Anfragetransformationen sowie Generalisierung über Datenbanken hinaus.
In Bezug auf Berechnungsmethoden sollen neue Techniken zur Elimination von Quantoren zweiter Stufe entwickelt werden, basierend auf Aussagenlogik - verwandt mit aktuellen SAT-Präprozessoren, basierend auf Prädikatenlogik erster Stufe, sowie durch Berücksichtigung spezifischer Formelmuster, die in der Sicht-basierten Anfrageverarbeitung vorkommen.
Die Projektergebnisse sollen als ausgearbeitete formale und automatisierte Grundlage für eine Vielzahl von weiteren für den Second-Order Ansatz geeigneten Anwendungen dienen. Dazu gehören beispielsweise Varianten von nicht-standard Inferenzen, abduktives Schließen, Modularisierung von Wissensbasen, nicht-monotones Schließen und Schließen über Wissen.
Artikel in Tagungsbänden
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
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
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
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
Herausgegebene Tagungsbände
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
Technische Berichte
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
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
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
Vorträge und Sonstiges
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
