A Logic for Veracity: Development and Implementation
Daniel Britten, Steve Reeves
TL;DR
The paper tackles veracity in supply chains by proposing a formal, intuitionistic logic that links veracity claims to witnesses and supports multi-agent trust with weighted relations. It develops core constructs for combining and choosing claims, and for reasoning under assumptions, then extends the framework to multiple actors with explicit trust relationships. The authors implement a mechanised version in Coq using a dependent inductive type for proof trees, and provide methods to render proofs in LaTeX and natural language, alongside a plan for semi-automated proof construction. The work aims to provide practical, verifiable foundations and tooling for applications such as organic-certification workflows, enabling reliable verification of information integrity across complex supply chains.
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.