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 the normal view instead:
scientific article; zbMATH DE number 7010789
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| 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
0.7169661521911621
0 references
0.7067534923553467
0 references
