pith. sign in

arxiv: 2312.08375 · v1 · submitted 2023-12-08 · 💻 cs.LO · cs.AI

An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic

Antoine Martina , Alexander Steen This is my paper

Pith reviewed 2026-05-24 05:27 UTC · model grok-4.3

classification 💻 cs.LO cs.AI
keywords abstract dialectical frameworkshigher-order logicIsabelle/HOLsemantics encodingformal verificationproof assistantargumentation frameworks
0
0 comments X

The pith

Abstract dialectical frameworks and their semantics can be encoded into classical higher-order logic for formal analysis in Isabelle/HOL.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how to translate abstract dialectical frameworks together with their acceptance conditions and semantics into statements of classical higher-order logic. These translations are then expressed and mechanically checked inside the Isabelle/HOL proof assistant. The resulting setup lets users apply both automated and interactive reasoning tools to the same logical representation. A reader would care because it turns informal reasoning about non-monotonic argumentation into machine-checked statements that can be reused across different analyses.

Core claim

An encoding maps each abstract dialectical framework to a collection of higher-order logic formulas whose models correspond exactly to the interpretations and extensions under the chosen semantics; important meta-theoretic relationships are stated as HOL theorems and proved inside Isabelle/HOL.

What carries the argument

The encoding function that turns an abstract dialectical framework into higher-order logic formulas while preserving its semantics.

If this is right

  • Meta-theoretical properties of abstract dialectical frameworks become machine-checkable statements.
  • Interpretations and extensions can be generated automatically by invoking HOL reasoners under given semantic constraints.
  • All analyses occur inside one uniform higher-order logic environment rather than separate specialized tools.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same encoding pattern could be applied to other structured argumentation systems that admit a declarative semantics.
  • Once the encoding exists, existing libraries of HOL lemmas about lattices or fixed points become directly usable for argumentation problems.

Load-bearing premise

The chosen mapping from abstract dialectical frameworks to higher-order logic formulas correctly preserves the original acceptance conditions and semantics.

What would settle it

A concrete abstract dialectical framework together with an interpretation that satisfies the encoded higher-order logic statements but fails to satisfy the original framework's semantics under the same conditions.

Figures

Figures reproduced from arXiv: 2312.08375 by Alexander Steen, Antoine Martina.

