Formal Proof of a Machine Closed Theorem in Coq
| Autor: | Hai Wan, Anping He, Zhiyang You, Xibin Zhao |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2014 |
| Předmět: | |
| Zdroj: | Journal of Applied Mathematics, Vol 2014 (2014) |
| Druh dokumentu: | article |
| ISSN: | 1110-757X 1687-0042 |
| 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: | Directory of Open Access Journals |
| Externí odkaz: |
|