IsaPlanner - IsaPlanner
 | tento článek příliš spoléhá na Reference na primární zdroje. (Leden 2014) (Zjistěte, jak a kdy odstranit tuto zprávu šablony) |
IsaPlanner[1] je plánovač důkazů pro interaktivní důkaz asistent, Isabelle. Původně vyvinutý Lucasem Dixonem[2] v rámci své disertační práce na VŠE University of Edinburgh, je nyní udržována členy skupiny pro matematické uvažování v Škola informatiky v Edinburghu. IsaPlanner je nejnovější ze série plánovacích testů napsaných v Edinburghu. Dřívější plánovači zahrnují Clam a LambdaClam.
Funkce
IsaPlanner umožňuje uživateli kódovat techniky uvažování pomocí a kombinátorský jazyk, pro domněnky a dokazování věty. IsaPlanner pracuje manipulací stavů uvažování, záznamů otevřených cílů, aktuálního plánu kontroly a dalších důležitých informací a kombinátory jsou funkce mapující stavy uvažování na líné seznamy států uvažování nástupce.
Knihovna IsaPlanner dodává kombinátory pro větvení a opakování, mimo jiné úkoly, a výkonné techniky uvažování lze vytvořit kombinací jednodušších technik uvažování s těmito kombinátory.
V IsaPlanner je připraveno několik uvažovacích technik, zejména IsaPlanner obsahuje implementaci dynamiky vlnící se, vlnící se heuristický schopný pracovat v vyšší řád nastavení, a nejlepší první vlnící se heuristika a technika uvažování pro důkazy od indukce.
Mezi další funkce patří interaktivní sledovací nástroj pro ruční procházení pokusy o kontrolu a modul pro prohlížení a manipulaci hierarchický důkazy.
Plánované funkce
Funkce v současné době[když? ] které jsou implementovány nebo plánovány do budoucna, jsou rozšířenou sadou důkazní kritici, vhodné pro použití v doménách vyššího řádu, dynamické relační vlnění, a vlnící se heuristika vhodná pro vlnění relační výrazy naproti tomu funkční výrazy, opět vhodné pro použití v doménách vyššího řádu, a integrace IsaPlanner s Obecný důkaz.[Citace je zapotřebí ]