#!/usr/bin/env swipl % Quick fwd test :- include(test_header). :- use_module(library(statistics)). :- mpred_notrace_exec. :- statistics. :- cls. % reset runtime counter :- statistics(runtime,_Secs). %~path(X,X). transitive(P) ==> ((t(P,X,Y),t(P,Y,Z)/(dif(X,Y),dif(Y,Z),dif(X,Z)))==> t(P, X, Z)). taxinomicPair(E,P) ==> (t(P,X,Y),t(E,Y,Z) ==> t(P, X, Z)). subRelation(E,P) ==> ((t(E,X,Y)/(dif(X,Y))) ==> t(P,X,Y)). edge(1,2). edge(2,3). edge(3,4). subRelation(edge,hop). subRelation(hop,path). symmetric(hop). symmetric(P) ==> (t(P,X,Y)/dif(X,Y) ==> t(P,Y,X)). antisymmetric(P)/fail ==> (t(P,X,Y)/dif(X,Y) ==> ~t(P,Y,X)). reflexive(P) ==> t(P,X,X). antireflexive(P) ==> ~t(P,X,X). :- cls. % things that cannot be true are removed % unneeded when loaded from main system: ~t(P,X,X) ==> \+ t(P,X,X). :- mpred_why(edge(X,Y)==>hop(X,Y)). % bug .. giving the wrong proof! :- mpred_why(edge(X,Y)==>hop(Y,X)). % bug .. not giving any proof! :- dif(X,Y), mpred_why(edge(X,Y)==>hop(Y,X)).