Forschungsfelder

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
Toggle side column

Forschungsfelder

Examle AF.png

Argumentation ist ein wichtiges Forschungsfeld der Künstlichen Intelligenz und des nichtmonotonen Schließens, welches Anwendungen in Bereichen wie z.B. Legal Reasoning, soziale Netzwerke, E-Government, Multi-Agenten-Systeme und Decision Support findet. Dabei hat sich das Konzept der abstrakten Argumentation Frameworks (AFs) zu einem der beliebtesten Ansätze entwickelt. Dieses relativ einfache aber sehr ausdrucksstarke Modell wurde im Jahre 1995 von Phan Minh Dung eingeführt und besteht, kurz gesagt, aus einer Menge von Argumenten und einer binären Attackrelation zwischen den Argumenten, durch die Konflikte ausgedrückt werden. Dabei ist mit "abstrakt" gemeint, dass man nicht die interne Struktur der Argumente betrachtet, sondern nur die Beziehung der Argumente zueinander, die durch die Attacken gegeben ist. Zur Lösung der Konflikte werden unterschiedliche Semantiken herangezogen, die zulässige Mengen von Argumenten auswählen. Abhängig von der jeweiligen Anwendung genügen diese Semantiken unterschiedlichen Anforderungen.

Answer Set Programming (ASP) ist ein Ansatz zur deklarativen Programmierung, basierend auf Logik Programmen evaluiert unter der sogenannten Stable Model Semantik (oder auch Answer Set Semantik). Ein Answer Set ist ein Modell (im Sinne einer Interpretation) des Logik Programms, und repräsentiert eine Lösung des modellierten Problems. Die deklarative Beschreibung (Modellierung) eines Problems steht dabei im Vordergrund, und nicht etwa die algorithmische Herangehensweise um das Problem zu lösen. ASP eignet sich speziell für (Such-)probleme in NP und NP^NP, und erfreut sich mittlerweile zunehmender Beliebtheit, dank ausgereifter Tool-Unterstützung.


Wir verwenden ASP weitestgehend anwendungsorientiert. So zum Beispiel, um unterschiedliche Semantiken für Argumentation Frameworks abzubilden und mit Hilfe von ASP-Solvern effizient zu berechnen.

Fly-brain.png

Beschreibungslogiken sind eines der Hauptparadigmen der Wissensrepräsentation. Sie sind aus semantischen Netzwerken und Frame-basierten Ansätzen entstanden.

Simple-unsat-16.pdf

Viele natürliche Berechnungsprobleme lassen sich als Constraint Satisfaction Probleme formulieren: gegeben ist eine endliche Menge von Variablen und eine endliche Menge an Bedingungen (Constraints), gefragt ist, ob es eine Lösung gibt, die allen Bedingungen genügt. Für welche Arten von Constraints lassen sich CSPs effizient lösen, und mit welchen Algorithmen? Für welche CSPs kann es solche Algorithmen nicht geben?

Whiteboard-David-Irina.jpg

Existenzielle Regeln sind ein Formalismus zur Wissensrepräsentation mit Anwendungen in der künstlichen Intelligenz und Datenbanken. Ihre syntaktische Allgemeinheit erlauben eine Integration von Formalismen aus der Wissensrepräsentation und aus dem Datenbankbereich. Syntaktisch sind existenzielle Regeln verwandt mit Datalog; ihre wesentliche zusätzliche Ausdrucksstärke besteht in der Möglichkeit, die Existenz von Domänenelementen zu beschreiben, die nicht von vornherein namentlich bekannt sind. Existenzielle Regeln, sind seit längerem unter verschiedenen Bezeichnungen bekannt und die Beantwortung von Anfragen an Daten unter Einbeziehung von existenziellen Regeln ist zur Zeit Gegenstand intensiver Forschung. Typische Fragestellungen hierbei sind beispielsweise: Welche Fragmente existenzieller Regeln verbinden hohe Ausdrucksstärke mit geringer Berechnungsaufwand? Welche allgemeinen Prinzipien garantieren die Entscheidbarkeit der Anfragebeantwortung? Was sind die spezifischen Komplexitäten konkreter Fragmente? Wie entwickelt man effiziente Softwaretools für diese Aufgaben?

Conceptlattice.png

Die Formale Begriffsanalyse ist eine mathematische Theorie, welche Begriffe und Begriffshierarchien mit Hilfe der Verbandstheorie beschreibt. Die Grundlage hierbei bilden elementare Datenstrukturen, so genannte formale Kontexte, welche Gegenständen und deren Merkmale beschreiben. Ein formaler Begriff setzt sich dann zusammen aus einer Menge von Gegenständen und einer Menge von Merkmalen, welche der philosophischen und sprachwissenschaftlichen Tradition folgend als Begriffsumfang und Begriffsinhalt bezeichnet werden. Formale Begriffe können dann zueinander in Beziehung gesetzt werden, woraus sich eine Ober-/Unterbegriffs-Hierarchie ergibt. Die Formale Begriffsanalyse wurde in den 1980er Jahren in Darmstadt in der Arbeitsgruppe von Rudolf Wille begründet und hat sich zu einer Disziplin entwickelt welche in vielen Bereichen praktische Anwendung findet, beispielsweise in Data- und Textmining, Wissensmanagement, Semantic Web, Softwareentwicklung, Wirtschaft oder Biologie.

Satisfiability testing (SAT) is a very generic decision problem, which can be used to solve many industrial problems, such as hardware verification, configuration, planning, or for tasks in bio informatics. Hence, improvements of SAT technology have a direct impact to all the fields that exploit SAT solvers in their tool chain.

Sequential and Parallel SAT Solving

