Distributed Assertion Management Framework
The Distributed Assertion Management Framework (DAMF) is a proposed collection of formats and techniques to enable heterogeneous formal reasoning systems and users to communicate assertions in a decentralized, reliable, and egalitarian manner. An assertion is a unit of mathematical knowledge—think lemmas, theorems, corollaries, etc.—that is cryptographically signed by its originator.
The philosophy of DAMF is explained in this technical report:
Farah Al Wardani, Kaustuv Chaudhuri, and Dale Miller (2023). Distributing and trusting proof checking: a preliminary report.
The technical construction of DAMF is explained in this draft paper:
Farah Al Wardani, Kaustuv Chaudhuri, and Dale Miller (2023). Formal Reasoning using Distributed Assertions. Submitted: 2023-03-08.
DAMF is based on content-addressable storage using the InterPlanetary File System (IPFS) network, and uses the InterPlanetary Linked Data (IPLD) data model to represent assertions and all their components.
Explore the proposed DAMF Formats.
Read about Processes in DAMF.
Install Dispatch, an intermediary tool that helps in integrating systems.
Experiment with some edge systems. In particular:
- Abella DAMF, a version of Abella with DAMF support.
- λProlog integrated with DAMF.
Read an example walkthrough of using a heterogeneous combination of systems to prove an assertion.