match Dung frameworks1. The tool ADF-BDD [
We recall basics of Abstract Dialectical Frameworks and refer the interested reader to the recent
Handbook of Formal Argumentation [
Definition 1. An ADF is a triple := (, , ) where is a fixed finite set of statements; ⊆ × is a set of links; and := { }∈ consists of acceptance conditions for statements, which correspond to propositional formulas ::= ∈ | ⊥ | ⊤ | ¬ | ( ∧ ) | ( ∨ ) | ( → ) over the parents () := {′ ∈ | (′, ) ∈ } of statement .
Since links can be determined by acceptance conditions, throughout this paper we will mostly
omit links and simply define ADFs as a tuple consisting of statements and their respective
acceptance conditions. We are following the newly proposed representation ofADFs with
roBDDs [
By representing ADFs as roBDDs the two previous definitions are combined: Definition 3. The BDD representation ℬ() = (ℬ 1 , . . . , ℬ ) of an ADF = (, ) is a tuple consisting of one BDD for each acceptance condition of ∈ where 1 ≤ ≤ = ||.
The semantics of a given ADF are based on three-valued interpretations. Such an interpretation is a function : → {t, f , u} that maps each statement to either true, false, or undecided. We call an interpretation two-valued, denoted by 2, if ∀ ∈ : () ∈ {t, f }. Additionally the information ordering ≤ is defined as the reflexive transitive closure of the relation < with u < for ∈ {t, f }. We lift ≤ and < to interpretations by ′ ≤ if ′() ≤ () for each ∈ , and ′ < if ′ ≤ and for some ∈ we have ′() < (). By ℬ [] := ℬ [/1 : () = t][/0 : () = f ] we define the partial evaluation of ℬ with respect to .
Definition 4. Let = (, ) be an ADF, ℬ() its BDD-representation, and be a threevalued interpretation over . The characteristic operator Γ () = ′ is defined by the revisited interpretation ′ of , such that for each ∈ ⎧t ⎪ ′() = ⎨f ⎪⎩u if the reduced ℬ [] is a tautology (i.e. is a 1 node); if the reduced ℬ [] is an inconsistency (i.e. is a 0 node); otherwise.
We are now in position to define Dung’s standard semantics for ADFs that is currently supported by ADF-BDD.DEV.
Definition 5. Let = (, ) be an ADF, ℬ() its BDD-representation, and a three-valued interpretation. is complete in if = Γ (), and is grounded in if is the least fixed-point of Γ for u with u() = u for each ∈ .
We additionally define the reduced ADF 2 := (2 , 2 ) for a two-valued interpretation (i.e. all statements are mapped to t or f) 2, a where 2 := { ∈ | 2() = t} and 2 := { [′/⊥ : 2(′) = f ] | ∈ 2 , ′ ∈ }. Analogously, we define the corresponding BDD-representation ℬ2 := ℬ[/0 : 2() = f ] and remove all statements and corresponding roBDDs, where 2() = t. Let be the grounded interpretation of ℬ2 , 2 is a stable model of if for all ∈ 2 : 2() = t implies () = t.
(a) Input (b) Parsed (c) Grounded
To analyse an ADF and to illustrate the diferent semantics, it is natural to give a visualisation
of the corresponding roBDD-representation as a graph. The underlying forest of roBDDs
is presented in a single graph marked with multiple root nodes where nodes from diferent
roBDDs are merged whenever possible. For ADF-BDD.DEV, we rely on a state of the art,
feature-rich, web-based library for graph visualisation3 [
The ADF = (, ) in the input in Figure 1a contains four statments, a through d (), represented by the unary predicates s. Its four corresponding acceptance conditions () are represented by the binary predicate ac that relates each statement to the actual condition as follows: (1) a is assumed to be true (“verum”). (2) b is true if b is true (which is self-supporting). (3) c is true if a and b are true. (4) d is true if b is not true. We use a common syntactic representation for ADFs [14, 15], first introduced by [ 16] and described in detail later [17]. In the future, we also plan to incorporate graphical ADF editing.
Figure 1b shows the roBDD representation ℬ() for as a forest of the underlying roBDDs with merged nodes as described above. The visualisation helps to see how the truth value of a statement depends on other statements by starting at the root for and then following the possible paths to the top. To simplify the indentification of a subtree that belongs to a statement, our ADF-BDD.DEV visualisation allows to hightlight those trees by clicking the “root” nodes 3G6 - https://g6.antv.antgroup.com/en/ 4Dagre original implementation https://github.com/dagrejs/dagre (and all other nodes as well). For instance, the root for a is directly at the “TOP” (i.e. 1) node, which indicates that a is true. To obtain the truth value for c, we start at the bottom left node. If a is known to be false, we follow the orange path, which is the low-edge in the roBDD, yielding that c is false as well. The blue path corresponds to the high-edge in the roBDD and represents the case, where a is true. Then, if b is also true, we find that c is true. Unsurprisingly, this direcly corresponds to acceptance condition (3) above.
The intuitive procedure of determining truth values iteratively by following paths and pluging in known values into the nodes of the roBDDs is exactly what is done by the characteristic operator Γ . Since we intuitively start with the interpretation u where all statements are undecided, this procedure gives us the grounded interpretation ground for . The grounded interpretation (and the other semantics introduced in Section 2) can again be visualised with ADF-BDD.DEV. Figure 1c shows the partial evaluation of ℬ() with respect to ground. This representation allows to debug the ADF and to analyse why some statements are still undecided. One can see that the statements b and c are still dependent on the outcome of b. In addition, it is also shown that whatever the result for b and c will be, statement d will behave with the inverse truth value. This is an important step in understanding and explaining further results and semantics and allows a way to directly address yet undecided truth-value assignments and their reasons.
In general there can be done various graphical deductions, based on given ADFs. One example is that for an roBDD-representation where no statement is either ’TOP’ or ’BOT’ the grounded interpretation will not have any accepted or rejected statements. Another one is that for big instances it can be easily checked if the reasoning structure is flat or deep. The wider the width of a deep structure is, the more the values of variables interplay into deciding the acceptance of a related statement. To the best of our knowledge, this is the first work to give this kind of insight.
In the future, we plan to further improve user experience on ADF-BDD.DEV. For example, we want to allow graphical editing of ADFs instead of only text based input and we want to allow to edit the produced roBDD representation directly. As a long term goal, the graphical editing can be enhanced with on-the-fly analysis and other advanced features to provide a fully-fledged “IDE” for ADF editing. Furthermore, better tooltips and hints shall assist even untrained users to become familiar with ADFs and their sematics by making use of the roBDD presentation in a didactic fashion. In its current form, we are convinced that ADF-BDD.DEV simplifies debugging of ADFs for individuals that are already familiar with ADFs. Looking further, we think that our powerfully backed yet easy to access tool ADF-BDD.DEV bears great potential for making work on ADFs more approachable for already experienced users but also for newcomers that want to get some first hands-on experience.
This work was supported in DFG grant 389792660 (TRR 248), by BMBF in grants ITEA-01IS21084 (InnoSale), and in DAAD grant 57616814 (SECAI).
Note that this work has already been presented at the “Fourth Workshop on Explainable Logic-Based Knowledge Representation” (XLoKR 2023), co-located with the 20th International Conference on Principles of Knowledge Representation and Reasoning [18]. M. Jünger, S. Leipert (Eds.), Graph Drawing, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 2002, pp. 31–44. doi:10.1007/3-540-45848-4_3. [13] G. Sander, Layout of compound directed graphs, workingPaper, 1996. URL: https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/25862. doi:10.22028/ D291-25806, accepted: 2005-06-23. [14] G. Brewka, M. Diller, G. Heissenberger, T. Linsbichler, S. Woltran, Solving advanced argumentation problems with answer set programming, TPLP 20 (2020) 391–431. [15] T. Linsbichler, M. Maratea, A. Niskanen, J. P. Wallner, S. Woltran, Advanced algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving, Artif. Intell. 307 (2022) 103697. [16] S. Ellmauthaler, J. P. Wallner, Evaluating Abstract Dialectical Frameworks with ASP, in: B. Verheij, S. Szeider, S. Woltran (Eds.), Proc. COMMA, volume 245, IOS Press, 2012, pp. 505–506. [17] S. Ellmauthaler, H. Straß, The DIAMOND system for argumentation: Preliminary report, in: M. Fink, Y. Lierler (Eds.), Proceedings of the Sixth International Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP), 2013. [18] S. Ellmauthaler, L. Gerlach, Adf-bdd.dev: Debug abstract dialectical frameworks with binary decision diagrams, in: The Fourth Workshop on Explainable Logic-Based Knowledge Representation (XLoKR 2023), 2023. URL: https://iccl.inf.tu-dresden.de/w/images/b/b4/ Xlokr-2023-ellmauthaler-gerlach-submission2105.pdf.