A Logic for Veracity: Development and Implementation
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913441854259200 |
|---|---|
| author | Britten, Daniel Reeves, Steve |
| author_facet | Britten, Daniel Reeves, Steve |
| contents | In the business rules of supply chains, there are concerns around trust, truth, demonstrability and authenticity. These concerns are gathered together under the name ``veracity".
In the work for this paper we were originally motivated by the requirement around organic certification in the wine industry in New Zealand, but veracity arises in many different situations and our formalisation shows how formal methods can give insights into many such practical problems.
One activity for formal methods involves taking informal processes and formalising them and subsequently building tools to support this formalisation and therefore the original processes too, and the work reported here is an example of that.
Here, then, we explore the idea of veracity in this spirit, give highlights of the development of a logic for it and show how that logic can be implemented in Coq, both for proof support and automation. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_16117 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A Logic for Veracity: Development and Implementation Britten, Daniel Reeves, Steve Logic in Computer Science In the business rules of supply chains, there are concerns around trust, truth, demonstrability and authenticity. These concerns are gathered together under the name ``veracity". In the work for this paper we were originally motivated by the requirement around organic certification in the wine industry in New Zealand, but veracity arises in many different situations and our formalisation shows how formal methods can give insights into many such practical problems. One activity for formal methods involves taking informal processes and formalising them and subsequently building tools to support this formalisation and therefore the original processes too, and the work reported here is an example of that. Here, then, we explore the idea of veracity in this spirit, give highlights of the development of a logic for it and show how that logic can be implemented in Coq, both for proof support and automation. |
| title | A Logic for Veracity: Development and Implementation |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2407.16117 |