ALMANAC: Argumentation Logics Manager and Argument Context Graph
In Entscheidungssituationen müssen Individuen und Organisationen zwischen einer Vielzahl von Optionen wählen. Sie stützen sich dabei auf Fakten, Meinungen und Argumente über diese oder ähnliche Situationen; Softwaresysteme, die bei der Entscheidung helfen könnten, beschränken sich dagegen auf die Faktenebene und ziehen Argumentationen nicht in Betracht.
Das Schwerpunktprogramm bringt Forscher zusammen, die robuste und skalierbare Modelle für Argumentationen in menschlicher Kommunikation untersuchen. Das ALMANAC Projekt soll den LogikPfeiler dieses Unterfangens unterstützen. Es gibt bereits eine große Menge an Arbeiten zur Wissensrepräsentation, zum Schlussfolgern und zur Modellierung von Argumentationen, und das SPP wird ohne Zweifel weitere entwickeln.
Das erste Ziel des ALMANAC Projekts is es, eine einheitliche Infrastruktur bereitzustellen, die die Zusammenarbeit zwischen den Projekten des SPP und der Argumentations-Community erleichtert, Resultate vergleichbar macht, und die Entwicklung gemeinsamer, logik-basierter Ressourcen unterstützt.
Konkret wollen wir
a) Ordnung in den Zoo der Logik-Formalismen bringen,
b) ihre Zusammenhänge katalogisieren und
c) sie auf realen Korpora testen (Benchmarking).
Dafür wollen wir das in der AG Kohlhase entwickelte OMDoc/MMT Format nutzen. Dieses verwendet Theoriegraphen sowohl für die modulare Repräsentation von Domänenwissen in logischen Sprachen als auch der Logiken selbst in Meta-Logiken. Zwischenlogische Beziehungen können als Theoriemorphismen – also wahrheitserhaltende Abbildungen zwischen Theorien – dargestellt werden. Das ALMANAC-Projekt strebt an hierfür einen "Logikatlas" zu erstellen, also eine offene Sammlung explizit repräsentierter Formalismen und Frameworks, der als Basis für die Methodenintegration im SPP dienen kann.
Das zweite Ziel des ALMANAC Projekts is es, die Theoriegraphenstruktur zu nutzen um Kontexte in Multi-Agenten-Argumentationen zu modellieren: Theoriegraphen erlauben bereits auf natürliche Weise durch Inklusionen und Interprätationen verbundene "kleine Ontologien" (die Theorien), die intern konsistent sind, aber untereinander widersprüchlich sein können. Um Theoriegraphen zu vollgültigen Arugmentationskontextgraphen zu erweitern wollen wir die Argumentrelationen wie z.B. Attacke, Zurückweisung oder Schwächung hinzufügen und ihre ontologischen Eigenschaften untersuchen.
OMDoc/MMT ist im MMT System implementiert. Dieses fungiert als eine (Meta)-Wissensbank und bietet logische Dienste wie Typ/Beweisprüfung, Logik-Übersetzungen und Browsen von Logik-Korpora. Das System ist eingebettet in das MathHub System das zusätzlich Nutzer- und Korpus-Verwaltungsdienste anbietet und als eine Infrastruktur für Logik-Benchmarks dienen kann (Joint Tasks, das dritte Ziel von ALMANAC). Letztere sollen Synergien zwischen den Projekten des SPP induzieren und so zur Kohärenz des Gesamtunternhemens beitragen.