HPA533
发表于 2025-3-25 04:58:35
A proof development system for the HOL theorem prover,In this paper, we present a system to improve the interaction between HOL and the user when doing proofs.
Mobile
发表于 2025-3-25 09:37:49
http://reply.papertrans.cn/43/4270/426975/426975_22.png
解冻
发表于 2025-3-25 14:01:58
Some theorems we should prove,Mathematical techniques can be used to produce precise, provably complete documentation for computer systems. However, such documents are highly detailed; oversights and other errors arc quite common. To detect the “early” errors in a document, one must attempt to prove certain simple theorems. This paper gives some examples of such theorems.
obsolete
发表于 2025-3-25 18:44:26
Using PVS to prove some theorems of David Parnas,David Parnas describes some theorems representative of those encountered in support of certification of software for the Darlington nuclear reactor. We describe the verification of these theorems using PVS.
圣歌
发表于 2025-3-25 23:40:21
Extending the HOL theorem prover with a computer algebra system to reason about the reals,In this paper we describe an environment for reasoning about the reals which combines the rigour of a theorem prover with the power of a computer algebra system.
CROW
发表于 2025-3-26 01:45:47
http://reply.papertrans.cn/43/4270/426975/426975_26.png
止痛药
发表于 2025-3-26 08:15:22
http://reply.papertrans.cn/43/4270/426975/426975_27.png
种族被根除
发表于 2025-3-26 11:18:07
http://reply.papertrans.cn/43/4270/426975/426975_28.png
戏服
发表于 2025-3-26 12:45:26
Reasoning with the formal definition of standard ML in HOL,. HOL theories of the Core syntax and dynamic semantics are presented, including a purely definitional representation of the semantic inference rules. The correctness of the representation is demonstrated by the derivation of several important language properties, including determinacy. A symbolic e
不安
发表于 2025-3-26 18:14:26
http://reply.papertrans.cn/43/4270/426975/426975_30.png