解冻
发表于 2025-3-26 23:47:56
http://reply.papertrans.cn/43/4270/426976/426976_31.png
钱财
发表于 2025-3-27 01:44:45
Inductive definitions: Automation and application,. We then describe how to generate free recursive types starting just from the Axiom of Infinity. This contrasts with the existing HOL development where several specific free recursive types are developed first.
META
发表于 2025-3-27 05:51:19
http://reply.papertrans.cn/43/4270/426976/426976_33.png
Triglyceride
发表于 2025-3-27 10:09:04
http://reply.papertrans.cn/43/4270/426976/426976_34.png
翅膀拍动
发表于 2025-3-27 16:05:29
http://reply.papertrans.cn/43/4270/426976/426976_35.png
擦掉
发表于 2025-3-27 18:21:48
0302-9743 field achieved since the predecessor conference. The papers presented fall into three general categories: representation of formalisms in higher order logic; applications of mechanized higher order logic; and enhancements to the HOL and other theorem proving systems.978-3-540-60275-0978-3-540-44784-9Series ISSN 0302-9743 Series E-ISSN 1611-3349
Type-1-Diabetes
发表于 2025-3-28 01:17:15
http://reply.papertrans.cn/43/4270/426976/426976_37.png
尖
发表于 2025-3-28 04:18:02
Experiments with ZF set theory in HOL and Isabelle,the construction of ... The advantages and disadvantages of higher-order set theory versus first-order set theory are explored experimentally. This study also provides a comparison of the proof infrastructure of HOL and Isabelle.
王得到
发表于 2025-3-28 06:52:58
Automatically synthesized term denotation predicates: A proof aid,ould and should not be matched, the function creates an ML predicate which can be used, for example, with filter or ...This paper reviews past discussions on denotation methods, the design and implementation of the filter synthesizer, applicable AI classification techniques, and possible application to more general term handling and recognition.
forebear
发表于 2025-3-28 12:22:59
Virtual theories,m. A side effect is that a version of autoloading is obtained for HOL90. A more radical feature that is obtained is the autoloading of tools. The system has been tested on part of a real hardware verification proof.