16 lines
788 B
Markdown
16 lines
788 B
Markdown
# Technical issues
|
|
- Clingo may or may not choose to propagate DL atoms before the ontology tells it to.
|
|
- Symbols for atoms are not always present in the control object (E.g. a rule `a :- a`)
|
|
Current workaround is to use signature (which don't get removed). This may have implications about what can be grounded.
|
|
|
|
- Minimality checking
|
|
- The solver should never "decide" to propagate theory atoms, but it does
|
|
This might be blockable with tagged clauses, but since the solver unifies solver literals with their theory literals, this may block the regular atoms sometimes.
|
|
|
|
|
|
- CLingo unifying the atoms is a big problem
|
|
|
|
|
|
- If theory atoms are false, then it didn't come from ontology
|
|
Maybe this will work:
|
|
if the final model is not minimal, then it can't have come from the ontology |