# An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic

arXiv: https://arxiv.org/abs/2312.08375 · HTML: https://mlsanity.com/paper/2312.08375/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 52 references that are in the map.
- First posted on arXiv 8 Dec 2023.

## Builds on (most cited first, 2 of 2)

- [Extensional Higher-Order Paramodulation in Leo-III](https://mlsanity.com/paper/1907.11501/) (2019)
- [A Formalisation of Abstract Argumentation in Higher-Order Logic](https://mlsanity.com/paper/2110.09174/) (2021)

## Abstract (arXiv)

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.