An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic

• URL: http://arxiv.org/abs/2312.08375v1
• Date: Fri, 8 Dec 2023 09:32:26 GMT
• Title: An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic
• Authors: Antoine Martina, Alexander Steen
• Abstract summary: This approach allows for the computer-assisted analysis of abstract dialectical frameworks. Exemplary applications include the formal analysis and verification of meta-theoretical properties.
• Score: 57.24311218570012
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: An approach for encoding abstract dialectical frameworks and their semantics into classical higher-order logic is presented. Important properties and semantic relationships are formally encoded and proven using the proof assistant Isabelle/HOL. This approach allows for the computer-assisted analysis of abstract dialectical frameworks using automated and interactive reasoning tools within a uniform logic environment. Exemplary applications include the formal analysis and verification of meta-theoretical properties, and the generation of interpretations and extensions under specific semantic constraints.

Related papers

• A Note on an Inferentialist Approach to Resource Semantics [48.65926948745294]
  'Inferentialism' is the view that meaning is given in terms of inferential behaviour. This paper shows how 'inferentialism' enables a versatile and expressive framework for resource semantics.
  arXiv  Detail & Related papers  (2024-05-10T14:13:21Z)
• Inferentialist Resource Semantics [48.65926948745294]
  This paper shows how inferentialism enables a versatile and expressive framework for resource semantics. How inferentialism seamlessly incorporates the assertion-based approach of the logic of Bunched Implications. This integration enables reasoning about shared and separated resources in intuitive and familiar ways.
  arXiv  Detail & Related papers  (2024-02-14T14:54:36Z)
• A Unifying Framework for Learning Argumentation Semantics [50.69905074548764]
  We present a novel framework, which uses an Inductive Logic Programming approach to learn the acceptability semantics for several abstract and structured argumentation frameworks in an interpretable way. Our framework outperforms existing argumentation solvers, thus opening up new future research directions in the area of formal argumentation and human-machine dialogues.
  arXiv  Detail & Related papers  (2023-10-18T20:18:05Z)
• Modeling Hierarchical Reasoning Chains by Linking Discourse Units and Key Phrases for Reading Comprehension [80.99865844249106]
  We propose a holistic graph network (HGN) which deals with context at both discourse level and word level, as the basis for logical reasoning. Specifically, node-level and type-level relations, which can be interpreted as bridges in the reasoning process, are modeled by a hierarchical interaction mechanism.
  arXiv  Detail & Related papers  (2023-06-21T07:34:27Z)
• Modeling and Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy [0.0]
  This article presents a semantical embedding for public announcement logic with relativized common knowledge. It enables the first-time automation of this logic with off-the-shelf theorem provers for classical higher-order logic. The work constitutes an important addition to the pluralist LogiKEy knowledge engineering methodology.
  arXiv  Detail & Related papers  (2021-11-02T15:14:52Z)
• A Formalisation of Abstract Argumentation in Higher-Order Logic [77.34726150561087]
  We present an approach for representing abstract argumentation frameworks based on an encoding into classical higher-order logic. This provides a uniform framework for computer-assisted assessment of abstract argumentation frameworks using interactive and automated reasoning tools.
  arXiv  Detail & Related papers  (2021-10-18T10:45:59Z)
• Public Announcement Logic in HOL [0.0]
  shallow semantical embedding for public announcement logic with relativized common knowledge is presented. This embedding enables the first-time automation of this logic with off-the-shelf theorem provers for classical higher-order logic.
  arXiv  Detail & Related papers  (2020-10-02T06:46:02Z)
• Higher-order Logic as Lingua Franca -- Integrating Argumentative Discourse and Deep Logical Analysis [0.0]
  We present an approach towards the deep, pluralistic logical analysis of argumentative discourse. We use state-of-the-art automated reasoning technology for classical higher-order logic.
  arXiv  Detail & Related papers  (2020-07-02T11:07:53Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.