adding --logic-program <pl-file> option

RELEASE

@@ -1,5 +1,6 @@
                                   EYE release
 
+v11.2.0 (2024-12-27) adding --logic-program <pl-file> option
 v11.1.4 (2024-12-23) using log:explains instead of log:proves
 v11.1.3 (2024-12-23) using --explain instead of --ether
 v11.1.2 (2024-12-20) replacing list:quicksort with (list ordering) list:sort sortedList where ordering can be "<", "=<", ">" and ">="

VERSION

@@ -1 +1 @@
-11.1.4
+11.2.0

eye.pl

@@ -22,7 +22,7 @@
 :- catch(use_module(library(process)), _, true).
 :- catch(use_module(library(http/http_open)), _, true).
 
-version_info('EYE v11.1.4 (2024-12-23)').
+version_info('EYE v11.2.0 (2024-12-27)').
 
 license_info('MIT License
 
@@ -63,6 +63,7 @@
     --image <pvm-file>              output all <data> and all code to <pvm-file>
     --intermediate <n3p-file>       output all <data> to <n3p-file>
     --license                       show license info
+    --logic-program <pl-file>       run logic program <pl-file>
     --max-inferences <nr>           halt after maximum number of inferences
     --no-distinct-input             no distinct triples in the input
     --no-distinct-output            no distinct answers in the output
@@ -105,6 +106,10 @@
     --pass-only-new                 output only new derived triples
     --query <n3-query>              output filtered with filter rules').
 
+:- op(1200, xfx, :=).
+
+:- dynamic((:=)/2).
+:- dynamic(answer/1).
 :- dynamic(answer/3).               % answer(Predicate, Subject, Object)
 :- dynamic(apfx/2).
 :- dynamic(argi/1).
@@ -167,6 +172,7 @@
 :- dynamic(semantics/2).
 :- dynamic(shellcache/2).
 :- dynamic(tabl/3).
+:- dynamic(step/3).
 :- dynamic(tmpfile/1).
 :- dynamic(tuple/2).
 :- dynamic(tuple/3).
@@ -292,11 +298,14 @@
     catch(gre(Argus), Exc,
         (   Exc = halt(0)
         ->  true
-        ;   (   flag('parse-only')
-            ->  true
-            ;   format(user_error, '** ERROR ** gre ** ~w~n', [Exc]),
-                flush_output(user_error),
-                nb_setval(exit_code, 3)
+        ;   (   Exc = halt(N)
+            ->  nb_setval(exit_code, N)
+            ;   (   flag('parse-only')
+                ->  true
+                ;   format(user_error, '** ERROR ** gre ** ~w~n', [Exc]),
+                    flush_output(user_error),
+                    nb_setval(exit_code, 3)
+                )
             )
         )
     ),
@@ -687,6 +696,38 @@
     format(user_error, '~w~n', [License]),
     flush_output(user_error),
     throw(halt(0)).
+opts(['--logic-program', File|_], _) :-
+    consult(File),
+    nb_setval(closure, 0),
+    nb_setval(limit, -1),
+    nb_setval(fm, 0),
+    nb_setval(mf, 0),
+    (   (_ := _)
+    ->  format(":- op(1200, xfx, :=).~n~n", [])
+    ;   version_info(Version),
+        format("~w~n", [Version])
+    ),
+    forall(
+        (   (Conc := _),
+            Conc \= true,
+            Conc \= false
+        ),
+        (   functor(Conc, P, A),
+            dynamic(P/A)
+        )
+    ),
+    eam2,
+    nb_getval(fm, Fm),
+    (   Fm = 0
+    ->  true
+    ;   format(user_error, "*** fm=~w~n", [Fm])
+    ),
+    nb_getval(mf, Mf),
+    (   Mf = 0
+    ->  true
+    ;   format(user_error, "*** mf=~w~n", [Mf])
+    ),
+    throw(halt(0)).
 opts(['--max-inferences', Lim|Argus], Args) :-
     !,
     (   number(Lim)
@@ -5248,6 +5289,90 @@
     catch(clause(B, true), _, fail),
     \+prfstep(A, _, _, _, _, _, _).
 
+% ---------------------
+% EAM2 abstract machine
+% ---------------------
+%
+% 1/ select rule Conc := Prem
+% 2/ prove Prem and if it fails backtrack to 1/
+% 3/ if Conc = true assert answer(Prem)
+%    else if Conc = false stop with return code 2
+%    else if ~Conc assert Conc and retract brake
+% 4/ backtrack to 2/ and if it fails go to 5/
+% 5/ if brake
+%       if not stable start again at 1/
+%       else output answers, output steps and stop
+%    else assert brake and start again at 1/
+%
+eam2 :-
+    (   (Conc := Prem),     % 1/
+        copy_term((Conc := Prem), Rule),
+        Prem,               % 2/
+        (   Conc = true     % 3/
+        ->  (   \+answer(Prem)
+            ->  assertz(answer(Prem))
+            ;   true
+            )
+        ;   (   Conc = false
+            ->  format("% inference fuse, return code 2~n", []),
+                portray_clause(fuse(Prem)),
+                throw(halt(2))
+            ;   (   term_variables(Conc, [])
+                ->  Concl = Conc
+                ;   Concl = (Conc := true)
+                ),
+                \+Concl,
+                astep2(Concl),
+                assertz(step(Rule, Prem, Concl)),
+                retract(brake)
+            )
+        ),
+        fail                % 4/
+    ;   (   brake           % 5/
+        ->  (   nb_getval(closure, Closure),
+                nb_getval(limit, Limit),
+                Closure < Limit,
+                NewClosure is Closure+1,
+                nb_setval(closure, NewClosure),
+                eam2
+            ;   answer(Prem),
+                portray_clause(answer(Prem)),
+                fail
+            ;   (   step(_, _, _)
+                ->  format("~n%~n% Proof steps~n%~n~n", []),
+                    step(Rule, Prem, Conc),
+                    portray_clause(step(Rule, Prem, Conc)),
+                    fail
+                ;   true
+                )
+            ;   true
+            )
+        ;   assertz(brake),
+            eam2
+        )
+    ).
+
+% assert new step
+astep2((B, C)) :-
+    astep2(B),
+    astep2(C).
+astep2(A) :-
+    (   \+A
+    ->  assertz(A)
+    ;   true
+    ).
+
+% stable(+Level)
+%   fail if the deductive closure at Level is not yet stable
+stable(Level) :-
+    nb_getval(limit, Limit),
+    (   Limit < Level
+    ->  nb_setval(limit, Level)
+    ;   true
+    ),
+    nb_getval(closure, Closure),
+    Level =< Closure.
+
 %
 % DJITI (Deep Just In Time Indexing)
 %
@@ -9200,7 +9325,7 @@
             ->  getbool(B, V)
             ;   V = B
             ),
-            inv(U, V)
+            invert(U, V)
         )
     ).
 
