Formal Proof of a Machine Closed Theorem in Coq
Joint Authors
You, Zhiyang
Zhao, Xibin
Wan, Hai
He, Anping
Source
Journal of Applied Mathematics
Issue
Vol. 2014, Issue 2014 (31 Dec. 2014), pp.1-9, 9 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2014-03-30
Country of Publication
Egypt
No. of Pages
9
Main Subjects
Abstract EN
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.
American Psychological Association (APA)
Wan, Hai& He, Anping& You, Zhiyang& Zhao, Xibin. 2014. Formal Proof of a Machine Closed Theorem in Coq. Journal of Applied Mathematics،Vol. 2014, no. 2014, pp.1-9.
https://search.emarefa.net/detail/BIM-505961
Modern Language Association (MLA)
Wan, Hai…[et al.]. Formal Proof of a Machine Closed Theorem in Coq. Journal of Applied Mathematics No. 2014 (2014), pp.1-9.
https://search.emarefa.net/detail/BIM-505961
American Medical Association (AMA)
Wan, Hai& He, Anping& You, Zhiyang& Zhao, Xibin. Formal Proof of a Machine Closed Theorem in Coq. Journal of Applied Mathematics. 2014. Vol. 2014, no. 2014, pp.1-9.
https://search.emarefa.net/detail/BIM-505961
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-505961
