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, 1-9

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)
http://downloads.hindawi.com/journals/JAM/2014/892832.pdf (application/pdf)
http://downloads.hindawi.com/journals/JAM/2014/892832.xml (text/xml)

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:hin:jnljam:892832

DOI: 10.1155/2014/892832

Access Statistics for this article

More articles in Journal of Applied Mathematics from Hindawi
Bibliographic data for series maintained by Mohamed Abdelhakeem ().