ALMANAC

Decision situations require individuals and organizations to choose between a multitude of options based on facts, opinions, and arguments about the situation at hand or similar ones. Current support systems are mostly fact-based and fail to take into account arguments found on the web or in the literature.

The SPP brings together a community of researchers who develop robust and scalable models for argumentations in human communication in all their complexity and imprecision. The proposed ALMANAC project aims to support the logic-based pillar of this enterprise. There is already a large set of prior work on the representation of knowledge, inference, and argumentations and the SPP will no doubt develop more.

The first objective of the proposed ALMANAC project is to provide a unifying infrastructure so that the SPP projects and wider community can interoperate, compare results, and create joint logic resources.

Concretely we propose to

a) bring order into the zoo of proposed formalisms,

b) categorize their inter-relations, and

c) benchmark them on real-world corpora

For this the ALMANAC project proposes to utilize the OMDoc/MMT framework developed by the proposer’s research group. The framework uses theory graphs for the modular representation of domain knowledge in logical languages and for logical formalisms themselves in meta-logics. Inter-logic relations can be modelled as theory-morphisms: truth-preserving mappings between theories. The ALMANAC project wants to provide the SPP with a “logic atlas” as a resource of explicitly represented formalisms and frameworks that can serve as a basis for integration of methods.

The second objective of the proposed ALMANAC project is to utilize the theory graph structure as a model for the contexts in multi-agent argumentations: theory graphs naturally provide “little ontologies” (the theories) that can be mutually exclusive and are interconnected by inclusions and views (in OMDoc/MMT). To augment them to full argumentation context graphs we want to add argumentation relations like attack, rebut, support, and undercut and study their ontological properties.

OMDoc/MMT is implemented by the MMT system, which serves as a (meta)-knowledge base and offers logical services like type/proof checking, inter-logic translation, and human-oriented browsing of corpora. MMT is integrated into the MathHub system which additionally offers user- and logic-corpus management facilities and can serve as the basis for logic-based challenges (Joint Tasks; the third objective of ALMANAC) that induce synergies between projects in the SPP and thus contribute to the coherence of the overall endeavor.