An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic
This work provides a formal method for researchers in computational argumentation to verify properties of abstract dialectical frameworks, though it is incremental as it builds on existing encoding techniques.
The paper tackles the problem of analyzing abstract dialectical frameworks by encoding them and their semantics into classical higher-order logic, enabling computer-assisted verification and generation of interpretations using proof assistants like Isabelle/HOL.
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.