A Logic for Veracity: Development and Implementation

TL;DR

This paper develops a formal logic for veracity, addressing trust and authenticity concerns in supply chains, with implementation in Coq to support proof and automation, inspired by organic certification scenarios.

Contribution

It introduces a novel logic for veracity and demonstrates its formalization and implementation in Coq, providing tools for practical verification in supply chain contexts.

Findings

Logic formalization of veracity concepts

Implementation in Coq for proof support

Application to supply chain trust issues

Abstract

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.