Reconstructing propositional proofs in type theory
| Autor: | Prieto Cubides, Jonathan Steven |
|---|---|
| Přispěvatelé: | Sicard Ramírez, Andrés |
| Jazyk: | Spanish; Castilian |
| Rok vydání: | 2017 |
| Předmět: |
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Demostración automática de Teoremas Teoría de Tipos TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Logic symbolic and mathematical LÓGICA SIMBÓLICA Y MATEMÁTICA Inference (logic) AGDA (Lenguaje de programación funcional) LÓGICA DE PRIMER ORDEN Ingeniería inversa Haskell (Lenguaje de programación de computadores) First-order logic INFERENCIA (LÓGICA) |
| Zdroj: | Repositorio EAFIT Universidad EAFIT instacron:Universidad EAFIT |
| Popis: | We describe a syntactical proof-reconstruction approach to verify derivations generated by Metis prover to theorems in classical propositional logic -- To verify such derivations, we formalize in type theory each inference rule of the Metis reasoning -- We developed a tool jointly with two Agda libraries to translate Metis derivations to Agda proof-terms -- These developments allowed us to type-check with Agda, Metis derivations step-by-step |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|