Formal Proof of a Machine Closed Theorem in Coq. (30th March 2014)

• Record Type: Journal Article
• Authors: Wan, Hai; He, Anping; You, Zhiyang; Zhao, Xibin
• Other Names: Song X. Academic Editor.
• Is Part Of: Journal of applied mathematics. Volume 2014(2014)
• Publication Date: 2014-03-30
• Subjects: Mathematics -- Periodicals; 519.05
• DOI: 10.1155/2014/892832
• Languages: English
• ISSNs: 1110-757X

Abstract

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.