标签: logic-programming

我想从SWI-Prolog切换到Prova-但似乎比预期的要难：

像这样succ()的谓词不可用，而像Var1+Var2>Var3这样的操作不起作用（显然它必须Var3<Var1+Var2是有效的）。

是否有可用的文档描述Prolog方言之间的差异？

当我的朋友开始在学校学习Prolog时,我取笑他学习一种无用的语言.然而,他向我展示了一些我从未知道的东西; 我想知道这种技术的来源.

技术是这样的:

permutation(List) :-
    isAMember(X, List),
    deleteFirstElement(X, List, Substring),
    % and so on

在这段代码中,isAMember(X, List)是一个函数,如果X在,则返回true List.然而,到现在为止X没有被定义为一个变量- 这样的计划将产生一堆新的线程,每一个可能的值X,使isAMember(X, List)真实的,并从那里继续.

这使我们能够以我能想象到的最简单,最优雅的方式创建多线程算法.

所以我的问题是: 这是Prolog特定的,还是所有逻辑和/或功能语言的特征？ 另外,我在哪里可以学到更多这样令人惊叹的多线程技术 - 这无疑是编程的未来.

我一直在研究声明性语言,似乎声明只是逻辑和函数语言的总称.还是我错了？是否有任何通用的声明性编程语言不能归类为功能或逻辑(al),只是"声明"？

我正在尝试使用core.logic,并希望启用我自己的自定义数据类型来参与逻辑表达式:

(deftype Expression [node vars]
  ....)

基本上,这表示数学表达式树中的节点,包含节点树和一组未使用的未绑定变量.node是常量,符号或(Operator Expression Expression....)树节点.我希望能够使用core.logic来操纵数学表达式,并匹配这些表达式的子树.

如果可能的话,我怎么能这样做？

我从core.logic源代码中看到,有许多协议看起来好像可以扩展(例如IUnifyTerms,IReifyTerms等等)但是它们并不完全清楚这些都是如何使用的,以及我真正使用的那些需要扩展.

是否有任何prolog实现能够枚举可数无限结果的所有元素？

让我们考虑列举所有自然数对.如果我们按{(0,0),(0,1),(1,0),(0,2),(1,1),(2,0),...}的顺序枚举对,我们可以枚举所有对.但是,如果我们按照{(0,0),(0,1),(0,2),(0,3)...}的顺序枚举对作为以下GNU prolog程序,我们永远不会达到诸如( 1,1).

% cat nats.pl
nat(0).
nat(X1) :- nat(X), X1 is X + 1.

pair_of_nats(X, Y) :- nat(X), nat(Y).
% prolog
GNU Prolog 1.3.0
By Daniel Diaz
Copyright (C) 1999-2007 Daniel Diaz
| ?- ['nats.pl'].
compiling /home/egi/prolog/nats.pl for byte code...
/home/egi/prolog/nats.pl compiled, 4 lines read - 762 bytes written, 9 ms

yes
| ?- pair_of_nats(X,Y).

X = 0
Y = 0 ? ;

X = 0
Y = 1 ? ;

X = 0
Y = 2 ? …

我想在一些可能被称为完全声明的Horn逻辑(或完全声明的Prolog)中形式化一些知识并执行查询.任何人都可以提供一些如何实施它的指导方针吗？我简要回顾一下上面链接中的精细描述:

形式语言是Prolog的核心语言:"程序"是Prolog中的一组规则和事实(包括函数和变量,基本上只包含用户定义的谓词).

然而,与Prolog相比,我正在寻找一种完整的逻辑程序标准声明语义 - 最少Herbrand模型(即归纳定义的基础术语集).在逻辑编程的理论工作中,这通常是研究的对象,众所周知,可以获得对查询的完整和完整的答案(在"递归可枚举的"意义上),例如,使用SLD解析以下条件:

• 公平搜索匹配规则(例如,Prolog的深度优先搜索不公平);
• 与" 发生检查 " 统一(检查变量在与其统一的术语中不会发生).