@@ -12303,8 +12428,8 @@
     ;   catch(call(C), _, fail)
     ).
 
-inv(false, true).
-inv(true, false).
+invert(false, true).
+invert(true, false).
 
 +(A, B, C) :-
     plus(A, B, C).

logic-programming/README.md

@@ -0,0 +1,19 @@
+# Logic Programming
+
+- Using webized prolog which basically means that atoms can be IRIs.
+- Besides top-down reasoning with `conclusion :- premise` rules, it also does bottom-up reasoning with `conclusion := premise` rules.
+- Bottum-up reasoning can use `stable(n)` to fail if the deductive closure at level `n` is not yet stable.
+- Proofs steps are `step((conclusion := premise), premise_inst, conclusion_inst)` and `conclusion_inst` is asserted.
+- Variables are interpreted as universally quantified variables except for `conclusion := premise` conclusion-only variables which are interpreted existentially.
+- Queries are posed as `true := premise` and answered as `answer(premise_inst)`.
+- Inference fuses are defined as `false := premise` and blown as `fuse(premise_inst)` with return code 2.
+
+## Rationale for bottom-up reasoning with `conclusion := premise` rules
+
+- conclusion can be a conjunction
+- conclusion can be `false` to blow an inference fuse
+- conclusion can be `true` to pose a query
+- conclusion can not be any other built-in
+- conclusion-only variables are existentials
+- generating proofs using `step/3` proof steps
+- avoiding loops that could occur with backward chaining

logic-programming/ackermann.pl

