acrophobia
发表于 2025-3-25 04:36:36
Reasoning about a class of linear systems of equations in HOL,bout natural numbers. The procedure has been developed in order to reason about an aspect of programs described in the Silage language. The semantics of Silage has been defined in the HOL system and specifies the class of linear systems of equations that the algorithm copes with.
BAN
发表于 2025-3-25 10:38:40
Towards a HOL theory of memory,an be expressed as simulations between the corresponding transition systems. We show how simulation relations are preserved by structuring operators over transition systems. We derive from them proof tactics used to establish simulation relations between basic memory models. These memory models are
Vital-Signs
发表于 2025-3-25 13:18:42
Providing tractable security analyses in HOL,and proving that these designs have particular nondisclosure security properties. These tools include the Romulus Interface Process Specification Language (IPSL) and a translator for translating IPSL specifications into HOL90.
并入
发表于 2025-3-25 18:46:20
First-order automation for higher-order-logic theorem proving,or proving comparable goals. Therefore it is vital to increase the automation of higher-order logic systems in order to really benefit from their particular advantages..Two approaches for incorporating first-order proof automation into the system LAMBDA have been investigated. In the first one, the
一致性
发表于 2025-3-25 23:37:31
http://reply.papertrans.cn/43/4270/426974/426974_25.png
彩色
发表于 2025-3-26 03:11:54
Datatypes in L2,ion but has restrictions on the use of function type construction. We sketch a set-theoretic model for these datatypes. Finally, we briefly discuss the relationship between L2‘s datatypes and datatypes in HOL.
NATTY
发表于 2025-3-26 06:01:00
http://reply.papertrans.cn/43/4270/426974/426974_27.png
Diskectomy
发表于 2025-3-26 10:56:13
http://reply.papertrans.cn/43/4270/426974/426974_28.png
photophobia
发表于 2025-3-26 14:05:40
http://reply.papertrans.cn/43/4270/426974/426974_29.png
MOAN
发表于 2025-3-26 19:10:16
Weak systems of set theory related to HOL,t does contain announcements (of novel unpublished results) and proofs (of frequently underregarded trivialities). For the reader who wishes to take this material further, the chief advantage of this essay will be the bibliography, which would be quite hard for a naïve reader to assemble from scratc