维持
发表于 2025-3-25 03:20:42
Applications of paper chemistry, in a growing library of mathematics for proof assistant Coq. On the other hand the computational issues raised by the univalent semantics may lead in the future to a new class of programming languages.
横条
发表于 2025-3-25 10:18:05
Practical applications of paper chemistry,ed part of reasoning with Nominal Isabelle, and together with analysing freshness is the part that differs most from paper proofs. In this paper we show how to define terms from .-calculus and reason about them without having to carry around the freshness conditions. As a case study we formalize the second fixed point theorem of the .-calculus.
灯丝
发表于 2025-3-25 14:41:43
http://reply.papertrans.cn/23/2234/223355/223355_23.png
Defraud
发表于 2025-3-25 16:02:27
Automated Certification of Implicit Induction Proofsthe certification process and show that the certification time is reasonable even for industrial-size applications. As a case study, we automatically prove and certify more than 40% of the lemmas needed for the validation of a conformance algorithm for the ABR protocol.
大漩涡
发表于 2025-3-25 23:32:58
http://reply.papertrans.cn/23/2234/223355/223355_25.png
发微光
发表于 2025-3-26 01:23:55
Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theoremed part of reasoning with Nominal Isabelle, and together with analysing freshness is the part that differs most from paper proofs. In this paper we show how to define terms from .-calculus and reason about them without having to carry around the freshness conditions. As a case study we formalize the second fixed point theorem of the .-calculus.
哑剧
发表于 2025-3-26 05:16:05
The Teaching Tool , A Proof-Checker for Gries and Schneider’s “Logical Approach to Discrete Math”rticular compromise between full formality and customary, more informal, mathematical practises, and thus teaches aspects of both. This is one source of several unusual requirements for a mechanised proof-checker; other interesting aspects arise from details of their notational conventions.
较早
发表于 2025-3-26 09:20:47
Practical applications of paper chemistry,zed using the HOL4 theorem prover. Memoized parsers based on our approach are polynomial-time in the size of the input. Preliminary real-world performance testing on highly ambiguous grammars indicates our parsers are faster than those generated by the popular Happy parser generator.
Alpha-Cells
发表于 2025-3-26 14:04:27
http://reply.papertrans.cn/23/2234/223355/223355_29.png
结束
发表于 2025-3-26 18:16:26
A Proposal for Broad Spectrum Proof Certificatessent the structure of proof evidence captured by a particular class of computational logic systems. While such proof certificates can capture a wide variety of proof structures, a proof checker can remain simple since it must only understand the micro-rules and the discipline of focusing. Since proo