prolog - λProlog 拒绝假设的推理查询？

Question

我怀疑 λProlog 的主要实现 teyjus 可能是一个废弃软件，但 λProlog 是一个令人着迷的 Prolog，它应该让你使用高阶逻辑、假设推理和其他东西，这就是为什么我'我正在尝试使用它。

文件“example.sig”:

sig example.

kind person, language type.

type hans person.
type german, french, italian language.

type grade person -> o.
type take person -> language -> o.

文件“example.mod”:

module example.

(grade P) :- (take P german), (take P french).
(grade P) :- (take P german), (take P italian).

take hans french.

但是，当我编译和加载它时，虽然它似乎可以工作，但假设的推理查询被拒绝:

[example] ?- take X Y.

The answer substitution:
Y = french
X = hans

More solutions (y/n)? y

no (more) solutions

[example] ?- grade X.

no (more) solutions

[example] ?- (take hans german) => (grade hans).
(1,19) : Error : Symbol => is not permitted within terms

我期待在最后一个"is"。我做错了什么？

Answer 1

当前版本的 Teyjus 不允许将查询中的含义直接输入到顶层。 Gopalan Nadathur 和我的书 (Programming with Higher-Order Logic) 在附录中提到了这个问题和解决方法(请参阅下面的摘录)。

A.4.2 与本书假设语言的偏差(第 287 页)

[...]

Teyjus 不允许在顶级目标中使用含义。当编译模型也扩展到这些目标时，这个特性可能会在将来发生变化，但就目前而言，这意味着某些示例(例如，在第 3.2 节中)不能直接使用该系统运行。请注意，仅在顶级目标中不允许使用含义:它们可以在出现在程序子句主体中的目标中自由使用。因此，可以通过首先构建一个合适的程序子句然后使用它来提出所需的查询来克服这个限制。例如，而不是提出查询

?- p a => p b => p X.

可以创建子句

test X :- p a => p b => p X.

然后使用查询

?- test X.