Compiling

This project has been compiled using The Coq Proof Assistant, version 8.16.0, running on Ubuntu 22.04.1 LTS.

This project can be compiled by calling make at the root. HTML documentation is generated by calling make doc at the root. The generated HTML files will be found in a directory ./docs/coqdoc/.

Note that the proof scripts make heavy use of UTF8 symbols. Such symbols also appear repeatedly in the documentation. We thus recommend browsing our proof on a system with comprehensive UTF8 support.

Documentation

Here is the documentation of the various files:

• notations: Some generic notations used throughout the development.
• list_tools: Generic predicates and operations on lists, and their properties.
• decidable_prop: Type class for decidable properties, with automated tactics.
• list_dec: Further predicates, operations and properties of lists over decidable types.
• coherence_graph: Here we define coherence graphs, and their cliques. Special attention is given to the decidability properties of the model.
• syntax_obs: Syntax of propositional logic.
• equiv_obs: Axiomatisation of Observation algebra, i.e. modular definition of an equivalence relation over our syntax, with some generic axioms.
• laws: Consequences of the axioms presented in equiv_obs.
• sem_obs: Interpretation of propositional logic sentences as closed sets of cliques of some graph. In this files we also prove the soundness of the axioms presented so far.
• fan: Definition of the finite antineighbourhood property (FAN), and completeness proof for the associated axiomatisation.
• anticlique: Definition of the infinite decidable anticlique graph, and completeness proof for the associated axiomatisation.
• product: Definition of the product of a family of graphs, and completeness proof for the associated axiomatisation.
• fin_sem_obs: For FAN graphs, it is equivalent to interpret sentences as sets of finite cliques.