Фокс
В автоматизированном доказательстве теорем PhoX — это помощник по доказательству, основанный на логике высшего порядка расширяемой . Пользователь задает PhoX первоначальную цель и направляет ее через подцели и доказательства, подтверждающие эту цель; внутри он строит естественные деревья вывода. Каждая ранее доказанная формула может стать правилом для последующих доказательств.
PhoX был первоначально разработан и реализован Кристофом Раффалли на OCaml языке программирования . Он продолжает возглавлять нынешнюю команду разработчиков, созданную совместными усилиями Университета Савойи и Университета Париж VII .
Основная цель проекта PhoX — создание удобной для пользователя системы проверки корректур с использованием системы типов, разработанной Жаном-Луи Кривином в Университете Париж VII. Предполагается, что она будет более интуитивно понятной, чем другие системы, оставаясь при этом расширяемой, эффективной и выразительной. По сравнению с другими системами синтаксис построения доказательства упрощен и приближен к естественному языку. Другие функции включают в себя построение доказательства на основе графического пользовательского интерфейса, рендеринг форматированного вывода и доказательство правильности программ на языке программирования ML .
PhoX в настоящее время используется для преподавания логики в Университете Савойи. Он находится в экспериментальном, но пригодном для использования состоянии. Он выпущен под CeCILL 2.0.
Внешние ссылки
[ редактировать ] | Эта логике статья, посвященная , незавершена . Вы можете помочь Википедии, расширив ее . |