2 
| ?- [user].
compiling user for byte code...
formula_0(P, Q):- (P; Q), \+ P.

user compiled, 2 lines read - 768 bytes written, 37208 ms

yes
| ?- formula_0(P, Q).
uncaught exception: error(instantiation_error,formula_0/2)

我基本上想要做的就是问这组表达式 {P or Q, ~P} 是否可满足？

但是错误消息在这里没有帮助......

PS。答案应该是“是”，当 P = false 并且 Q = true 时，这个公式是满足的。

4

3 回答 3

3

您收到实例化错误的原因是，在将它们用作目标时，对它们知之甚少，也P无话可说Q。例如，当您询问时，您是对的：

?- G.

thenG = true是使查询成功的解决方案。但例如也是如此，G = (a=a)因为a=a也是如此。由于无法枚举所有G成功的目标，因此会出现实例化错误。但是请注意，例如，当您显式提供绑定时，您会得到预期的结果：

?- G = true, G.
G = true.

因此，您应该提供一组您感兴趣的值：

?- maplist(boolean, [P,Q]), formula(P, Q).

并定义例如：

boolean(true).
boolean(false).

以获得具体的解决方案。或者使用约束，它可以让你在使用变量之前约束它们的域。

编辑：由于对此进行了一些讨论，因此我将进行更详细的讨论。出现的主要问题是：为什么查询

?- Q.

没有唯一的解决方案成功

Q = true.

因为显然，true成功，因此是一个有效的解决方案？回答：还有其他可能的答案，因为true这不是唯一成功的目标。例如，连词(true,true)也成功。现在假设这Q = true是上述查询的唯一解决方案，那么情况将是：

?- Q, Q = (true, true).

失败（因为dif(true, (true,true))它本身就是真的），但只是简单地交换目标

?- Q = (true,true), Q.

成功，因为否则?- true, true也将失败，而事实并非如此。对于最基本的谓词（统一），这已经违反了合取的交换性。

请注意，虽然true和(true,true) 都在作为目标执行时成功，但它们显然是不同的术语，通常不能相互替代。类似地，术语与术语append([], [], [])不同true，尽管两者在作为目标执行时都会成功。Q因此，您会遇到实例化错误，因为在查询?- Q.中对提供有用结果的了解太少。

于 2013-10-09T08:18:50.203 回答
3

使用对布尔值进行约束逻辑编程。_

:- 使用模块（库（clpb））。

示例查询：

?- sat((P+Q) * ~P).
P = 0, Q = 1.                   % succeeds deterministically
于 2015-11-13T13:29:48.237 回答
1

Gnu Prolog 支持“裸变量”调用，这是一种语法功能，允许编写您在formula_0/2. 但是在执行它时，必须绑定变量！

| ?- P.            
uncaught exception: error(instantiation_error,top_level/0)

| ?- P=write(1), P.
1
P = write(1)

然后只需使用可调用对象：

| ?- formula_0(fail,true). 
yes
于 2013-10-09T08:16:24.360 回答