я не пример, но я гугл некоторых людей может использовать Isabelle искать лемму и найти новую лемму с Изабеллойкак открыть новую лемму или угадать или искать следующую лемму, нужно доказать в Isabelle
не знаю, где давать подсказки для поиска или поиска следующей леммы после того, как текущая лемма окажется автоматически
Вы можете привести примеры того, как найти леммы?
Johansson et al. недавно представили систему теоретического исследования, то есть придумали леммы, основанные на ваших определениях. Вы можете найти их реализацию на GitHub и на бумаге по адресу arXiv. В этой статье вы также найдете множество примеров. Единственным недостатком является то, что, насколько я могу судить, их реализация работает только с Isabelle2013-2.
Johansson, Moa, et al. «Хипстер: интеграция теории исследований в помощнике по доказательству». Интеллектуальная компьютерная математика. Springer International Publishing, 2014. 108-122.
Для поиска лемм find_theorems обычно используется тем, что вы использовали бы, но это только найдет существующие леммы, как в вашей теории, так и в импортируемых вами теориях, включая стандартные библиотеки.
Изабель не изобретает для вас настоящие новые леммы.
Это был бы хороший вопрос для редактирования, чтобы попытаться улучшить ваш вопрос. Можете ли вы найти способ выразить это более четко? Чтобы дать некоторый контекст? Чтобы привести пример разработки, где вам нужны такие функции, и почему средства, о которых вы знаете, недостаточны? – dfeuer