Formal Proof of a Machine Closed Theorem in Coq

Hai Wan, Anping He, Zhiyang You and Xibin Zhao

Journal of Applied Mathematics, 2014, vol. 2014, issue 1

Abstract: 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.

Date: 2014
References: Add references at CitEc
Citations:

Downloads: (external link)
https://doi.org/10.1155/2014/892832

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:wly:jnljam:v:2014:y:2014:i:1:n:892832

Access Statistics for this article

More articles in Journal of Applied Mathematics from John Wiley & Sons
Bibliographic data for series maintained by Wiley Content Delivery ().