ALMANAC: Argumentation Logics Manager & Argument Context Graph

决策情况要求个人和组织在基于事实、观点和关于手头情况或类似情况的论点的多种选择之间进行选择。目前的支持系统大多是基于事实的，没有考虑到网络或文献中的论点。SPP聚集了一个研究社区，他们为人类交流中的各种复杂和不精确的描述开发了健壮和可扩展的模型。拟议的年鉴项目旨在支持该企业以逻辑为基础的支柱。在知识、推理和论证的表示方面已经有了大量的前期工作，SPP无疑还会进一步发展。拟议的年鉴项目的第一个目标是提供一个统一的基础设施，以便SPP项目和更广泛的社区能够互操作、比较结果并创建联合逻辑资源。具体地说，我们建议a)将提出的形式主义纳入动物园，b)对它们的相互关系进行分类，c)以现实世界的企业为基准为此，Almanac项目建议使用由提出者的研究小组开发的OMDoc/MMT框架。该框架使用理论图对逻辑语言中的领域知识进行模块化表示，并使用元逻辑中的逻辑形式化本身。逻辑之间的关系可以被建模为理论-态射：理论之间的真理保持映射。年鉴项目希望为SPP提供一个“逻辑图谱”，作为明确表示的形式主义和框架的资源，可以作为方法集成的基础。拟议的年鉴项目的第二个目标是利用理论图结构作为多智能体论证中的上下文模型：理论图自然地提供可以相互排斥并通过包含和视图(在OMDoc/MMT中)相互联系的“小本体”(理论)。OMDoc/MMT由MMT系统实现，作为(元)知识库，提供类型/证明检查、逻辑间翻译和人性化的语料库浏览等逻辑服务。MMT被整合到MathHub系统中，该系统还提供了用户和逻辑语料库管理设施，可作为基于逻辑的挑战(联合任务；年鉴的第三个目标)的基础，从而在战略计划项目之间产生协同作用，从而促进整体努力的一致性。

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 ar- gumentations 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 toa) bring order into the zoo of proposed formalisms,b) categorize their inter-relations, andc) benchmark them on real-world corporaFor 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.