Skip to content

Latest commit

 

History

History
50 lines (36 loc) · 2.28 KB

README.md

File metadata and controls

50 lines (36 loc) · 2.28 KB
Raw

Agda-Metis Build Status DOI

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.

Prerequisites

To install the required libraries see Agda documentation.

Installation

  1. Clone this repository:
$ git clone https://github.com/jonaprieto/agda-metis.git
$ cd agda-metis
  1. In order to test the installation of agda-metis you can run some tests.
$ make test

References

  • 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