search

Coda-Coda / Veracity-Logic-Mechanised

This is a mechanisation of a logic for veracity in Coq.
https://coda-coda.github.io/Veracity-Logic-Mechanised/
MIT License
0 stars 0 forks source link

readme

Veracity Logic Mechanised

This repository contains a mechanisation of a logic for veracity in Coq as well as early work in Isabelle.

The veracity logic mechanised in Coq is best viewed at: https://coda-coda.github.io/Veracity-Logic-Mechanised

Please see the arXiv paper at https://arxiv.org/abs/2302.06164 for more information.

Codespaces + VSCoq (using this repository from just a web-browser)

Note: Codespaces have free quotas but are not free in general, for more information see here.

  1. Open in GitHub Codespaces or resume your existing Codespace. It should take about 5 minutes to create a new Codespace, resuming an existing Codespace should be quicker.
  2. Open a .v file (in the /Coq sub-folder) and use the keyboard shortcuts Alt+UpArrow and Alt+DownArrow to step forward and back through the proofs, and Alt+RightArrow to step forward up to the cursor. On macOS use Control+Option instead of Alt.
  3. Delete the Codespace once you are finished, to avoid being charged for storage costs. Ensure that you download or commit and push any changes you would like to keep before deleting the Codespace.

For general information about GitHub Codespaces, please see: https://github.com/features/codespaces.