Armory
发表于 2025-3-25 05:54:01
http://reply.papertrans.cn/48/4706/470578/470578_21.png
granite
发表于 2025-3-25 10:26:26
A , Tactic for Equality Learning in Linear Arithmetic,T-solving: combining tactics by exchanging equalities. The paper describes how we have implemented equality learning in a new . tactic, dealing with linear arithmetic over rationals. It also illustrates how this tactic interacts with other . tactics.
值得赞赏
发表于 2025-3-25 14:13:25
http://reply.papertrans.cn/48/4706/470578/470578_23.png
或者发神韵
发表于 2025-3-25 16:34:57
http://reply.papertrans.cn/48/4706/470578/470578_24.png
BRIBE
发表于 2025-3-25 23:19:36
A Formalization of the LLL Basis Reduction Algorithm,anized soundness proof of the LLL algorithm using Isabelle/HOL. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.
Chronological
发表于 2025-3-26 03:48:28
HOL Light QE,strate the implementability of . and the benefits of having quotation and evaluation in a proof assistant. The resulting system is called .. Here we document the design of . and the challenges that needed to be overcome. The resulting implementation is freely available.
Largess
发表于 2025-3-26 05:49:37
Efficient Mendler-Style Lambda-Encodings in Cedille,in constant-time. As a result, we can define lambda-encoded natural numbers with an induction principle and a constant-time predecessor function so that the normal form of a numeral requires only linear space. The paper also includes several more advanced examples.
osteoclasts
发表于 2025-3-26 11:52:48
Conference proceedings 2018, as well as applications to verifying hardware and software systems to ensure their safety and security, and applications to the formal verication of mathematical results..Chapters 2, 10, 26, 29, 30 and 37 are available open access under a CreativeCommons Attribution 4.0 International License via link.springer.com..
trigger
发表于 2025-3-26 13:53:08
http://reply.papertrans.cn/48/4706/470578/470578_29.png
弓箭
发表于 2025-3-26 20:18:27
Backwards and Forwards with Separation Logic,is derived directly from the standard operators of separation logic, the latter uses a new one. We implement our framework in the interactive proof assistant Isabelle/HOL, and enable automation with several interactive proof tactics.