债务人
发表于 2025-3-21 16:06:11
书目名称Interactive Theorem Proving影响因子(影响力)<br> http://figure.impactfactor.cn/if/?ISSN=BK0470571<br><br> <br><br>书目名称Interactive Theorem Proving影响因子(影响力)学科排名<br> http://figure.impactfactor.cn/ifr/?ISSN=BK0470571<br><br> <br><br>书目名称Interactive Theorem Proving网络公开度<br> http://figure.impactfactor.cn/at/?ISSN=BK0470571<br><br> <br><br>书目名称Interactive Theorem Proving网络公开度学科排名<br> http://figure.impactfactor.cn/atr/?ISSN=BK0470571<br><br> <br><br>书目名称Interactive Theorem Proving被引频次<br> http://figure.impactfactor.cn/tc/?ISSN=BK0470571<br><br> <br><br>书目名称Interactive Theorem Proving被引频次学科排名<br> http://figure.impactfactor.cn/tcr/?ISSN=BK0470571<br><br> <br><br>书目名称Interactive Theorem Proving年度引用<br> http://figure.impactfactor.cn/ii/?ISSN=BK0470571<br><br> <br><br>书目名称Interactive Theorem Proving年度引用学科排名<br> http://figure.impactfactor.cn/iir/?ISSN=BK0470571<br><br> <br><br>书目名称Interactive Theorem Proving读者反馈<br> http://figure.impactfactor.cn/5y/?ISSN=BK0470571<br><br> <br><br>书目名称Interactive Theorem Proving读者反馈学科排名<br> http://figure.impactfactor.cn/5yr/?ISSN=BK0470571<br><br> <br><br>
故意钓到白杨
发表于 2025-3-21 20:47:07
Verified Synthesis of Knowledge-Based Programs in Finite Synchronous EnvironmentsKBPs to executable automata with a proof of correctness in Isabelle/HOL. We develop the algorithm top-down, using Isabelle’s locale mechanism to structure these proofs, and show that two classic examples can be synthesised using Isabelle’s code generator.
cogitate
发表于 2025-3-22 03:54:14
https://doi.org/10.1007/978-3-642-22863-6ACL2; Coq; HOL; Isabelle; formal methods; program semantics; proof assistants
MAG
发表于 2025-3-22 04:38:33
978-3-642-22862-9Springer-Verlag GmbH Berlin Heidelberg 2011
NAUT
发表于 2025-3-22 10:35:19
Interactive Theorem Proving978-3-642-22863-6Series ISSN 0302-9743 Series E-ISSN 1611-3349
Vldl379
发表于 2025-3-22 15:51:45
Advances in the Formalization of the Odd Order TheoremWe present some of the proof techniques and library designs we used to formalize a large part of the proof of the Odd Order theorem.
cancer
发表于 2025-3-22 19:29:26
http://reply.papertrans.cn/48/4706/470571/470571_7.png
蕨类
发表于 2025-3-23 01:14:17
Lecture Notes in Computer Sciencehttp://image.papertrans.cn/i/image/470571.jpg
dowagers-hump
发表于 2025-3-23 02:51:54
http://reply.papertrans.cn/48/4706/470571/470571_9.png
Abduct
发表于 2025-3-23 07:08:09
Formalization of Entropy Measures in HOLe some of its properties using the HOL theorem prover. This infrastructure is then used to formalize information theoretic fundamentals like Shannon entropy and relative entropy. We discuss potential applications of the proposed formalization for the analysis of data compression and security protocols.