IsaPlanner
IsaPlanner to narzędzie do planowania proofa dla interaktywnej asystentki sprawdzającej , Isabelle . Pierwotnie opracowany przez Lucasa Dixona jako część jego pracy doktorskiej na Uniwersytecie w Edynburgu , jest obecnie utrzymywany przez członków Mathematical Reasoning Group w School of Informatics w Edynburgu. IsaPlanner to najnowszy z serii planistów dowodowych napisanych w Edynburgu. Wcześniejsi planiści to Clam i LambdaClam.
Cechy
IsaPlanner umożliwia użytkownikowi zakodowanie technik wnioskowania, używając języka kombinatora , do snucia domysłów i dowodzenia twierdzeń . IsaPlanner działa poprzez manipulowanie stanami rozumowania, zapisami otwartych celów, aktualnym planem dowodowym i innymi ważnymi informacjami, a kombinatory to funkcje odwzorowujące stany rozumowania na leniwe listy kolejnych stanów rozumowania.
Biblioteka IsaPlanner dostarcza kombinatory do rozgałęzień i iteracji , między innymi, a potężne techniki wnioskowania można tworzyć łącząc prostsze techniki wnioskowania z tymi kombinatorami.
Kilka technik wnioskowania jest gotowych do wdrożenia w IsaPlanner, w szczególności IsaPlanner zawiera implementację dynamicznego falowania , heurystykę falowania zdolną do pracy w ustawieniach wyższego rzędu , heurystykę falowania najlepszego pierwszego oraz technikę rozumowania dla dowodów przez indukcję .
Dodatkowe funkcje obejmują interaktywne narzędzie do śledzenia, umożliwiające ręczne przechodzenie przez próby dowodowe oraz moduł do przeglądania i manipulowania dowodami hierarchicznymi .
Planowane funkcje
Funkcje obecnie [ kiedy? ] wdrażany lub planowany na przyszłość to rozszerzony zestaw krytyków dowodowych, odpowiedni do użycia w domenach wyższego rzędu, dynamiczne falowanie relacji, heurystyka falowania odpowiednia do falowania wyrażeń relacyjnych w przeciwieństwie do wyrażeń funkcjonalnych , ponownie odpowiednia do użycia w domeny wyższego rzędu oraz integracja IsaPlanner z Proof General. [ potrzebne źródło ]