问题描述
大约2-3周前，我开始学习定理证明者Isabelle.我仍然是一个绝对的初学者，到目前为止，我已经完成了在Isabelle/HOL中进行编程和验证"教程.
I started to learn Isabelle, the theorem prover, about 2-3 weeks ago. I am still an absolute beginner and I worked with the tutorial "Programming and Proving in Isabelle/HOL" so far.
到目前为止，我发现的关于矩阵的唯一帮助是查看 HOL库中的源代码.
The only help on matrices I found so far was to look at the source code in the HOL library.
现在，我想学习如何证明矩阵的性质.矩阵的lambda语法对我来说仍然是新的.在Isabelle中是否有任何有关使用矩阵的教程或基本/中级示例?
Now I want to learn how to prove properties about matrices. The lambda syntax for matrices is still new to me.Are there any tutorials or basic/intermediate examples on using matrices in Isabelle?
推荐答案
这是AFP http://afp.sourceforge.net/entries/Matrix.shtml
CeTA http://cl-informatik.uibk.ac.at/software/ceta/在这里作为应用程序被引用，因此您可以在其中查看如何在实践中使用它的示例.
CeTA http://cl-informatik.uibk.ac.at/software/ceta/ is cited here as an application, so you may look there for examples how it is being used in practice.
这篇关于伊莎贝尔(Isabelle):如何处理矩阵的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！