Testing Seeye with tpl, swipl and scryer-prolog

General
1

Seeye is a very premature “Second eye” which is under development at http://eulersharp.sourceforge.net/2021/02seeye

------------------
Second eye - Seeye
------------------

Seeye performs controlled chaining with Euler path detection.

Controlled chaining is backward chaining for rules like 'CONC :- PREM' and
forward chaining for rules like 'PREM => CONC'. For the latter the conclusion
can be a conjunction and it can also be 'false' to declare an inference fuse.

Euler paths are roughly "don't step in your own steps" which is inspired by
what Leonhard Euler discovered in 1736 for the Königsberg Bridge Problem.
Seeye sees the rule 'PREM => CONC' as 'PREM and NOT(CONC) implies CONC'.

Run all the tests via
$ ./test tpl                # using Trealla ProLog and taking about 0.690 sec
$ ./test swipl              # using SWI Prolog and taking about     1.420 sec
$ ./test scryer-prolog      # using Scryer-Prolog and taking about 33.390 sec
3

I was actually introducing (-:)/2 in illegal instruction for retina test · Issue #132 · infradig/trealla (github.com) to give the reasoner a hint to do forward chaining (instead of the usual backward chaining for (:-)/2) because I couldn’t find another way to solve the dpe.pl test case (trying hard with tabling but was loosing). But then coming from a Notation3 world where you simply say PREM => CONC as well as in the coherent logic and the TPTP world, logical implication is represented by the operator (=>)/2. I found the new use in swipl HEAD => BODY really contradictory with the classical logic use BODY => HEAD i.e. PREM => CONC.

6 
$ swipl
Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.19-2-gc2ef0f4e8)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.

For online help and background, visit https://www.swi-prolog.org
For built-in help, use ?- help(Topic). or ?- apropos(Word).

?- op(1150,xfx,'-:').
true.

?- assertz(re(b,X) -: not_re(c,X)).
true.

?- X -: Y.
X = re(b, _4036),
Y = not_re(c, _4036).


$ tpl
Trealla Prolog (c) Infradig 2020, v1.6.17
?- op(1150,xfx,'-:').
true.
?- assertz(re(b,X) -: not_re(c,X)).
true.
?- X -: Y.
X = re(b,_2),
Y = not_re(c,_2).


$ scryer-prolog
?- op(1150,xfx,'-:').
   true.
?- assertz(re(b,X) -: not_re(c,X)).
caught: error(syntax_error(incomplete_reduction),read_term/3:1)
?- assertz((re(b,X) -: not_re(c,X))).
   true.
?- X -: Y.
   X = re(b,_A), Y = not_re(c,_A).
7

See also http://eulersharp.sourceforge.net/2021/02seeye/LICENSE

9

Fair enough, am reverting to the original (-:)/2 notation.
Original in the sense of what we introduced in illegal instruction for retina test · Issue #132 · infradig/trealla (github.com)