@@ -0,0 +1,45 @@
+% Ackermann function
+% See https://en.wikipedia.org/wiki/Ackermann_function
+
+% ackermann(x, y, z)
+'urn:example:ackermann'([A, B], C) :-
+    D is B+3,
+    ackermann(A, D, 2, E),
+    C is E-3.
+
+% succ (x=0)
+ackermann(0, A, _, B) :-
+    !,
+    B is A+1.
+
+% sum (x=1)
+ackermann(1, A, B, C) :-
+    !,
+    C is A+B.
+
+% product (x=2)
+ackermann(2, A, B, C) :-
+    !,
+    C is A*B.
+
+% exponentiation (x=3), tetration (x=4), pentation (x=5), hexation (x=6), etc
+ackermann(_, 0, _, 1) :-
+    !.
+ackermann(A, B, C, D) :-
+    E is B-1,
+    ackermann(A, E, C, F),
+    G is A-1,
+    ackermann(G, F, C, D).
+
+% queries
+true := 'urn:example:ackermann'([0, 6], _).
+true := 'urn:example:ackermann'([1, 2], _).
+true := 'urn:example:ackermann'([1, 7], _).
+true := 'urn:example:ackermann'([2, 2], _).
+true := 'urn:example:ackermann'([2, 9], _).
+true := 'urn:example:ackermann'([3, 4], _).
+true := 'urn:example:ackermann'([3, 14], _).
+true := 'urn:example:ackermann'([4, 0], _).
+true := 'urn:example:ackermann'([4, 1], _).
+true := 'urn:example:ackermann'([4, 2], _).
+true := 'urn:example:ackermann'([5, 0], _).

logic-programming/acp.pl

@@ -0,0 +1,51 @@
+% Access control policy example
+
+'urn:example:policy'('urn:example:test1', 'urn:example:PolicyX').
+'urn:example:has'('urn:example:test1', 'urn:example:A').
+'urn:example:has'('urn:example:test1', 'urn:example:B').
+'urn:example:has'('urn:example:test1', 'urn:example:C').
+'urn:example:Policy'('urn:example:PolicyX').
+'urn:example:allOf'('urn:example:PolicyX', 'urn:example:A').
+'urn:example:allOf'('urn:example:PolicyX', 'urn:example:B').
+'urn:example:anyOf'('urn:example:PolicyX', 'urn:example:C').
+'urn:example:noneOf'('urn:example:PolicyX', 'urn:example:D').
+
+'urn:example:pass'(A, 'urn:example:allOfTest') :-
+    'urn:example:policy'(B, A),
+    'urn:example:Policy'(A),
+    forall(
+        'urn:example:allOf'(A, C),
+        'urn:example:has'(B, C)
+    ).
+
+'urn:example:pass'(A, 'urn:example:anyOfTest') :-
+    'urn:example:policy'(B, A),
+    'urn:example:Policy'(A),
+    findall(C,
+        (
+            'urn:example:anyOf'(A, C),
+            'urn:example:has'(B, C)
+        ),
+        D
+    ),
+    length(D, E),
+    E \= 0.
+
+'urn:example:pass'(A, 'urn:example:noneOfTest') :-
+    'urn:example:policy'(B, A),
+     'urn:example:Policy'(A),
+    findall(C,
+        (
+            'urn:example:noneOf'(A, C),
+            'urn:example:has'(B, C)
+        ),
+        D
+    ),
+    length(D, 0).
+
+% query
+true :=
+    'urn:example:Policy'(A),
+    'urn:example:pass'(A, 'urn:example:allOfTest'),
+    'urn:example:pass'(A, 'urn:example:anyOfTest'),
+    'urn:example:pass'(A, 'urn:example:noneOfTest').

logic-programming/age.pl

@@ -0,0 +1,15 @@
+% age checker
+
+% person data
+'urn:example:birthDay'('urn:example:patH', [1944, 8, 21]).
+
+% is the age of a person above some years?
+'urn:example:ageAbove'(S, A) :-
+    'urn:example:birthDay'(S, [Yb, Mb, Db]),
+    Ya is Yb+A,
+    date_time_stamp(date(Ya, Mb, Db, 22, 0, 0, _, _, _), Tc),
+    get_time(T),
+    Tc =< T.
+
+% query
+true := 'urn:example:ageAbove'(_, 80).