如何发现新的引理或猜测或搜索下一个要在 Isabelle 中证明的引理
how to discover new lemma or guess or search the next lemma which want to be proved in Isabelle
我没有例子，但我用谷歌搜索了一些人可以
使用 Isabelle 搜索引理并与 Isabelle
一起发现新的引理
当前引理自动证明后，不知道从哪里提示发现或搜索下一个引理
你能举例说明如何发现引理吗？
对于搜索引理，您通常会使用 find_theorems，但这只会查找现有的引理，无论是在您的理论中，还是在您导入的理论中，包括标准库。
伊莎贝尔并没有为你发明真正新的引理。
约翰逊等人。最近提出了一个理论探索系统，即根据您的定义提出引理。您可以在 GitHub and the paper on arXiv 上找到它们的实现。在论文中，您还会找到很多示例。唯一的缺点是，据我所知，它们的实现仅适用于 Isabelle2013-2。
约翰逊、莫阿等人。 "Hipster: Integrating Theory Exploration in a Proof Assistant."智能计算机数学。施普林格国际出版社, 2014. 108-122.
我没有例子，但我用谷歌搜索了一些人可以 使用 Isabelle 搜索引理并与 Isabelle
一起发现新的引理当前引理自动证明后，不知道从哪里提示发现或搜索下一个引理
你能举例说明如何发现引理吗？
对于搜索引理，您通常会使用 find_theorems，但这只会查找现有的引理，无论是在您的理论中，还是在您导入的理论中，包括标准库。
伊莎贝尔并没有为你发明真正新的引理。
约翰逊等人。最近提出了一个理论探索系统，即根据您的定义提出引理。您可以在 GitHub and the paper on arXiv 上找到它们的实现。在论文中，您还会找到很多示例。唯一的缺点是，据我所知，它们的实现仅适用于 Isabelle2013-2。
约翰逊、莫阿等人。 "Hipster: Integrating Theory Exploration in a Proof Assistant."智能计算机数学。施普林格国际出版社, 2014. 108-122.