mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-19 09:29:36 +01:00
19 lines
1.4 KiB
Markdown
19 lines
1.4 KiB
Markdown
# Solver for ADFs grounded semantics by utilising OBDDs - ordered binary decision diagrams
|
|
|
|
|
|
## Abstract Dialectical Frameworks
|
|
An abstract dialectical framework (ADF) consists of abstract statements. Each statement has an unique label and might be related to other statements (s) in the ADF. This relation is defined by a so-called acceptance condition (ac), which intuitively is a propositional formula, where the variable symbols are the labels of the statements. An interpretation is a three valued function which maps to each statement a truth value (true, false, undecided). We call such an interpretation a model, if each acceptance condition agrees to the interpration.
|
|
## ordered Binary Decision Diagram
|
|
An ordered binary decision diagram is a normalised representation of binary functions, where satisfiability- and validity checks can be done relatively cheap.
|
|
|
|
## Input-file format:
|
|
Each statement is defined by an ASP-style unary predicate s, where the enclosed term represents the label of the statement.
|
|
The binary predicate ac relates each statement to one propositional formula in prefix notation, with the logical operations and constants as follows:
|
|
- and(x,y): conjunction
|
|
- or(x,y): disjunctin
|
|
- iff(x,Y): if and only if
|
|
- xor(x,y): exclusive or
|
|
- neg(x): classical negation
|
|
- c(v): constant symbol "verum" - tautology/top
|
|
- c(f): constant symbol "falsum" - inconsistency/bot
|