细微的差异
发表于 2025-3-28 15:37:29
Representing Structural Language Features in Formal Meta-languages challenge when representing languages in meta-languages such as standard formats like . or logical frameworks like .. It is desirable to use shallow representations where a structural language feature is represented by the analogous feature of the meta-language, but the richness of structural langu
maverick
发表于 2025-3-28 22:03:40
Formally Verifying Proofs for Algebraic Identities of Matricesexplicit algorithms relying on non-commutative Gröbner bases. We address not only verification, but also exploration and reasoning towards establishing new identities and even proving mathematical properties. Especially Gröbner-driven elimination theory navigates us to insightful conclusions. We pre
G-spot
发表于 2025-3-28 23:45:29
http://reply.papertrans.cn/47/4695/469415/469415_43.png
granite
发表于 2025-3-29 05:38:11
Maintaining a Library of Formal Mathematics entry for contributors and to lessen the burden of reviewing contributions, we have developed a number of tools for the library which check proof developments for subtle mistakes in the code and generate documentation suited for our varied audience.
镇痛剂
发表于 2025-3-29 08:00:32
Conference proceedings 2020 Italy, in July 2020*..The 15 full papers, 1 invited paper and 2 abstracts of invited papers presented were carefully reviewed and selected from a total of 35 submissions. The papers focus on advances in automated theorem provers and formalization, computer algebra systems and their libraries, and a
琐事
发表于 2025-3-29 14:07:24
http://reply.papertrans.cn/47/4695/469415/469415_46.png
未成熟
发表于 2025-3-29 16:16:41
A Framework for Formal Dynamic Dependability Analysis Using HOL Theorem Provingly. In this paper, we describe recent developments towards this direction along with a roadmap on how to be able to develop a framework for formal reasoning support for DFTs, DRBDs and CTMCs in a higher-order-logic theorem prover.
带子
发表于 2025-3-29 21:36:14
A Survey of Languages for Formalizing Mathematicsowledge, and language frameworks that allow building customized languages..We evaluate their advantages based on our experience in designing and applying languages and tools for formalizing mathematics. We reach the conclusion that no existing language is truly good enough yet and derive ideas for possible future improvements.
Accrue
发表于 2025-3-29 23:56:17
Induction with Generalization in Superposition Reasoningners automating induction. We demonstrate the strength of our technique by showing that many interesting mathematical properties of natural numbers and lists can be proved automatically using this extension.
Malaise
发表于 2025-3-30 07:14:58
Formalizing Graph Trail Properties in Isabelle/HOLry library of Isabelle/HOL with an algorithm computing the length of a longest strictly decreasing graph trail starting from a vertex for a given weight distribution, and prove that any decreasing trail is also an increasing one.