Formal proof of a machine closed theorem in Coq (Q1714805)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Formal proof of a machine closed theorem in Coq |
scientific article; zbMATH DE number 7010789
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Formal proof of a machine closed theorem in Coq |
scientific article; zbMATH DE number 7010789 |
Statements
Formal proof of a machine closed theorem in Coq (English)
0 references
1 February 2019
0 references
Summary: The paper presents a formal proof of a machine closed theorem of \(\mathrm{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.
0 references
