The agda-metis library is a formalization in Agda to reconstruct syntactically the Metis inference rules for propositional logic. This library works jointly with Agda-Prop. Both libraries are intended to support output from the Athena tool. Supporting proofs generated by Metis v2.4.20180301.
To install the required libraries see Agda documentation.
- Clone this repository:
$ git clone https://github.com/jonaprieto/agda-metis.git
$ cd agda-metis
- In order to test the installation of agda-metis you can run some tests.
$ make test
-
Hurd, J. (2003). First-order Proof Tactics In Higher-order Logic Theorem Provers. Design and Application of Strategies/Tactics in Higher Order Logics, Number NASA/CP-2003-212448 in NASA Technical Reports, 56–68. Retrieved from http://www.gilith.com/research/papers
-
Böhme, S., & Weber, T. (2010). Fast LCF-Style Proof Reconstruction for Z3. In M. Kaufmann & L. C. Paulson (Eds.), Interactive Theorem Proving: First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings (pp. 179–194). Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-14052-5_14
-
Kanso, K., & Setzer, A. (2016).A Light-weight Integration Of Automated And Interactive Theorem Proving. Mathematical Structures in Computer Science, 26(1), 129–153. https://doi.org/10.1017/S0960129514000140