A Comprehensive Formalization of Propositional Logic in Coq: Deduction Systems, Meta-Theorems, and Automation Tactics
The increasing significance of theorem proving-based formalization in mathematics and computer science highlights the necessity for formalizing foundational mathematical theories. In this work, we employ the Coq interactive theorem prover to methodically formalize the language, semantics, and syntax...
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Artigo |
| Lenguaje: | Inglês |
| Publicado: |
MDPI AG
2023-05-01
|
| Colección: | Mathematics |
| Materias: | |
| Acceso en línea: | https://www.mdpi.com/2227-7390/11/11/2504 |
| Etiquetas: |
Sin Etiquetas, Sea el primero en etiquetar este registro!
|