IsaPlanner
 |
IsaPlanner [1] — планировщик доказательств для интерактивного помощника по доказательствам Изабель . Первоначально разработан Лукасом Диксоном. [2] как часть его докторской диссертации в Эдинбургском университете , сейчас она поддерживается членами Группы математических рассуждений Школы информатики в Эдинбурге.IsaPlanner — последний из серии планировщиков доказательств, написанных в Эдинбурге. Более ранние планировщики включают Clam и LambdaClam.
Функции
[ редактировать ]IsaPlanner позволяет пользователю кодировать методы рассуждения, используя язык комбинатора , для построения предположений и доказательства теорем . IsaPlanner работает, манипулируя состояниями рассуждения, записями открытых целей, текущим планом доказательства и другой важной информацией, а комбинаторы — это функции, отображающие состояния рассуждения в ленивые списки последующих состояний рассуждения.
Библиотека IsaPlanner, предоставляет комбинаторы для ветвления и итерации помимо других задач, , а мощные методы рассуждения могут быть созданы путем объединения более простых методов рассуждения с этими комбинаторами.
Несколько методов рассуждения уже реализованы в IsaPlanner, в частности, IsaPlanner включает реализацию динамического пульсирования , эвристику пульсации, способную работать в настройках более высокого порядка , эвристику пульсации по принципу «наилучшее первое» и технику рассуждения для доказательств путем индукции .
Дополнительные функции включают в себя интерактивный инструмент отслеживания для ручного пошагового выполнения попыток доказательства и модуль для просмотра иерархических доказательств и управления ими.
Планируемые функции
[ редактировать ]Возможности на данный момент [ когда? ] реализуемые или запланированные на будущее, — это расширенный набор критиков доказательств , подходящий для использования в областях более высокого порядка, динамическое реляционное колеблющееся движение, колеблющаяся эвристика, подходящая для чередования реляционных выражений в отличие от функциональных выражений, снова подходящая для использования в более высоких домены заказа и интеграция IsaPlanner с Proof General . [ нужна ссылка ]