伊莎贝尔(Isabelle):如何处理矩阵 [英] Isabelle: how to work with matrices

问题描述

大约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 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):如何处理矩阵的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！