mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-19 09:29:36 +01:00
38 lines
2.7 KiB
Markdown
38 lines
2.7 KiB
Markdown
 [](https://coveralls.io/github/ellmau/adf-obdd)     
|
|
# 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
|
|
|
|
# Development notes
|
|
To run all the tests placed in the submodule you need to run
|
|
```bash
|
|
$> git submodule init
|
|
```
|
|
at the first time.
|
|
Afterwards you need to update the content of the submodule to be on the currently used revision by
|
|
```bash
|
|
$> git submodule update
|
|
```
|
|
|
|
The tests can be started by using the test-framework of cargo, i.e.
|
|
```bash
|
|
$> cargo test
|
|
```
|
|
Note that some of the instances are quite big and it might take some time to finish all the tests.
|
|
If you do not initialise the submodule, tests will "only" run on the other unit-tests and (possibly forthcoming) other integration tests.
|