Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2310.01626 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909461742878720 |
|---|---|
| author | Cabalar, Pedro Muñiz, Brais |
| author_facet | Cabalar, Pedro Muñiz, Brais |
| contents | In this note, we introduce the notion of support graph to define explanations for any model of a logic program. An explanation is an acyclic support graph that, for each true atom in the model, induces a proof in terms of program rules represented by labels. A classical model may have zero, one or several explanations: when it has at least one, it is called a justified model. We prove that all stable models are justified whereas, in general, the opposite does not hold, at least for disjunctive programs. We also provide a meta-programming encoding in Answer Set Programming that generates the explanations for a given stable model of some program. We prove that the encoding is sound and complete, that is, there is a one-to-one correspondence between each answer set of the encoding and each explanation for the original stable model. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_01626 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Model Explanation via Support Graphs Cabalar, Pedro Muñiz, Brais Logic in Computer Science In this note, we introduce the notion of support graph to define explanations for any model of a logic program. An explanation is an acyclic support graph that, for each true atom in the model, induces a proof in terms of program rules represented by labels. A classical model may have zero, one or several explanations: when it has at least one, it is called a justified model. We prove that all stable models are justified whereas, in general, the opposite does not hold, at least for disjunctive programs. We also provide a meta-programming encoding in Answer Set Programming that generates the explanations for a given stable model of some program. We prove that the encoding is sound and complete, that is, there is a one-to-one correspondence between each answer set of the encoding and each explanation for the original stable model. |
| title | Model Explanation via Support Graphs |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2310.01626 |