fixing --plato

RELEASE

@@ -1,5 +1,6 @@
                                   EYE release
 
+v11.2.11 (2025-01-04) fixing --plato
 v11.2.10 (2025-01-03) fixing --plato for existential rules
 v11.2.9 (2025-01-03) renaming to plato (prolog with IRI atoms)
 v11.2.8 (2025-01-02) renaming to wepl (webized prolog)

VERSION

@@ -1 +1 @@
-11.2.10
+11.2.11

eye.pl

@@ -22,7 +22,7 @@
 :- catch(use_module(library(process)), _, true).
 :- catch(use_module(library(http/http_open)), _, true).
 
-version_info('EYE v11.2.10 (2025-01-03)').
+version_info('EYE v11.2.11 (2025-01-04)').
 
 license_info('MIT License
 
@@ -789,8 +789,8 @@
         format("~w~n", [Version])
     ),
     forall(
-        (Conc :+ _),
-        dynify(Conc)
+        (Conc :+ Prem),
+        dynify((Conc :+ Prem))
     ),
     eam2,
     throw(halt(0)).
@@ -5310,7 +5310,10 @@
                 ;   true
                 ),
                 throw(halt(2))
-            ;   labelvars(Conc, 0, _),
+            ;   (   Conc \= (_ :+ _)
+                ->  labelvars(Conc, 0, _)
+                ;   true
+                ),
                 \+Conc,
                 astep2((Conc, step(Rule, Prem, Conc))),
                 retract(brake)
@@ -12651,7 +12654,9 @@
 dynify(A) :-
     A =.. [B|C],
     length(C, N),
-    (   current_predicate(B/N)
+    (   (   current_predicate(B/N)
+        ;   B = /
+        )
     ->  true
     ;   dynamic(B/N)
     ),

plato/diamond-property.pl

@@ -4,8 +4,6 @@
 
 :- op(1200, xfx, :+).
 
-:- dynamic('<urn:example:not_r>'/2).
-
 '<urn:example:re>'(a, b), '<urn:example:re>'(a, c) :+ true.
 
 % equality axioms

plato/gps.pl

@@ -50,7 +50,6 @@
     forall(member(F, E), assertz(F)).
 
 % test data
-:- dynamic('<urn:example:location>'/2).
 
 % partial map of Belgium
 '<urn:example:description>'(
@@ -103,7 +102,7 @@
 ).
 
 % current state
-'<urn:example:location>'('<urn:example:i1>', '<urn:example:gent>').
+'<urn:example:location>'('<urn:example:i1>', '<urn:example:gent>') :+ true.
 
 % query
 true :+

plato/multi-agent.pl

@@ -3,8 +3,6 @@
 
 :- op(1200, xfx, :+).
 
-:- dynamic('<urn:example:completed>'/1).
-
 % define agents
 '<urn:example:agent>'('<urn:example:agent1>').
 '<urn:example:agent>'('<urn:example:agent2>').

plato/output/gps.pl

@@ -28,6 +28,9 @@
                                   ])).
 
 % proof steps
+  step(('<urn:example:location>'('<urn:example:i1>', '<urn:example:gent>'):+true),
+       true,
+       '<urn:example:location>'('<urn:example:i1>', '<urn:example:gent>')).
   step((true:+'<urn:example:findpath>'('<urn:example:map_be>', ['<urn:example:location>'(_, '<urn:example:oostende>'), _, _, _, _, _, [5000.0, 5.0, 0.2, 0.4, 1]])),
        '<urn:example:findpath>'('<urn:example:map_be>',
                                 [ '<urn:example:location>'('<urn:example:i1>',

plato/output/qiana.pl

@@ -0,0 +1,25 @@
+:- op(1200, xfx, :+).
+
+% answers
+  answer('<urn:example:believes>'('<urn:example:Fabian>',
+                                  ('<urn:example:notNecessarilyA>'(A, '<urn:example:gold>'):+'<urn:example:glitter>'(A)))).
+  answer('<urn:example:notNecessarilyA>'('<urn:example:northStar>',
+                                         '<urn:example:gold>')).
+
+% proof steps
+  step((A:+'<urn:example:says>'('<urn:example:Einstein>', A)),
+       '<urn:example:says>'('<urn:example:Einstein>',
+                            ('<urn:example:notNecessarilyA>'(B, '<urn:example:gold>'):+'<urn:example:glitter>'(B))),
+       ('<urn:example:notNecessarilyA>'(B, '<urn:example:gold>'):+'<urn:example:glitter>'(B))).
+  step((true:+'<urn:example:believes>'('<urn:example:Fabian>', _)),
+       '<urn:example:believes>'('<urn:example:Fabian>',
+                                ('<urn:example:notNecessarilyA>'(A, '<urn:example:gold>'):+'<urn:example:glitter>'(A))),
+       true).
+  step(('<urn:example:notNecessarilyA>'(A, '<urn:example:gold>'):+'<urn:example:glitter>'(A)),
+       '<urn:example:glitter>'('<urn:example:northStar>'),
+       '<urn:example:notNecessarilyA>'('<urn:example:northStar>',
+                                       '<urn:example:gold>')).
+  step((true:+'<urn:example:notNecessarilyA>'(_, _)),
+       '<urn:example:notNecessarilyA>'('<urn:example:northStar>',
+                                       '<urn:example:gold>'),
+       true).

plato/qiana.pl

@@ -0,0 +1,18 @@
+% Qiana examples
+% See https://github.com/dig-team/Qiana
+
+% says(Einstein, not (forall x: glitters(x) => gold(x)))
+'<urn:example:says>'('<urn:example:Einstein>', ('<urn:example:notNecessarilyA>'(X, '<urn:example:gold>') :+ '<urn:example:glitter>'(X))).
+
+% example
+'<urn:example:glitter>'('<urn:example:northStar>').
+
+% forall phi, x: says(Einstein, phi) => believes(x, phi)
+'<urn:example:believes>'(_, Phi) :- '<urn:example:says>'('<urn:example:Einstein>', Phi).
+
+% forall phi: says(Einstein, phi) => phi
+Phi :+ '<urn:example:says>'('<urn:example:Einstein>', Phi).
+
+% queries
+true :+ '<urn:example:believes>'('<urn:example:Fabian>', _).
+true :+ '<urn:example:notNecessarilyA>'(_, _).

plato/superdense-coding.pl

@@ -21,8 +21,6 @@
 
 :- op(1200, xfx, :+).
 
-:- dynamic('<urn:example:sdcoding>'/2).
-
 % |R) = |0, 0) + |1, 1)
 r(false, false).
 r(true, true).

plato/workplace-benchmark.pl

@@ -2,8 +2,6 @@
 
 :- op(1200, xfx, :+).
 
-:- dynamic('<urn:example:does>'/2).
-
 % facts about what employees are doing
 '<urn:example:prepare>'(X, Y) :-
     Z is Y//3,