问题标签 [acl2]

我需要做这样的事情，但在 ACL2 中：

它使用 COMMON LISP，但我不知道如何执行此任务...

我们不能使用标准的 Common Lisp 结构，例如 LOOP、DO。只是递归。

我有一些链接，但我觉得很难理解：

• ACL2 编程简介

基本上，我需要写一个标题所说的内容，我能想到的唯一关系是，如果我从列表中取出一些元素TAKE，然后取出不那么重要的另一半，然后再CDR取出APPEND两个我用来证明它与原始列表相同。（经过长时间的痛苦构建），证明似乎很好（它编译得很好），但由于某种原因，它在运行时失败了。我正在将 Proofpad 与 Dracula 一起使用，以防您需要信息。

这是代码：

这是我得到的错误日志。

至少有人能指出我正确的方向吗？我已经阅读了错误日志，我得到的是存在某种冗余。我根本不知道如何解决这个问题。

如果我这样做（'(1 2 3 4)而不是(random-integer-list)），则会引发错误：

我的设置：

1. 安装球拍

2. 打开它并运行以下代码：

   (磅)lang 球拍 (需要 (planet cce/dracula:8:23/lang/dracula))

3. 重新启动 Racket 博士。单击窗口底部的“选择语言”，然后在 Dracula 下选择 ACL2。

4. 从 Dracula 菜单中，选择“Change ACL2 Executable Path...”，然后选择位于 proofpad 安装文件夹（即“C:\Program Files (x86)\Proof”中的“run_acl2”（或“run_acl2.exe”） Pad”，如果您有 64 位 PC）

5. 下载 PSP++ 并运行它。一定要解压到Proofpad的安装目录下，不然会告诉你没找到需要的东西。

在常见的 lisp 中有map，它可以让你做这样的事情：

返回(2 2 2 2 2 2)

但是现在我在 ACL2 工作，没有map. 所以在我看来，我剩下的唯一选择就是递归计算我想要的，除非有另一种更简单和/或更有效的方法。

...这正是我的问题。有没有比创建一个称为类似的递归函数更好的方法divide-two-lists？感觉就像是基于 lisp 的语言自然应该做的事情，而不是让你专门为它创建另一个函数，这就是我问的原因。

我看到很多关于如何使用 ACL2 来证明代码的资源，正如您所期望的那样，但没有关于如何在生产中使用您的证明代码的资源。

我是否可以调整我的 ACL2 代码以使用 CLISP/Scheme/Clojure？ACL2 也可以运行我的代码吗？（教程在哪里，我使用 ACL2 不是按照它的目的吗？）

谢谢！

我正在尝试编写与 Centaur ACL2-Bridge 的绑定。到目前为止，我可以按照以下顺序启动桥接：

1. cd books
2. sudo acl2
3. acl2 !> (include-book centaur/bridge/acl2/top)
4. acl2 !> (bridge::start "Users/Brian/Desktop/acl2server")

现在，发送命令会产生错误：

也许这是一个编译错误，或者是系统中的一个错误，我还不确定。 acl2 --version产量Version 1.10-dev-r16020M-trunk (DarwinX8664)

谢谢你的帮助！

I am trying to solve problems on LISP and I am stuck with this problem for many days.

"Write a function, called wheres-waldo, that takes a lisp object (i.e., a data structure built from conses) as argument and returns a Lisp expression that extracts the symbol waldo from this object, if it is present"

For example,

E.g: (wheres-waldo '(emerson ralph waldo)) =

E.g: (wheres-waldo '(mentor (ralph waldo emerson) (henry david thoreau))) =

I have written some recursion for example,

I found this question from http://ai.eecs.umich.edu/people/wellman/courses/eecs492/f94/MP1.html wheres-waldo. Any help would be appreciated. Thank you.

我试图证明以下函数是正确的，并且很难弄清楚，即使它看起来很明显！

通过这样做，我只需要使用以下函数证明 (app (rev x) (rev y)) 等效于 (rev (app xy))))：

这就是我做另一个的方式（希望是正确的）

“反向附加东西”

= 转速的定义

= rev 的输出合约

= "反向追加事物"

= rev 的输出合约

= len 的定义

= rev 的输出合约

我在使用 acl2 时遇到了一些问题，试图证明以下内容：

这导致：

但是，当我尝试：

它很容易成功。有谁知道为什么会发生这种情况以及如何解决？

如何在 ACL2 中禁用跳过证明警告？包括故意有很多跳过证明的书籍可能非常冗长。

如何禁用太多ifs启发式？有时证明者出去吃午饭，当我打断它时，我可以看到证明者正忙于调用too-many-ifs0and count-ifs-lst。