Описание тега acl2

Описание тега Вопросы с тегом
Автоматическое средство доказательства теорем - программная система, состоящая из языка программирования, расширяемой теории в логике первого порядка и механического средства доказательства теорем. Язык ввода и реализация ACL2 построены на Common Lisp.
2 ответа

Понимание ошибки тегов

Я пытаюсь разобраться в сообщении об ошибке, чтобы я мог его исправить. Как правильно исправить следующую ошибку? Должен ли я пойти добавить :oslib, :quicklisp, а также :quicklisp.osicat к включенным книгам внутри books/oslib/rmtree.lisp? Является л…
23 сен '14 в 20:36
1 ответ

Написание функции select() в ACL2

Я пытаюсь написать функцию в ACL2 (в частности, ACL2s), которая принимает список и натуральное число и возвращает элемент в списке по указанному индексу. Так (выберите (список 1 2 3) 2) вернет 3. Вот мой код: ;; select: List x Nat -> All (defunc …
25 янв '16 в 18:25
1 ответ

При создании книг ACL2, как мне избавиться от ошибки "Волшебное число..."

При сборке книг для ACL2 я получаю следующую ошибку. Как мне от этого избавиться? Magic number checking on storable file failed at ../../lib/Storable.pm (autosplit into ../../lib/auto/Storable/_retrieve.al) line 380, at /<elided>/sw/acl2/books…
02 сен '14 в 21:08
1 ответ

Как отключить быстрый и грязный шаг замены замены

Когда я прерываю свои доказательства, которые вышли на обед, я вижу quick-and-dirty-subsumption-replacement-step в обратном следе. Как отключить эту эвристику?
14 янв '16 в 22:17
1 ответ

Отмена области только для чтения в emacs с использованием ACL2

Я столкнулся с каким-то странным заклинанием нажатий клавиш в emacs при использовании ACL2, и область в моем буфере становится доступной только для чтения. Что может вызвать это? Как мне пометить регион только для чтения?
27 мар '15 в 16:18
1 ответ

Как обновить значения переменных в ACL2?

Я новичок в ACL2 доказатель теоремы. Я хочу обновить значение переменной на основе результата XOR трех переменных. Я думаю, что "setq" сделает это для меня. (setq out (xor (xor a b) c)) Тем не менее, я получаю эту ошибку: Ошибка ACL2 в верхнем уровн…
15 ноя '17 в 05:35
1 ответ

Вызов функции n раз acl2

Я не могу понять, как вызвать функцию n раз для использования в другой функции У меня есть функция (defun right-shift (l) (append l '(0))) И мне нужно написать еще одну функцию, которая должна сместить '(l) n раз (defun right-shift-n-times (l n) (na…
25 окт '17 в 18:23
1 ответ

acl2 равенство с отрицанием

У меня проблемы с acl2, пытаюсь доказать следующее: (thm (implies (acl2-numberp x) (equal (* -2 x) (* 2 (- x))))) что приводит к: ACL2 !>(thm (implies (acl2-numberp x) (equal (* -2 x) (* 2 (- x))))) *1 (the initial Goal, a key checkpoint) is push…
29 июл '14 в 17:38
1 ответ

Часы GL ACL2 закончились

Что это значит, когда я получаю следующее сообщение об ошибке? Я загрузил GL. | ACL2 Error in ( DEFTHM SOME-THEOREM-THAT-USES-GL ...): The clock | ran out.~%
05 ноя '15 в 00:17
1 ответ

Как мне заставить time$ работать с ctrl+t e в ACL2 и emacs?

При попытке скопировать форму в мой буфер оболочки ACL2 с помощью ctrl+t e, и я уже поместил time$ в свой буфер оболочки, я получаю ошибку о невозможности вставить форму. Как я могу изменить макрос emacs так, чтобы я мог вставить в буферы оболочки A…
23 ноя '15 в 16:25
0 ответов

Запуск и тестирование свойства, выражающего связь между TAKE и APPEND

По сути, мне нужно написать то, что написано в названии, единственное отношение, которое я смог придумать, - это если я беру некоторое количество элементов из списка с TAKE а затем возьмите не столь важную другую половину с CDR а потом APPEND два, к…
27 авг '13 в 17:36
1 ответ

Как исправить петлю в перезаписи доказательства

Я пытаюсь моделировать натуральные числа в унарной записи (O, (S O), (S (S O)),...) в ACL2 и докажем коммутативность сложения. Вот моя попытка: ; a NATURAL is 'O or a list ('S n') where n' is a NATURAL (defun naturalp (n) (cond ((equal n 'O) t) (t (…
31 янв '16 в 11:41
0 ответов

Как вы расширяете чистый скрипт ACL2 в полноценную программу

Я вижу много ресурсов о том, как использовать ACL2 для проверки кода, как и следовало ожидать, но не о том, как использовать проверенный код в работе. Нужно ли настроить код ACL2 для работы с CLISP/Scheme/Clojure? Может ли ACL2 запустить мой код? (г…
13 ноя '13 в 10:35
1 ответ

Как я могу отследить ACL2 rewriter?

Как я могу отследить ACL2 rewriter? Мне бы очень хотелось узнать, что происходит внутри прувера. Желательно ли искать этот тип информации или я должен просто следовать Методу?
10 июл '15 в 17:37
1 ответ

Определить книги, в настоящее время сертифицированные с помощью ACL2

Как узнать, какие книги в настоящее время сертифицированы с помощью ACL2 на данном компьютере? Я знаю, что могу посмотреть на результат и понять это, но это требует нетривиальных усилий.
02 апр '15 в 19:21
1 ответ

Как избежать сбоя в низкоуровневом отладчике при компиляции ACL2 на SBCL?

Как избежать сбоя в низкоуровневом отладчике при компиляции ACL2 на SBCL? Вот сообщение об ошибке, которое я получаю при компиляции с использованием SBCL 1.2.3 в Linux: <snip> ACL2 loading '((COMP-FN :EXEC NIL "1" STATE)). NIL Finished loading…
03 сен '14 в 12:47
0 ответов

В макротрансформаторе возможно ли поднять определение до верхнего уровня?

В макропреобразователе ACL2 возможно ли поднять определение функции до верхнего уровня? Я пытаюсь создать макрос let-map которые могут определять такие функции, как map-double ниже, когда дано double функция. Если бы я заботился только о верхнем уро…
24 мар '16 в 16:59
1 ответ

ACL2 как сохранить часть списка?

Так что я все еще относительно новичок в acl2 и lisp, я не знаю, как это сделать в lisp. Как я могу добиться своего комментария?(Минусы...) Я продолжаю думать итератор, но мне сказали, что ACL2 использует только рекурсию (defun keep-at-most-n-bits (…
18 окт '18 в 16:59
1 ответ

Рекурсивное добавление списков в начало элемента в списке

Используя acl2, я пытаюсь создать функцию "ins", которая рекурсивно добавляет первый аргумент (список) в начало каждого элемента во втором аргументе (другой список), где (ins (something) ( (a b c) (d e f) ...)) возвращается ( (something a b c) (some…
01 дек '15 в 21:28
1 ответ

Отсортированная карта в ACL2

Я должен использовать отсортированную структуру карты / индекса в ACL2. В настоящее время у меня есть следующее: ( (key1 . (val1 val2)) (key2 . (val3)) (key3 . (val4 val5 val6)) ) Есть ли другой способ сделать это более эффективно?
10 ноя '14 в 11:50