4
ответа
Можно ли программировать и проверять инварианты в Haskell?
Когда я пишу алгоритм, я обычно записываю инварианты в комментариях. Например, одна функция может вернуть упорядоченный список, а другая ожидает, что список будет упорядочен. Я знаю, что ...
вопрос задан: 15 December 2014 10:43
4
ответа
Гильбертова система - автоматизирует доказательство
Я пытаюсь доказать оператор ~ (a-> ~ b) => в Гильбертовой системе стиля. К сожалению, кажется, что невозможно придумать общий алгоритм для нахождения доказательства, но я ищу...
вопрос задан: 11 June 2014 12:57
4
ответа
Интерактивная математическая система доказательства
Я ищу инструмент (предпочтенный GUI, но CLI работал бы), который позволяет мне вводить математические выражения и затем выполнять манипуляции ими, но ограничивает меня только математически допустимыми операциями. Кроме того...
вопрос задан: 7 March 2013 17:43
1
ответ
Идрис - доказательство равенства в поточечной функции [дубликат]
Можно ли доказать равенство функций, если они равны поточечно? - т. е. построить следующую функцию: pointwiseEquals: (f: a - & gt; b) - & gt; (g: a - & gt; b) - & gt; ((x: a) - & gt; (f x) = (...
вопрос задан: 27 September 2015 12:50
1
ответ
Как выучить agda
Я пытаюсь выучить agda. Однако у меня возникла проблема. Все руководства, которые я нашел на вики-сайте agda, слишком сложны для меня и охватывают различные аспекты программирования. После параллельного чтения 3 ...
вопрос задан: 26 February 2012 18:20
1
ответ
Показ (голова. init), = направляются в Agda
Я пытаюсь доказать простую лемму в Agda, который я думаю, верно. Если вектор имеет больше чем два элемента, брать его голову после взятия init совпадает со взятием его головы сразу. Я...
вопрос задан: 10 August 2010 16:09
0
ответов
Кто-нибудь пробовал доказать Z3 с помощью самого Z3?
Кто-нибудь пробовал доказывать Z3 с самим Z3? Возможно ли вообще доказать, что Z3 правильный, используя Z3? Более теоретически, можно ли доказать, что инструмент X правильный, используя сам X?
вопрос задан: 23 February 2017 11:06
0
ответов
Сопоставление с шаблоном, не специализирующееся на типах
Я играю в Coq,
Мне просто нужна была функция, которая принимает список [1,2,3,2,4] и возвращает что-то вроде Sorted [1,2,3,4] - то есть удаляет плохие части, но ...
вопрос задан: 11 April 2016 03:16
0
ответов
Ограничения решателей SMT
Традиционно большая часть работы с вычислительной логикой была либо пропозициональной, и в этом случае вы использовали SAT (решатель булевой выполнимости ), либо первый -порядок, и в этом случае вы использовали теорему первого -порядка...
вопрос задан: 21 July 2012 13:11
0
ответов
Разница между Z3 и coq
Мне интересно, может ли кто-нибудь сказать мне разницу между Z3 и coq? Мне кажется, что coq является помощником по доказательству в том смысле, что он требует от пользователя заполнения шагов доказательства, тогда как Z3 не имеет...
вопрос задан: 17 July 2012 22:10
0
ответов
Кто-нибудь видел хорошую реализацию средства доказательства теорем SATCHMO на Прологе с открытым исходным кодом?
Я видел довольно много статей о программе доказательства теорем SATCHMO, в которых рассказывается о реализациях Пролога. Но единственная реализация исходного кода, которую я нашел до сих пор, была в книге, и она была действительно ограниченной ...
вопрос задан: 8 February 2012 05:15
0
ответов
Шаблонное соответствие с ассоциативными и коммутативными операторами
Шаблонное соответствие (как, например, в Prolog, языках семейства ML и различных оболочках экспертных систем) обычно работает путем сопоставления запроса с данными элемент за элементом в строгом порядке. В доменах ...
вопрос задан: 1 December 2011 00:44
0
ответов
SMT-решатели для арифметики битовых векторов
Я планирую несколько экспериментов в символьном исполнении кода C, используя готовый решатель SMT и задаваясь вопросом, какой решатель использовать; глядя, например, участники конкурса SMT,и взяв только open -...
вопрос задан: 7 June 2011 10:33
0
ответов
Использование средств доказательства теорем для обнаружения атак
Я слышал немного об использовании автоматических средств доказательства теорем при попытках чтобы показать, что уязвимости системы безопасности не существуют в программной системе. В общем, это чертовски сложно сделать. У меня вопрос ...
вопрос задан: 16 February 2011 00:00