序言中的连续演算答案

【问题标题】：Sequent calculus in prolog序言中的连续演算
【发布时间】：2019-03-02 03:48:46
【问题描述】：

我真的是 Prolog 的新手。我必须在 Prolog 中编写连续微积分的规则，我认为我做得对。如果公式有效，则代码应返回 true，否则返回 false。这是我的代码：

如果公式有效，则返回 true。

但如果我使用无效的公式运行代码，它永远不会结束，我真的不知道如何修复它。

查询 -? sc([ ],[ (neg ((neg p)or neg (neg p)))]). 应该返回 false，因为该公式无效。

我将不胜感激。

【问题讨论】：

请不要将您的代码作为图片发布。将其发布为文本，以便我们可以使用它。大多数用户不会尝试以文本形式回答没有代码的问题。
对不起，我会在以后将其作为文本发布。
这是否意味着您要编辑这个问题？
请显示您运行的查询和预期的结果。
请编辑您的问题并将代码的实际文本放在那里。全部选中并单击{} 按钮以正确格式化。你知道[ (neg ((neg p)or neg (neg p)))] 是一个元素的列表吗？

标签： prolog logic runtime-error

【解决方案1】：

析取规则有错误。进一步的排列规则是一个结构规则：

G, A, B, D |- C
---------------
G, B, A, D |- C

您应该对其进行编码，使其不会循环。但现在这完全可以发生。有一个简单的技巧，也许你想实现它，只将非原子交换到前面。

这是一个清理后的版本：

:- use_module(library(basic/lists)).

sc([neg(A)|L],R) :- !, sc(L,[A|R]).
sc(L,[neg(A)|R]) :- !, sc([A|L],R).
sc(L,[or(A,B)|R]) :- !, sc(L,[A,B|R]).
sc([or(A,B)|L],R) :- !, sc([A|L],R), sc([B|L],R).
sc([A|L],R) :- atom(A), select(B,L,H), compound(B), !, sc([B,A|H],R).
sc(L,[A|R]) :- atom(A), select(B,R,H), compound(B), !, sc(L,[B,A|H]).
sc(L,R) :- member(A,L), member(A,R), !.

这里有一些运行：

Jekejeke Prolog 3, Runtime Library 1.3.5
(c) 1985-2019, XLOG Technologies GmbH, Switzerland

?- sc([],[neg(or(neg(p),neg(neg(p))))]).
No
?- sc([],[or(neg(p),neg(neg(p)))]).
Yes

备注：我已经将身份规则移到最后，所以它只会命中原子。我已经放置了削减，一些inversion lemmas 证明了经典逻辑是合理的。可能不适用于其他逻辑或出现非地面问题时。

【讨论】：

哦，谢谢。我刚刚以不同的方式使用排列对我的代码进行了另一种更正，它可以工作。
我刚刚发布了我的新代码。是否总是需要将身份规则放在最后？ @j4n 烧伤53
不，我猜你也可以允许规则 G, A |- A, D 而不仅仅是 G, P |- P, D。至少在经典逻辑中我猜你可以证明前者也是可导出的。
我刚刚看到，你的身份规则是正确的。前提是 intersection/3 谓词足够稳定，可以这样调用。所以我编辑了我的帖子，身份规则没有错误。

【解决方案2】：

:- use_module(library/basic/lists)).

sc(I,D) :- \+(intersection(I,D,[])),!.
sc([(neg F)|I],D) :- sc2(I,[F|D]),!.
sc(I,[(neg F)|D]) :- sc2([F|I],D),!.
sc(I,[(F1 or F2)|D]) :- union([F1,F2],D,D1),sc2(I,D1),!.
sc([(F1 or F2)|I],D) :- sc2([F1|I],D),sc2([F2|I],D),!.
sc2(I,D):-permutation(I,I1),permutation(D,D1),sc(I1,D1).

【讨论】：

你又试过 sc([],[neg(or(neg(p),neg(neg(p))))]) 了吗？