Figure 1
Figure 1. Figure 1: Visualisation of an example ADF taken from [16, Example 3.2]. [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The proof of Lemma 1 in Isabelle/HOL. v : X ⊆ S −→ {t,f}, with elements of S \ X being interpreted as u. Three-valued interpretations are thus encoded by two objects, a set X and a mapping v. X is then a term of type ′ s Set corresponding to the set containing the statements mapped to either t or f by the interpretation, and v is then a term of type ′ s ⇒ o corresponding to the actual mapping of the statem… view at source ↗
Figure 3
Figure 3. Figure 3: Relations between ADF semantics, following [16]. Arrows represent inclu [PITH_FULL_IMAGE:figures/full_fig_p021_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Counter-example generation using Nitpick for an invalid inclusion state [PITH_FULL_IMAGE:figures/full_fig_p022_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Isabelle/HOL source file after encoding the ADF example from Fig. 1. [PITH_FULL_IMAGE:figures/full_fig_p024_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: An example AF. – v1 := λs. s = a ∨ s = b ∨ s = c – v2 := λs. s = a ∨ s = d – v3 := λs. s = a – v4 := λs. ⊥ – X3 := λs. s = a – X4 := λs. s = a Finally, it can be established that the above encoded interpretations behave as expected: – v1 and v2 are models, i.e., modelS,L,C v1 and modelS,L,C v2. – No other two-valued model can be found: No model can be found for (modelS,L,C w)∧ ¬(w = v1) ∧ ¬(w = v2) – v1, v… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The manuscript presents an encoding of abstract dialectical frameworks (ADFs), their interpretations, and the standard semantics (admissible, complete, preferred, grounded, stable) into classical higher-order logic inside the Isabelle/HOL proof assistant. Machine-checked proofs are supplied for the encoded operators and for the expected meta-theoretic relationships among the semantics; exemplary applications include verification of properties and generation of extensions under semantic constraints.

Significance. The work supplies a uniform HOL environment in which ADF analysis can exploit both automated and interactive reasoning. The machine-checked proofs constitute a concrete strength: once the HOL definitions are accepted as faithful, the internal consistency and preservation claims are discharged by the assistant rather than by hand.

minor comments (2)
  1. [Introduction] The introduction would benefit from a short comparison table or paragraph situating the HOL encoding against existing formalizations of ADFs or AFs in other proof assistants.
  2. [§3] Notation for the lifting of acceptance conditions into HOL predicates (around the definition of the characteristic operator) could be accompanied by one additional explanatory sentence for readers less familiar with Isabelle syntax.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive review and the recommendation to accept the manuscript. The summary accurately captures the contribution of encoding ADFs and their semantics into HOL with machine-checked proofs in Isabelle/HOL.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines an explicit encoding of ADFs, interpretations, and standard semantics (admissible, complete, preferred, grounded, stable) into Isabelle/HOL, then supplies machine-checked proofs that the encoded operators and extension sets satisfy the expected meta-theoretic relationships. Because the proofs are performed inside the proof assistant, the derivation is self-contained; the only external requirement is that the HOL definitions faithfully reproduce the original mathematical definitions of ADFs, which is discharged by the formalization itself rather than by any self-referential fit, ansatz, or self-citation chain. No step reduces to its inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper's contribution is the encoding itself, resting on standard mathematical axioms of HOL and the assumption that the encoding is faithful. No free parameters or invented entities are indicated in the abstract.

axioms (1)
  • standard math The soundness and consistency of higher-order logic as implemented in Isabelle/HOL
    The proofs rely on the underlying logic being sound.

pith-pipeline@v0.9.0 · 5583 in / 1079 out tokens · 31433 ms · 2026-05-24T05:27:03.931934+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

52 extracted references · 52 canonical work pages

  1. [1]

    Handling Inconsistency with Preference-Based Argumentation

    Leila Amgoud and Srdjan Vesic. Handling Inconsistency with Preference-Based Argumentation. InInternational Conference on Scalable Uncertainty Management, pages 56–69, 2010

    work page 2010

  2. [2]

    A QBF-based formalization of abstract argumentation semantics.Journal of Applied Logic, 11(2):229–252, 2013

    Ofer Arieli and Martin WA Caminada. A QBF-based formalization of abstract argumentation semantics.Journal of Applied Logic, 11(2):229–252, 2013

    work page 2013

  3. [3]

    Abstract Argu- mentation Frameworks and Their Semantics

    Pietro Baroni, Martin Caminada, and Massimiliano Giacomin. Abstract Argu- mentation Frameworks and Their Semantics. In Pietro Baroni, Dov M. Gabbay, Massimiliano Giacomin, and Leendert van der Torre, editors,Handbook of Formal Argumentation, pages 159–236. College Publications, 2018

    work page 2018

  4. [4]

    SCC-recursiveness: A general schema for argumentation semantics.Artificial Intelligence, 168(1-2):162– 210, 2005

    Pietro Baroni, Massimiliano Giacomin, and Giovanni Guida. SCC-recursiveness: A general schema for argumentation semantics.Artificial Intelligence, 168(1-2):162– 210, 2005

    work page 2005

  5. [5]

    On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n- person games: 25 years later.Argument Comput., 11(1-2):1–14, 2020

    Pietro Baroni, Francesca Toni, and Bart Verheij. On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n- person games: 25 years later.Argument Comput., 11(1-2):1–14, 2020

    work page 2020

  6. [6]

    Clark Barrett, Christopher L Conway, Morgan Deters, Liana Hadarean, Dejan Jo- vanović, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. InInternational Conference on Computer Aided Verification, pages 171–177, 2011

    work page 2011

  7. [7]

    A software system using a SAT solver for reasoning under complete, stable, preferred, and grounded argumenta- tion semantics

    Christoph Beierle, Florian Brons, and Nico Potyka. A software system using a SAT solver for reasoning under complete, stable, preferred, and grounded argumenta- tion semantics. In Joint German/Austrian Conference on Artificial Intelligence (Künstliche Intelligenz), pages 241–248, 2015

    work page 2015

  8. [8]

    Church’s Type Theory.Stanford En- cyclopedia of Philosophy, pages 1–62, 2019

    Christoph Benzmüller and Peter Andrews. Church’s Type Theory.Stanford En- cyclopedia of Philosophy, pages 1–62, 2019

    work page 2019

  9. [9]

    Automation of higher-order logic

    Christoph Benzmüller and Dale Miller. Automation of higher-order logic. In Dov M. Gabbay, Jörg H. Siekmann, and John Woods, editors,Handbook of the History of Logic, Volume 9 — Computational Logic, pages 215–254. North Hol- land, Elsevier, 2014

    work page 2014

  10. [10]

    Designing nor- mative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support.Artificial intelligence, 287:103348, 2020

    Christoph Benzmüller, Xavier Parent, and Leendert van der Torre. Designing nor- mative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support.Artificial intelligence, 287:103348, 2020

    work page 2020

  11. [11]

    Checking the acceptability of a set of ar- guments

    Philippe Besnard and Sylvie Doutre. Checking the acceptability of a set of ar- guments. In Proceedings of the 10th International Workshop on Non-Monotonic Reasoning (NMR 2004), pages 59–64, 2004

    work page 2004

  12. [12]

    IOS Press, 2009

    Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors.Handbook of Satisfiability, volume 185 ofFrontiers in Artificial Intelligence and Applications. IOS Press, 2009. An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic 29

    work page 2009

  13. [13]

    Extending Sledgehammer with SMT Solvers.Journal of automated reasoning, 51(1):109–128, 2013

    Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C Paulson. Extending Sledgehammer with SMT Solvers.Journal of automated reasoning, 51(1):109–128, 2013

    work page 2013

  14. [14]

    Nitpick: A Counterexample Gen- eratorforHigher-OrderLogicBasedonaRelationalModelFinder

    Jasmin Christian Blanchette and Tobias Nipkow. Nitpick: A Counterexample Gen- eratorforHigher-OrderLogicBasedonaRelationalModelFinder. In International Conference on Interactive Theorem Proving, pages 131–146, 2010

    work page 2010

  15. [15]

    Weighted Abstract Dialectical Frameworks through the Lens of Approximation Fixpoint Theory.Proceedings of the AAAI Conference on Artificial Intelligence, 33(01):2686–2693, 2019

    Bart Bogaerts. Weighted Abstract Dialectical Frameworks through the Lens of Approximation Fixpoint Theory.Proceedings of the AAAI Conference on Artificial Intelligence, 33(01):2686–2693, 2019

    work page 2019

  16. [16]

    Wallner, and StefanWoltran

    Gerhard Brewka, Stefan Ellmauthaler, Hannes Strass, Johannes P. Wallner, and StefanWoltran. Abstractdialecticalframeworks. InPietroBaroni,DovM.Gabbay, Massimiliano Giacomin, and Leendert van der Torre, editors,Handbook of formal argumentation, pages 237–285. College Publications, 2018

    work page 2018

  17. [17]

    Abstract dialectical frameworks revisited

    Gerhard Brewka, Stefan Ellmauthaler, Hannes Strass, Johannes Peter Wallner, and Stefan Woltran. Abstract dialectical frameworks revisited. InProceedings of the Twenty-Third international joint conference on Artificial Intelligence, pages 803–809, 2013

    work page 2013

  18. [18]

    Abstract Dialectical Frameworks Revisited

    Gerhard Brewka, Stefan Ellmauthaler, Hannes Strass, Johannes Peter Wallner, and Stefan Woltran. Abstract Dialectical Frameworks Revisited. InProceedings of the Twenty-Third international joint conference on Artificial Intelligence, pages 803–809, 2013

    work page 2013

  19. [19]

    Weighted AbstractDialecticalFrameworks

    Gerhard Brewka, Hannes Strass, Johannes Wallner, and Stefan Woltran. Weighted AbstractDialecticalFrameworks. Proceedings of the AAAI Conference on Artificial Intelligence, 32(1), 2018

    work page 2018

  20. [20]

    Abstract Dialectical Frameworks

    Gerhard Brewka and Stefan Woltran. Abstract Dialectical Frameworks. InPro- ceedings of the Twelfth International Conference on Principles of Knowledge Rep- resentation and Reasoning, pages 102–111, 2010

    work page 2010

  21. [21]

    Logical Encoding of Argumentation Frameworks with Higher-order Attacks and Evidential Sup- ports

    Claudette Cayrol and Marie-Christine Lagasquie-Schiex. Logical Encoding of Argumentation Frameworks with Higher-order Attacks and Evidential Sup- ports. International Journal on Artificial Intelligence Tools, 29(03n04):2060003:1– 2060003:50, 2020

    work page 2020

  22. [22]

    Foun- dations of implementations for formal argumentation.IfCoLog Journal of Logics and their Applications, 4(8):2623–2705, 2017

    Federico Cerutti, Sarah A Gaggl, Matthias Thimm, and Johannes Wallner. Foun- dations of implementations for formal argumentation.IfCoLog Journal of Logics and their Applications, 4(8):2623–2705, 2017

    work page 2017

  23. [23]

    An Efficient Java- Based Solver for Abstract Argumentation Frameworks: jArgSemSAT

    Federico Cerutti, Mauro Vallati, and Massimiliano Giacomin. An Efficient Java- Based Solver for Abstract Argumentation Frameworks: jArgSemSAT. Inter- national Journal on Artificial Intelligence Tools, 26(02):1750002:1—-1750002:26, 2017

    work page 2017

  24. [24]

    A formulation of the simple theory of types.Journal of Symbolic Logic, 5(2):56–68, 1940

    Alonzo Church. A formulation of the simple theory of types.Journal of Symbolic Logic, 5(2):56–68, 1940

    work page 1940

  25. [25]

    Argumentation update in YALLA (Yet Another Logic Language for Argumentation)

    Florence Dupin de Saint-Cyr, Pierre Bisquert, Claudette Cayrol, and Marie- Christine Lagasquie-Schiex. Argumentation update in YALLA (Yet Another Logic Language for Argumentation). International Journal of Approximate Reasoning, 75:57–92, 2016

    work page 2016

  26. [26]

    Approximations, Stable Operators, Well-Founded Fixpoints and Applications in Nonmonotonic Reasoning

    Marc Denecker, Victor W Marek, and Mirosław Truszczyński. Approximations, Stable Operators, Well-Founded Fixpoints and Applications in Nonmonotonic Reasoning. In Logic-Based Artificial Intelligence, pages 127–144, 2000

    work page 2000

  27. [27]

    Ultimate approx- imation and its application in nonmonotonic knowledge representation systems

    Marc Denecker, Victor W Marek, and Mirosław Truszczyński. Ultimate approx- imation and its application in nonmonotonic knowledge representation systems. Information and Computation, 192(1):84–121, 2004. 30 A. Martina and A. Steen

    work page 2004

  28. [28]

    Reasoning in ab- stract dialectical frameworks using quantified boolean formulas.Argument Com- put., 6(2):149–177, 2015

    Martin Diller, Johannes Peter Wallner, and Stefan Woltran. Reasoning in ab- stract dialectical frameworks using quantified boolean formulas.Argument Com- put., 6(2):149–177, 2015

    work page 2015

  29. [29]

    On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games

    Phan Minh Dung. On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artificial intelligence, 77(2):321–357, 1995

    work page 1995

  30. [30]

    Coherence in finite argument systems

    Paul E Dunne and Trevor JM Bench-Capon. Coherence in finite argument systems. Artificial Intelligence, 141(1-2):187–203, 2002

    work page 2002

  31. [31]

    Stage semantics and the SCC- recursive schema for argumentation semantics.Journal of Logic and Computation, 26(4):1149–1202, 2014

    Wolfgang Dvořák and Sarah Alice Gaggl. Stage semantics and the SCC- recursive schema for argumentation semantics.Journal of Logic and Computation, 26(4):1149–1202, 2014

    work page 2014

  32. [32]

    Complexity-sensitive decision procedures for abstract argumentation

    Wolfgang Dvořák, Matti Järvisalo, Johannes Peter Wallner, and Stefan Woltran. Complexity-sensitive decision procedures for abstract argumentation. Artificial Intelligence, 206:53–78, 2014

    work page 2014

  33. [33]

    Reasoning in Argumentation Frameworks Using Quantified Boolean Formulas.Computational Models of Argument: Proceedings of COMMA, 6:133–144, 2006

    Uwe Egly and Stefan Woltran. Reasoning in Argumentation Frameworks Using Quantified Boolean Formulas.Computational Models of Argument: Proceedings of COMMA, 6:133–144, 2006

    work page 2006

  34. [34]

    The DIAMOND system for computing with abstract dialectical frameworks

    Stefan Ellmauthaler and Hannes Strass. The DIAMOND system for computing with abstract dialectical frameworks. In COMMA, volume 266 of Frontiers in Artificial Intelligence and Applications, pages 233–240. IOS Press, 2014

    work page 2014

  35. [35]

    College Publications, 2013

    Dov M Gabbay.Meta-logical Investigations in Argumentation Networks, volume 44 of Studies in Logic – Mathematical Logic and Foundations. College Publications, 2013

    work page 2013

  36. [36]

    On the Decomposition of Abstract Dialectical Frameworks and the Complexity of Naive-based Semantics

    Sarah Alice Gaggl, Sebastian Rudolph, and Hannes Strass. On the Decomposition of Abstract Dialectical Frameworks and the Complexity of Naive-based Semantics. Journal of Artificial Intelligence Research, 70:1–64, 2021

    work page 2021

  37. [37]

    Completeness in the theory of types

    Leon Henkin. Completeness in the theory of types. Journal of Symbolic Logic, 15(2):81–91, 1950

    work page 1950

  38. [38]

    Advancedalgorithmsforabstractdialecticalframeworksbased on complexity analysis of subclasses and SAT solving.Artif

    Thomas Linsbichler, Marco Maratea, Andreas Niskanen, Johannes Peter Wallner, andStefanWoltran. Advancedalgorithmsforabstractdialecticalframeworksbased on complexity analysis of subclasses and SAT solving.Artif. Intell., 307:103697, 2022

    work page 2022

  39. [39]

    An Encoding of Abstract Dialectical Frameworks into Higher- Order Logic

    Antoine Martina. An Encoding of Abstract Dialectical Frameworks into Higher- Order Logic. Supplemental material to the article: Isabelle/HOL sources files

    work page

  40. [40]

    Z3: An Efficient SMT Solver

    Leonardo de Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. InInter- national Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340, 2008

    work page 2008

  41. [41]

    Isabelle/HOL: A Proof Assistant for Higher-Order Logic

    Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science 2283. Springer, 2002

    work page 2002

  42. [42]

    E – a brainiac theorem prover.AI Communications, 15(2-3):111– 126, 2002

    Stephan Schulz. E – a brainiac theorem prover.AI Communications, 15(2-3):111– 126, 2002

    work page 2002

  43. [43]

    Springer, 2009

    Guillermo Ricardo Simari and Iyad Rahwan, editors.Argumentation in Artificial Intelligence. Springer, 2009

    work page 2009

  44. [44]

    Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III.KI-Künstliche Intelligenz, 34(1):105–108, 2020

    Alexander Steen. Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III.KI-Künstliche Intelligenz, 34(1):105–108, 2020

    work page 2020

  45. [45]

    Extensional Higher-Order Paramod- ulation in Leo-III.Journal of Automated Reasoning, 65(6):775–807, 2021

    Alexander Steen and Christoph Benzmüller. Extensional Higher-Order Paramod- ulation in Leo-III.Journal of Automated Reasoning, 65(6):775–807, 2021

    work page 2021

  46. [46]

    A Formalisation of Abstract Argumenta- tion in Higher-Order Logic.Journal of Logic and Computation, 09 2023

    Alexander Steen and David Fuenmayor. A Formalisation of Abstract Argumenta- tion in Higher-Order Logic.Journal of Logic and Computation, 09 2023. exac027. An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic 31

    work page 2023

  47. [47]

    Approximating operators and semantics for abstract dialectical frameworks

    Hannes Strass. Approximating operators and semantics for abstract dialectical frameworks. Artificial Intelligence, 205:39–70, 2013

    work page 2013

  48. [48]

    Analyzing the computational complex- ity of abstract dialectical frameworks via approximation fixpoint theory.Artificial Intelligence, 226:34–74, 2015

    Hannes Strass and Johannes Peter Wallner. Analyzing the computational complex- ity of abstract dialectical frameworks via approximation fixpoint theory.Artificial Intelligence, 226:34–74, 2015

    work page 2015

  49. [49]

    Argumentation and Answer Set Program- ming

    Francesca Toni and Marek Sergot. Argumentation and Answer Set Program- ming. Logic Programming, Knowledge Representation, and Nonmonotonic Rea- soning, pages 164–180, 2011

    work page 2011

  50. [50]

    Advanced SAT techniques for abstract argumentation

    Johannes Peter Wallner, Georg Weissenbacher, and Stefan Woltran. Advanced SAT techniques for abstract argumentation. InInternational Workshop on Com- putational Logic in Multi-Agent Systems, pages 138–154, 2013

    work page 2013

  51. [51]

    Markus Wenzel and Lawrence C. Paulson. Isabelle/isar. InThe Seventeen Provers of the World, volume 3600 ofLecture Notes in Computer Science, pages 41–49. Springer, 2006

    work page 2006

  52. [52]

    An Argumentation-Based Approach to Han- dling Inconsistencies in DL-Lite

    Xiaowang Zhang and Zuoquan Lin. An Argumentation-Based Approach to Han- dling Inconsistencies in DL-Lite. InAnnual Conference on Artificial Intelligence, pages 615–622, 2009

    work page 2009