Formal Proof of a Machine Closed Theorem in Coq
| Autor: | Anping He, Xibin Zhao, Zhiyang You, Hai Wan |
|---|---|
| Rok vydání: | 2014 |
| Předmět: |
Discrete mathematics
Article Subject lcsh:Mathematics Applied Mathematics State (functional analysis) lcsh:QA1-939 Formal proof Algebra Computer-assisted proof TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Concrete syntax TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Scheme (mathematics) Embedding TRACE (psycholinguistics) Mathematics Theorem Proving System |
| Zdroj: | Journal of Applied Mathematics, Vol 2014 (2014) J. Appl. Math. |
| ISSN: | 1687-0042 1110-757X |
| DOI: | 10.1155/2014/892832 |
| Popis: | The paper presents a formal proof of a machine closed theorem of TLA+in the theorem proving system Coq. A shallow embedding scheme is employed for the proof which is independent of concrete syntax. Fundamental concepts need to state that the machine closed theorems are addressed in the proof platform. A useful proof pattern of constructing a trace with desired properties is devised. A number of Coq reusable libraries are established. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|