我想使用如下谓词:
range(X,0,5)
range(X,4,200)
range(X,-1000000,1000000)
dom_range(X,-1000000,1000000)
含义:
range(X,0,5) :- member(X,[0,1,2,3,4,5]).
range(X,4,200) :- member(X,[4,5,6...198,199,200]).
range(X,-1000000,1000000) :- member(X,[-1000000,...,1000000]).
dom_range(X,-1000000,1000000) :- domain(X, [-1000000,...,1000000]).
如何在Prolog中很好地编码(考虑解决方案性能 - 递归的深度等)？
预计解决方案将在GNU-Prolog上运行.
PS问题受到这个问题的启发.
我正在尝试从Java中的文本文件中读取Unicode代码点.本InputStreamReader类返回流的内容int通过int,我希望会做我想做的,但它并不构成代理对.
我的测试程序:
import java.io.*;
import java.nio.charset.*;
class TestChars {
public static void main(String args[]) {
InputStreamReader reader =
new InputStreamReader(System.in, StandardCharsets.UTF_8);
try {
System.out.print("> ");
int code = reader.read();
while (code != -1) {
String s =
String.format("Code %x is `%s', %s.",
code,
Character.getName(code),
new String(Character.toChars(code)));
System.out.println(s);
code = reader.read();
}
} catch (Exception e) {
}
}
}
其行为如下:
$ java TestChars
> keyboard ?. pizza
Code 6b is `LATIN SMALL LETTER K', …我正在努力学习Coq的数学证明语言,但是我在尝试证明某些东西时遇到了一些麻烦,我将其简化为以下愚蠢的陈述:
Lemma foo: forall b: bool, b = true -> (if b then 0 else 1) = 0.
这是我的尝试:
proof.
let b: bool.
let H: (b = true).
此时证明状态为:
b : bool
H : b = true
============================
thesis :=
(if b then 0 else 1) = 0
现在我想重写if条件b来true为了能够证明论点.但是,两者都是"小步"
have ((if b then 0 else 1) = (if true then 0 else 1)) by H.
和"更大的一步"
have ((if b then 0 else 1) = …我想使用 Prolog解决Dan Finkel 的“巨型猫军队之谜”。
基本上，您从 开始[0]，然后通过使用以下三种操作之一来构建此列表：添加5、添加7或取sqrt。您已成功完成游戏的时候，你已经成功地建立一个列表，这样2，10和14出现在列表中，顺序，并且可以有他们之间的其他数字。
规则还要求所有元素都是不同的，它们都是<=60并且都只是整数。例如，从 开始[0]，您可以应用(add5, add7, add5)，这将导致[0, 5, 12, 17]，但由于它没有 2,10,14 的顺序，它不能满足游戏。
我想我已经成功地编写了所需的事实，但我不知道如何实际构建列表。我认为使用dcg是一个不错的选择，但我不知道如何。
这是我的代码：
:- use_module(library(lists)).
:- use_module(library(clpz)).
:- use_module(library(dcgs)).
% integer sqrt
isqrt(X, Y) :- Y #>= 0, X #= Y*Y.
% makes sure X occurs before Y and Y occurs before Z
before(X, Y, Z) --> ..., [X], ..., …我正在努力学习Coq,但我发现很难从我在软件基础和依赖类型认证编程中读到的内容跳到我自己的用例.
特别是,我想我会尝试nth在列表上创建一个经过验证的函数版本.我设法写了这个:
Require Import Arith.
Require Import List.
Import ListNotations.
Lemma zltz: 0 < 0 -> False.
Proof.
intros. contradict H. apply Lt.lt_irrefl.
Qed.
Lemma nltz: forall n: nat, n < 0 -> False.
Proof.
intros. contradict H. apply Lt.lt_n_0.
Qed.
Lemma predecessor_proof: forall {X: Type} (n: nat) (x: X) (xs: list X),
S n < length (x::xs) -> n < length xs.
Proof.
intros. simpl in H. apply Lt.lt_S_n. assumption.
Qed. …考虑来自https://puzzling.stackexchange.com/questions/20238/explore-the-square-with-100-hops的问题：
给定一个 10x10 方格的网格，您的任务是只访问每个方格一次。在每个步骤中，您可以
- 水平或垂直跳过 2 个方块或
- 对角跳过 1 个正方形
换句话说（接近我执行以下）中，从1至100个这样的标记10×10网格数，在坐标每平方(X, Y)为1或等于一个大于“前”方在(X, Y-3)，(X, Y+3)，(X-3, Y)，(X+3, Y)，(X-2, Y-2)，(X-2, Y+2)，(X+2, Y-2)，或(X+2, Y+2).
这看起来像是一个简单的约束编程问题，Z3 可以从一个简单的声明式规范在 30 秒内解决它：https : //twitter.com/johnregehr/status/1070674916603822081
我使用 CLP(FD) 在 SWI-Prolog 中的实现不能很好地扩展。事实上，除非预先指定了几乎两行，否则它甚至无法解决问题的 5x5 实例：
?- number_puzzle_(_Square, Vars), Vars = [1,24,14,2,25, 16,21,5,8,20 |_], time(once(labeling([], Vars))).
% 10,063,059 inferences, 1.420 CPU in 1.420 seconds (100% CPU, 7087044 Lips)
_Square = square(row(1, 24, …