decode
发表于 2025-3-25 06:37:59
http://reply.papertrans.cn/63/6262/626188/626188_21.png
Accolade
发表于 2025-3-25 09:07:11
https://doi.org/10.1007/11812289LaTeX; complexity; e-learning; formal logic; formal mathematics; interactive algebra; knowledge management
escalate
发表于 2025-3-25 11:50:38
http://reply.papertrans.cn/63/6262/626188/626188_23.png
飓风
发表于 2025-3-25 16:20:18
Mathematical Knowledge Management978-3-540-37106-9Series ISSN 0302-9743 Series E-ISSN 1611-3349
Hectic
发表于 2025-3-25 20:38:30
0302-9743 Overview: 978-3-540-37104-5978-3-540-37106-9Series ISSN 0302-9743 Series E-ISSN 1611-3349
output
发表于 2025-3-26 01:07:17
http://reply.papertrans.cn/63/6262/626188/626188_26.png
Misgiving
发表于 2025-3-26 04:35:53
A Formal Correspondence Between OMDoc with Alternative Proofs and the ,-Calculus of the .-calculus seen as a proof format. We provide explanations in pseudo-natural language of proofs in both formats, and a formal correspondence between the two by means of two mutually inverse encodings of one format in the other one.
含水层
发表于 2025-3-26 10:38:37
Verifying and Invalidating Textbook Proofs Using Scunakable representations of natural deduction proofs. We show how the new mathematical assistant system Scunak can be used to verify a textbook proof by translating the . version into a proof term in a dependent type theory. We also show how Scunak can give interesting output upon failure.
Flustered
发表于 2025-3-26 14:26:53
http://reply.papertrans.cn/63/6262/626188/626188_29.png
爱国者
发表于 2025-3-26 17:19:13
Structured Induction Proofs in Isabelle/Isarn-standard variants of induction as well, such as co-induction and nominal induction. This demonstrates that Isar provides a viable platform for building domain-specific tools that support fully-formal mathematical proof composition.