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.

• Agda 2.5.4+
• agda-prop

To install the required libraries see Agda documentation.

1. Clone this repository:

$ git clone https://github.com/jonaprieto/agda-metis.git
$ cd agda-metis

2. 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