TIGER 发表于 2025-3-28 15:08:45

http://reply.papertrans.cn/47/4695/469423/469423_41.png

反馈 发表于 2025-3-28 21:53:23

The Coq Library as a Theory Graph,ribution is a translation of the Coq module system into theory graphs. This greatly reduces the complexity of the library as the more arcane module system features are eliminated while preserving most of the structure. On the practical side, our main contribution is an implementation of this transla

虚弱的神经 发表于 2025-3-29 02:08:07

http://reply.papertrans.cn/47/4695/469423/469423_43.png

冥想后 发表于 2025-3-29 05:17:02

http://reply.papertrans.cn/47/4695/469423/469423_44.png

翻布寻找 发表于 2025-3-29 08:19:28

Diagram Combinators in MMT, We provide many important combinators, and our extension allows library developers to define arbitrary new ones. We evaluate our framework by building a library of algebraic theories in an extremely compact way.

preeclampsia 发表于 2025-3-29 14:40:59

http://reply.papertrans.cn/47/4695/469423/469423_46.png

轻信 发表于 2025-3-29 16:08:18

Andrea Condoluci,Michael Kohlhase,Dennis Müller,Florian Rabe,Claudio Sacerdoti Coen,Makarius Wenzel

欢腾 发表于 2025-3-29 20:04:48

Daniel Raggi,Aaron Stockdill,Mateja Jamnik,Grecia Garcia Garcia,Holly E. A. Sutherland,Peter C.-H. C

Diskectomy 发表于 2025-3-30 03:57:16

http://reply.papertrans.cn/47/4695/469423/469423_49.png

断断续续 发表于 2025-3-30 06:56:48

Conference proceedings 2019ical information. Separate communities have developed to investigate and build computer based systems for computer algebra, automated deduction, and mathematical publishing as well as novel user interfaces. While all of these systems excel in their own right, their integration can lead to synergies offering significant added value.
页: 1 2 3 4 [5] 6 7
查看完整版本: Titlebook: Intelligent Computer Mathematics; 12th International C Cezary Kaliszyk,Edwin Brady,Claudio Sacerdoti Coen Conference proceedings 2019 Sprin