We develop a generic SAT-solver that serves as a basis for various solver configurations via combination of solver components. It shall offer great flexibility in deriving different SAT-solver instances from available components and existing parameters. This is of importance in many respects, e.g. in optimizing solvers for a particular domain by automatically tuning solver parameters and in constructing portfolio-based solvers. We consider components from classical DPLL-based to CDCL-based solvers, from principal components (e.g. search, unit propagation, decision heuristics, backtracking) to secondary components (e.g. learning, clause forgetting heuristics, restart heuristics). A special focus is put on simplification and formula rewriting techniques.


Given a good sequential SAT solver, parallel solvers are investigated to improve the performance of SAT technology on modern multi-core architectures. Here, the focus is to partition the search space recursively, to benefit from the increasing number of available computing resources.

As SAT systems become more and more complex, verifiable output is required. Hence, we study how to produce unsatisfiability proofs for existing SAT techniques and parallel SAT solvers, to allow to use as many existing techniques as possible and still being able to verify the result of the SAT solver.

Encoding Real-World Problems

Furthermore, encoding real world problems into the language of SAT is often non-trivial. Hence, encodings for commonly used constraints are studies and new ways to describe these constraints in propositional logic are developed. We currently focus on cardinality constraints and pseudo Boolean constraints, which are frequently used in configuration, car sequencing, or planning.

Optimization and Enumerating all Models

Besides solving a single decision problem with a SAT solver, finding an optimal solution, or finding all solutions are two common tasks as well. In our group, we extend SAT solvers to encounter all solutions of a formula, or the related real world problem. Furthermore, we develop an optimization solver.

Kiwv-group-picture.jpg

Human Reasoning, Computational Logic, and Connectionism
The project aims at developing non-classical logics as well as connectionist realizations thereof which are adequate for human reasoning.
For further information, please contact Christoph Wernhard.

Human Reasoning in Computational Logic

Until now there are no widely accepted theories that give formal representations of sophisticated human reasoning. In our project we address this issue by exploring current results from relevant research areas. The goal is to formalize a framework that allows the expression of reasoning processes which are fundamental in order to explain human behaviour. Conventional formal approaches such as classical logic are not appropriate for this purpose as they cannot deal with the most elementary parts humans are confronted with e.g. incomplete information. Alternatives can be found in formalizations of weaker logics such as non-monotonic logics or three-valued logics. Furthermore, in the field of neurosicence (e.g. connectionist networks) and cognitive science (e.g. studies from psychological reasoning such as the selection and suppression task) a lot of reaserach is going on in understanding and simulating human reasoning processes. Their results are important for our purpose as they deal with similar fundamental questions about human behaviour.
For further information, please contact Emmanuelle Dietz.

Semantic-technologies.png

Semantische Technologien umfassen eine Vielzahl verschiedener Methoden und Technologien, die der Darstellung, der Verwaltung, dem Austausch oder der Verarbeitung von semantischer Daten dienen. Den Kern dieser Arbeiten bilden maschinen-lesbare Formate für Daten und Schemainformation (Ontologien). Bedeutende Technologiestandards wurden dafür vom World Wide Web Consortium (W3C) verabschieded, insbesondere im Rahmen der Anstrengungen rund um das sogenannte Semantic Web bzw. Web of Data. Die wichtigsten dieser Standards sind das RDF Resource Description Language (ein graph-basiertes Datenformat), die OWL Web Ontology Language (eine auf Beschreibungslogiken basierende Ontologiesprache) sowie die SPARQL Protocol and RDF Query Language (eine Sprache für Datenbankabfragen und Datenverwaltung). Dennoch umfassen semantische Technologien auch andere Ansätze, wie zum Beispiel die Metadaten-Annotation mittels schema.org, sowie methodologische und infrastrukturelle Aspekte.


Die Forschung im Bereich semantischer Technologien beschäftigt sich mit einer Vielzahl angewandter Fragestellungen. Die Spezifikation und Verarbeitung von Ontologien ist dabei eng mit dem Gebiet der Wissensrepräsentation und des logischen Schließens verwandt, während andere Fragestellungen einen Bezug zu Datenbanken, Informationsextraktion und Web-Systemen haben. Die besondere Natur verteilter Daten im Web spielt besonders im Bereich Linked Open Data eine wichtige Rolle, gleichwohl gibt es viele wichtige Anwendungen von OWL und RDF, in denen das World Wide Web nur eine untergeordnete Rolle spielt.

Ramon Llull - Ars Magna Tree and Fig 1.png

Das Forschungsgebiet Wissensrepräsentation und logisches Schließen befasst sich mit der Darstellung von menschlichem Wissen in Computersystemen und mit der Berechnung logischer Konsequenzen aus diesem Wissen. Durch logische Deduktion leiten solche Systeme implizites Wissen aus den gegebenen Informationen ab. Damit spielt die formale Wissensrepräsentation eine wichtige Rolle zur Konstruktion intelligenter Computersysteme. Aber auch in Anwendungen, in denen große Wissensbasen erstellt werden, werden diese Technologien eingesetzt, da logisches Schließen helfen kann, Redundanz zu vermeiden und Fehler zu entdecken.


Die meisten modernen Ansätze in der Wissensrepräsentation beruhen auf formaler Logik, wobei Beschreibungslogiken und regelbasierte Formalismen die wichtigsten Sprachfamilien darstellen. In vielen Anwendungen sind Wissensbasen die Grundlage für Ontologien, so dass Wissensrepräsentation in enger Beziehung zu anderen Forschungegebieten steht, zum Beispiel zu semantischen Technologien. Obwohl das Grundgerüst der Wissensrepräsentation die theoeretische Forschung auf der formalen Logik ist, umfasst die Forschung in diesem Gebiet auch viele angewandte Fragestellungen, so z.B. die Entwicklung effizienter Tools zum automatischen Schließen.