GQM-Coq

This project is a formalization of the paper “One Modal Logic to Rule Them All?” by Wesley H. Holliday and Tadeusz Litak. The paper is available at https://escholarship.org/uc/item/07v9360j. This formalization was created as part of a master project at the FAU Erlangen-Nuremberg.

Requirements

This project is tested with coq version 8.7.2 and 8.8.0.

This project uses Autosubst (https://github.com/uds-psl/autosubst). It must be installed from the coq86-devel branch as described in the README of Autosubst.

For inversion the inverts … as tactic from lib/LibTactics.v is used, which is taken from the code of the Software Foundations book at https://softwarefoundations.cis.upenn.edu/.

Building the project

To build the project run $ make

There are several ways to build a documentation.

• HTML with proofs: $ make html
• HTML without proofs: $ make gallinahtml
• pdf with proofs: $ make all.pdf
• pdf without proofs: $ make all-gal.pdf

HTML documentation can be found in the html subfolder, pdf documentation is created in the main folder as all.pdf or all-gal.pdf.

Naming Conventions

GQM formulas: A,B,C…, sometimes f,g,…

Context: c

BAEA formulas: a,b,…

FO formulas: f,g,…