|
|
|
|
Formal proof of a machine closed theorem in coq
|
|
|
|
|
|
|
|
نویسنده
|
wan h. ,he a. ,you z. ,zhao x.
|
|
منبع
|
journal of applied mathematics - 2014 - دوره : 2014 - شماره : 0
|
|
چکیده
|
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. © 2014 hai wan et al.
|
|
|
|
|
آدرس
|
school of software,tsinghua university,nlist, China, guangxi key laboratory of hybrid computation and ic design analysis,guangxi university for nationalities,nanning, China, general office of the guangxi zhuang autonomous region people's government,nanning, China, school of software,tsinghua university,nlist, China
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Authors
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|