我想知道在以下情况下如何重新排列目标: proof (rule iffI, (*here I would like to swap goal order*), rule ccontr我意识到prefer和defer可以用于应用样式的证明,但我希望有一种方法可以用于proof (...)部分。编辑:
正如Andreas所说,在上面的示例中编写rule iffI[rotated]是有效的。然而,在以下情况下,是否可以在不改变引理语句的情况下交换目标顺序?>
我正在阅读和Bratko的人工智能Prolog编程,第5章:控制回溯。起初,切分似乎是模仿其他编程语言中已知的if-else子句的一种直接方式。原因很清楚:第一条规则失败了,第二条规则不再有任何与它相关的条件,所以它会成功。我理解这一点,但随后提出了一个解决方案(以下是一个):
max(X,Y,Z):- X =< Y,!, Y = Z.之前的所有内容都是真的,停止终止,包括任何具有相同谓词的其他规则”。但是,这不可能是正确的,因为这意味着Y = Z的实例化只能在失败的情况下进行,这对于该规则来说是无