Здесь вы:
function neat_trim($str, $n, $delim='…') {
$len = strlen($str);
if ($len > $n) {
preg_match('/(.{' . $n . '}.*?)\b/', $str, $matches);
return rtrim($matches[1]) . $delim;
}
else {
return $str;
}
}
:- 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).
В правиле дизъюнкции есть ошибка. Далее, правило перестановки является структурным правилом:
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
Замечания: я переместил правило идентификации до конца, поэтому оно будет только ударить атомы. Я поместил разрезы, что оправдано некоторыми леммами обращения для классической логики. Может не работать для других логик или когда возникают неосновательные проблемы.