我正在寻找一个简洁的实现,它将建立在现有功能的基础上,而不是发明轮子.我看到的两个更有希望的方向是将它作为Prolog的元解释器实现,或者作为一些定理证明器的一部分.任何在这些领域具有实践知识的人都能提供一些如何实施它的指导方针吗？可以在miniKanren中轻松实现吗？

我的意图是以完全陈述的方式形式化一些知识.这种形式化的关键特征是它精确地对应于(单调)归纳的数学概念,因此可以通过归纳论证容易地推理知识及其属性.

我需要找到所有 16 位数字 ( x, y, z) 的三元组（实际上只有在不同三元组中与相同位置的位完美匹配的位），这样

y | x = 0x49ab
(y >> 2) ^ x = 0x530b
(z >> 1) & y = 0x0883
(x << 2) | z = 0x1787

直接使用 8700K 的策略需要大约 2 天，这太多了（即使我会使用我可以访问的所有 PC（R5-3600、i3-2100、i7-8700K、R5-4500U、3xRPi4、RPi0/W）这将花费太多时间）。

如果位移位不在等式中，那么这样做将是微不足道的，但是使用位移位很难做同样的事情（甚至可能是不可能的）。

所以我想出了一个非常有趣的解决方案：将方程解析为关于数字位的语句（类似于“x XOR 的第 3 位 XOR y 的第 1 位等于 1”），并且所有这些语句都用 Prolog 语言之类的语言编写（或只是解释他们使用真值表操作）执行所有明确的位将被发现。这个解决方案也很困难：我不知道如何编写这样的解析器，也没有 Prolog 的经验。(*)

所以问题是：这样做的最佳方法是什么？如果是 (*) 那么怎么做呢？

编辑：为了更容易在此处编码数字的二进制模式：

0x49ab = 0b0100100110101011
0x530b = 0b0101001100001011
0x0883 = 0b0000100010000011
0x1787 = 0b0001011110000111

我正在尝试解决一个练习,以便更熟悉prolog.

任务如下:

% Sten wants to send Lisa 100 flowers. He can choose from lilies, roses and tulips.
% One lily costs $50, rose $10 and tulip $1. Find how many flowers of each type he 
% must buy, so that he spends exactly $500.

我已经解决了这个练习,但我觉得有点笨重.我的代码是:

% numbers 1..100
digit(1). digit(2). digit(3). digit(4). digit(5). digit(6). digit(7). digit(8).
digit(9). digit(10). digit(11). digit(12). digit(13). digit(14). digit(15). digit(16). 
digit(17). digit(18). digit(19). digit(20). digit(21). digit(22). digit(23). digit(24). 
digit(25). digit(26). digit(27). digit(28). digit(29). digit(30). digit(31). …

我一直在使用Clojure.logic 完成The Reasoned Schemer(TRS),并注意这里记录的差异.我到达了第3章第24帧,TRS报告了这一点

(run 5 [x]
  (lolo '((a b) (c d) . x)))

应该产生

'(()
  (())
  (() ())
  (() () ())
  (() () () ())

现在,我实现了`lolo as

(defn lolo
  "Succeeds if l is a list-of-lists."
  [l]
  (conde
   ((emptyo l) s#)
   ((fresh [a]
           (firsto l a)
           (listo a)) (fresh [d]
                             (resto l d)
                             (lolo d)))
   (s# u#)))

这会产生以下奇怪的结果:

'(()
  (())
  ((_0))
  (() ())
  ((_0 _1)))

这基本上意味着我的lolo正在制作泄漏新变量的解决方案.如果我继续前进,试着看一个模式,我明白了

'(()
  (())
  ((_0))
  (() ())
  ((_0 _1))
  (() …

SWI Prolog允许在非最低级别的顶级之前执行目标,如下所示

swipl -s consultingfile.pl -g start

但是,当具有非零arity的谓词指定如下时

swipl -s consultingfile.pl -g start(1)

它给出了一个错误

syntax error near unexpected token '('

如何将非零arity谓词作为最高级别之前的目标传递？