–吃
发表于 2025-3-28 15:35:59
978-3-031-42752-7The Editor(s) (if applicable) and The Author(s), under exclusive license to Springer Nature Switzerl
Gastric
发表于 2025-3-28 20:03:59
Intelligent Computer Mathematics978-3-031-42753-4Series ISSN 0302-9743 Series E-ISSN 1611-3349
啮齿动物
发表于 2025-3-29 00:00:19
Large-Scale Formal Proof for the Working Mathematician—Lessons Learnt from the ALEXANDRIA Projecteat strides in the formalisation of mathematics and also in some relevant technologies, above all machine learning. Six years of intensive formalisation activity seem to show that even the most advanced results, drawing on multiple fields of mathematics, can be formalised using the tools available t
Detoxification
发表于 2025-3-29 03:13:53
Never Trust Your Solver: Certification for SAT and QBFor QBF solvers. Such solvers are sophisticated and highly tuned pieces of software, often too complex to be verified themselves. Now the question arises how one can one be sure that the result of such a solver is correct, especially when its result is critical for proving the correctness of another
一再困扰
发表于 2025-3-29 08:22:53
http://reply.papertrans.cn/47/4695/469416/469416_45.png
净礼
发表于 2025-3-29 14:26:52
http://reply.papertrans.cn/47/4695/469416/469416_46.png
冰雹
发表于 2025-3-29 15:50:45
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigatione logic based shallow semantic embedding of category theory by providing a formalization of the notion of elementary topoi. Additionally, we formalize symmetrical monoidal closed categories expressing the denotational semantic model of intuitionistic multiplicative linear logic. Next to these meta-l
cajole
发表于 2025-3-29 22:42:22
Learning Support Systems Based on Mathematical Knowledge Managementing problems, this can only be achieved via adaptive, interactive learning support services. In this paper we show how these can be generated by modeling the domain, the learner competencies, and the rhetoric and didactic relations among learning objects, re-using existing technologies and systems o
jarring
发表于 2025-3-30 02:01:40
Isabelle Formalisation of Original Representation Theorems computational biology) were discovered by cross-site data mining on huge databases, and building on existing Isabelle-verified event structures enumeration algorithms. Given the origin and newness of such theorems, their formal verification is particularly desirable. This paper presents such a veri
BLANC
发表于 2025-3-30 05:55:35
Teaching Linear Algebra in a Mechanized Mathematical Environmentthat this is a better way to teach linear algebra than the “old fashioned way”. We discuss some technological tools such as Maple, Matlab, Python, and Jupyter Notebooks, and some choices of topics that are especially suited to teaching with these tools. The discussion is informed by our experience o