Skip to content

Commit

Permalink
having log:herbrandInterpretation and log:herbrandTerm instead of log…
Browse files Browse the repository at this point in the history
…:herbrand
  • Loading branch information
josd committed Feb 24, 2025
1 parent baa1f5c commit 2ee08b3
Show file tree
Hide file tree
Showing 38 changed files with 557 additions and 555 deletions.
1 change: 1 addition & 0 deletions RELEASE
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
EYE release

v11.9.5 (2025-02-24) having log:herbrandInterpretation and log:herbrandTerm instead of log:herbrand
v11.9.4 (2025-02-24) fixing issue https://github.com/orgs/eyereasoner/discussions/139#discussioncomment-12301405
v11.9.3 (2025-02-24) fixing issue https://github.com/eyereasoner/eye/issues/140
v11.9.2 (2025-02-24) dropping log:compoundTerm and using log:herbrand instead
Expand Down
2 changes: 1 addition & 1 deletion VERSION
Original file line number Diff line number Diff line change
@@ -1 +1 @@
11.9.4
11.9.5
3 changes: 2 additions & 1 deletion eye-builtins.n3
Original file line number Diff line number Diff line change
Expand Up @@ -154,7 +154,8 @@ log:equalTo a e:Builtin.
log:forAllIn a e:Builtin.
log:graffiti a e:Builtin.
log:hasPrefix a e:Builtin.
log:herbrand a e:Builtin.
log:herbrandInterpretation a e:Builtin.
log:herbrandTerm a e:Builtin.
log:ifThenElseIn a e:Builtin.
log:implies a e:Builtin.
log:includes a e:Builtin.
Expand Down
30 changes: 15 additions & 15 deletions eye.pl
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@
:- catch(use_module(library(process)), _, true).
:- catch(use_module(library(http/http_open)), _, true).

version_info('EYE v11.9.4 (2025-02-24)').
version_info('EYE v11.9.5 (2025-02-24)').

license_info('MIT License

Expand Down Expand Up @@ -4011,7 +4011,7 @@
wt0(fail) :-
!,
write('("fail") '),
wp('<http://www.w3.org/2000/10/swap/log#herbrand>'),
wp('<http://www.w3.org/2000/10/swap/log#herbrandInterpretation>'),
write(' true').
wt0([]) :-
!,
Expand Down Expand Up @@ -7567,20 +7567,20 @@
)
).

'<http://www.w3.org/2000/10/swap/log#herbrand>'(A, B) :-
'<http://www.w3.org/2000/10/swap/log#herbrandInterpretation>'(A, B) :-
\+flag(restricted),
atomify(A, C),
( nonvar(B),
memberchk(B, [true, false])
-> D =.. C,
( B = true
-> catch(call(D), _, fail)
; \+catch(call(D), _, fail)
)
; C = [D|E],
read_term_from_atom(D, B, [variables(E)])
D =.. C,
( B = true
-> catch(call(D), _, fail)
; \+catch(call(D), _, fail)
).

'<http://www.w3.org/2000/10/swap/log#herbrandTerm>'([literal(A, type('<http://www.w3.org/2001/XMLSchema#string>'))|B], C) :-
\+flag(restricted),
atomify(B, D),
read_term_from_atom(A, C, [variables(D)]).

'<http://www.w3.org/2000/10/swap/log#ifThenElseIn>'(A, B) :-
\+flag(restricted),
nonvar(B),
Expand Down Expand Up @@ -12601,13 +12601,13 @@
'<http://eulersharp.sourceforge.net/2003/03swap/log-rules#derive>'([literal(A, type('<http://www.w3.org/2001/XMLSchema#string>'))|B], true), C], true), when(D, C)) :-
!,
D =.. [A|B].
conjify('<http://www.w3.org/2000/10/swap/log#herbrand>'([literal(when, type('<http://www.w3.org/2001/XMLSchema#string>')),
'<http://www.w3.org/2000/10/swap/log#herbrand>'([literal(A, type('<http://www.w3.org/2001/XMLSchema#string>'))|B], true), C], true), when(D, C)) :-
conjify('<http://www.w3.org/2000/10/swap/log#herbrandInterpretation>'([literal(when, type('<http://www.w3.org/2001/XMLSchema#string>')),
'<http://www.w3.org/2000/10/swap/log#herbrandInterpretation>'([literal(A, type('<http://www.w3.org/2001/XMLSchema#string>'))|B], true), C], true), when(D, C)) :-
!,
D =.. [A|B].
conjify('<http://eulersharp.sourceforge.net/2003/03swap/log-rules#derive>'([literal(!, type('<http://www.w3.org/2001/XMLSchema#string>'))], true), !) :-
!.
conjify('<http://www.w3.org/2000/10/swap/log#herbrand>'([literal(!, type('<http://www.w3.org/2001/XMLSchema#string>'))], true), !) :-
conjify('<http://www.w3.org/2000/10/swap/log#herbrandInterpretation>'([literal(!, type('<http://www.w3.org/2001/XMLSchema#string>'))], true), !) :-
!.
conjify('<http://eulersharp.sourceforge.net/2003/03swap/prolog#cut>'([], true), !) :-
!.
Expand Down
Binary file modified eye.zip
Binary file not shown.
4 changes: 2 additions & 2 deletions reasoning/bi/biA.n3
Original file line number Diff line number Diff line change
Expand Up @@ -52,15 +52,15 @@
} a :PASS.
{
{
("atom_codes" "HOME" (72 79 77 69)) log:herbrand true.
("atom_codes" "HOME" (72 79 77 69)) log:herbrandInterpretation true.
} => {
:epac1 :result true.
}.
} a :PASS.
{
{
("date(1970, 1, 1, 0, 0, 0.0, 0, 'UTC', -)") e:compoundTerm "date(1970,1,1,0,0,0.0,0,'UTC',-)".
("date_time_stamp" "date(1970,1,1,0,0,0.0,0,'UTC',-)" 0.0) log:herbrand true.
("date_time_stamp" "date(1970,1,1,0,0,0.0,0,'UTC',-)" 0.0) log:herbrandInterpretation true.
0.0 math:equalTo 0.0.
} => {
:epdts1 :result true.
Expand Down
4 changes: 2 additions & 2 deletions reasoning/bi/biP.n3
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@
{?X log:equalTo 3. ("sqrt(_width^2+_length^2)" ?X 4) e:calculate ?R. ?R math:equalTo 5.0} => {:ec2 :result true}.
{("_period-250" "PT5M2S"^^xsd:dayTimeDuration) e:calculate ?R. ?R math:equalTo 52.0} => {:ec3 :result true}.
{((55 66 72 87 56 77 73 69 74 56) (1.66 1.78 1.87 1.92 1.66 1.89 1.86 1.79 1.80 1.66)) e:cov ?R. ?R math:equalTo 0.992777777777778} => {:eco1 :result true}.
{("atom_codes" "HOME" (72 79 77 69)) log:herbrand true} => {:epac1 :result true}.
{("date(1970, 1, 1, 0, 0, 0.0, 0, 'UTC', -)") e:compoundTerm ?U. ("date_time_stamp" ?U ?R) log:herbrand true. ?R math:equalTo 0.0} => {:epdts1 :result true}.
{("atom_codes" "HOME" (72 79 77 69)) log:herbrandInterpretation true} => {:epac1 :result true}.
{("date(1970, 1, 1, 0, 0, 0.0, 0, 'UTC', -)") e:compoundTerm ?U. ("date_time_stamp" ?U ?R) log:herbrandInterpretation true. ?R math:equalTo 0.0} => {:epdts1 :result true}.
{?SCOPE e:findall (?O {:s :p ?O} (:o1 :o2))} => {:ef1 :result true}.
{("This is a ~w with number ~w and with an escaped linefeed \n" "test" 5) e:format "This is a test with number 5 and with an escaped linefeed \n"} => {:ef4 :result true}.
{({:a :b :c. :d :e :f} true) e:graphDifference {:a :b :c. :d :e :f}} => {:egd1 :result true}.
Expand Down
26 changes: 13 additions & 13 deletions reasoning/d3-group/d3-group-proof.n3
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ skolem:lemma1 a r:Inference;
("identity" "rotation_120" "rotation_240" "reflection_a" "reflection_b" "reflection_c") :validGroup true.
};
r:evidence (
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrand true}]
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("identity" "rotation_120" "rotation_240" "reflection_a" "reflection_b" "reflection_c") :validGroup true}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ("identity" "rotation_120" "rotation_240" "reflection_a" "reflection_b" "reflection_c")];
Expand All @@ -49,7 +49,7 @@ skolem:lemma2 a r:Inference;
("identity" "rotation_120" "rotation_240" "reflection_a" "reflection_b") :validGroup true.
};
r:evidence (
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrand true}]
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("identity" "rotation_120" "rotation_240" "reflection_a" "reflection_b") :validGroup true}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ("identity" "rotation_120" "rotation_240" "reflection_a" "reflection_b")];
Expand All @@ -60,7 +60,7 @@ skolem:lemma3 a r:Inference;
("identity" "rotation_120" "rotation_240" "reflection_a" "reflection_c") :validGroup true.
};
r:evidence (
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrand true}]
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("identity" "rotation_120" "rotation_240" "reflection_a" "reflection_c") :validGroup true}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ("identity" "rotation_120" "rotation_240" "reflection_a" "reflection_c")];
Expand All @@ -71,7 +71,7 @@ skolem:lemma4 a r:Inference;
("identity" "rotation_120" "rotation_240" "reflection_a") :validGroup true.
};
r:evidence (
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrand true}]
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("identity" "rotation_120" "rotation_240" "reflection_a") :validGroup true}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ("identity" "rotation_120" "rotation_240" "reflection_a")];
Expand All @@ -82,7 +82,7 @@ skolem:lemma5 a r:Inference;
("identity" "rotation_120" "rotation_240" "reflection_b" "reflection_c") :validGroup true.
};
r:evidence (
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrand true}]
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("identity" "rotation_120" "rotation_240" "reflection_b" "reflection_c") :validGroup true}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ("identity" "rotation_120" "rotation_240" "reflection_b" "reflection_c")];
Expand All @@ -93,7 +93,7 @@ skolem:lemma6 a r:Inference;
("identity" "rotation_120" "rotation_240" "reflection_b") :validGroup true.
};
r:evidence (
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrand true}]
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("identity" "rotation_120" "rotation_240" "reflection_b") :validGroup true}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ("identity" "rotation_120" "rotation_240" "reflection_b")];
Expand All @@ -104,7 +104,7 @@ skolem:lemma7 a r:Inference;
("identity" "rotation_120" "rotation_240" "reflection_c") :validGroup true.
};
r:evidence (
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrand true}]
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("identity" "rotation_120" "rotation_240" "reflection_c") :validGroup true}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ("identity" "rotation_120" "rotation_240" "reflection_c")];
Expand All @@ -115,7 +115,7 @@ skolem:lemma8 a r:Inference;
("identity" "rotation_120" "rotation_240") :validGroup true.
};
r:evidence (
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrand true}]
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("identity" "rotation_120" "rotation_240") :validGroup true}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ("identity" "rotation_120" "rotation_240")];
Expand All @@ -126,7 +126,7 @@ skolem:lemma9 a r:Inference;
("identity" "reflection_a") :validGroup true.
};
r:evidence (
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrand true}]
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("identity" "reflection_a") :validGroup true}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ("identity" "reflection_a")];
Expand All @@ -137,7 +137,7 @@ skolem:lemma10 a r:Inference;
("identity" "reflection_b") :validGroup true.
};
r:evidence (
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrand true}]
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("identity" "reflection_b") :validGroup true}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ("identity" "reflection_b")];
Expand All @@ -148,7 +148,7 @@ skolem:lemma11 a r:Inference;
("identity" "reflection_c") :validGroup true.
};
r:evidence (
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrand true}]
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("identity" "reflection_c") :validGroup true}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ("identity" "reflection_c")];
Expand All @@ -159,7 +159,7 @@ skolem:lemma12 a r:Inference;
("identity") :validGroup true.
};
r:evidence (
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrand true}]
[ a r:Fact; r:gives {("consult" "./d3-group.pl") log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("identity") :validGroup true}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ("identity")];
Expand All @@ -168,7 +168,7 @@ skolem:lemma12 a r:Inference;
skolem:lemma13 a r:Extraction;
r:gives {
@forAll var:x_0. {
("consult" "./d3-group.pl") log:herbrand true.
("consult" "./d3-group.pl") log:herbrandInterpretation true.
var:x_0 :validGroup true.
} => {
var:x_0 :validGroup true.
Expand Down
2 changes: 1 addition & 1 deletion reasoning/d3-group/d3-group-query.n3
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
@prefix : <https://eyereasoner.github.io/ns#>.

{
("consult" "./d3-group.pl") log:herbrand true.
("consult" "./d3-group.pl") log:herbrandInterpretation true.
?Group :validGroup true.
} => {
?Group :validGroup true.
Expand Down
36 changes: 18 additions & 18 deletions reasoning/dining-philosophers/dp.n3
Original file line number Diff line number Diff line change
Expand Up @@ -9,36 +9,36 @@

{?P :pickup true} <= {
?P :chopstick (?L ?R).
("mutex_lock" ?L) log:herbrand true.
("mutex_lock" ?R) log:herbrand true.
("mutex_lock" ?L) log:herbrandInterpretation true.
("mutex_lock" ?R) log:herbrandInterpretation true.
}.

{?P :putdown true} <= {
?P :chopstick (?L ?R).
("mutex_unlock" ?R) log:herbrand true.
("mutex_unlock" ?L) log:herbrand true.
("mutex_unlock" ?R) log:herbrandInterpretation true.
("mutex_unlock" ?L) log:herbrandInterpretation true.
}.

{?P :run (?T ?S)} <= {
("sleep" ?T) log:herbrand true.
#("format" "# ~w thinking for ~w seconds~n" (?P ?T)) log:herbrand true.
("sleep" ?T) log:herbrandInterpretation true.
#("format" "# ~w thinking for ~w seconds~n" (?P ?T)) log:herbrandInterpretation true.
?P :pickup true.
("sleep" ?S) log:herbrand true.
#("format" "# ~w eating for ~w seconds~n" (?P ?S)) log:herbrand true.
("sleep" ?S) log:herbrandInterpretation true.
#("format" "# ~w eating for ~w seconds~n" (?P ?S)) log:herbrandInterpretation true.
?P :putdown true.
}.

{
("thread_create" {:person1 :run (0.100 0.100)} ?A ()) log:herbrand true.
("thread_create" {:person2 :run (0.200 0.200)} ?B ()) log:herbrand true.
("thread_create" {:person3 :run (0.300 0.300)} ?C ()) log:herbrand true.
("thread_create" {:person4 :run (0.250 0.200)} ?D ()) log:herbrand true.
("thread_create" {:person5 :run (0.025 0.100)} ?E ()) log:herbrand true.
("thread_join" ?A ?F) log:herbrand true.
("thread_join" ?B ?G) log:herbrand true.
("thread_join" ?C ?H) log:herbrand true.
("thread_join" ?D ?I) log:herbrand true.
("thread_join" ?E ?J) log:herbrand true.
("thread_create" {:person1 :run (0.100 0.100)} ?A ()) log:herbrandInterpretation true.
("thread_create" {:person2 :run (0.200 0.200)} ?B ()) log:herbrandInterpretation true.
("thread_create" {:person3 :run (0.300 0.300)} ?C ()) log:herbrandInterpretation true.
("thread_create" {:person4 :run (0.250 0.200)} ?D ()) log:herbrandInterpretation true.
("thread_create" {:person5 :run (0.025 0.100)} ?E ()) log:herbrandInterpretation true.
("thread_join" ?A ?F) log:herbrandInterpretation true.
("thread_join" ?B ?G) log:herbrandInterpretation true.
("thread_join" ?C ?H) log:herbrandInterpretation true.
("thread_join" ?D ?I) log:herbrandInterpretation true.
("thread_join" ?E ?J) log:herbrandInterpretation true.
} => {
:all :got :dinner.
}.
40 changes: 20 additions & 20 deletions reasoning/dining-philosophers/dpE.n3
Original file line number Diff line number Diff line change
Expand Up @@ -27,24 +27,24 @@ skolem:lemma2 a r:Inference;
r:evidence (
[ a r:Fact; r:gives {("thread_create" {
:person1 :run (0.1 0.1).
} skolem:t_0 ()) log:herbrand true}]
} skolem:t_0 ()) log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("thread_create" {
:person2 :run (0.2 0.2).
} skolem:t_1 ()) log:herbrand true}]
} skolem:t_1 ()) log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("thread_create" {
:person3 :run (0.3 0.3).
} skolem:t_2 ()) log:herbrand true}]
} skolem:t_2 ()) log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("thread_create" {
:person4 :run (0.25 0.2).
} skolem:t_3 ()) log:herbrand true}]
} skolem:t_3 ()) log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("thread_create" {
:person5 :run (0.025 0.1).
} skolem:t_4 ()) log:herbrand true}]
[ a r:Fact; r:gives {("thread_join" skolem:t_0 true) log:herbrand true}]
[ a r:Fact; r:gives {("thread_join" skolem:t_1 true) log:herbrand true}]
[ a r:Fact; r:gives {("thread_join" skolem:t_2 true) log:herbrand true}]
[ a r:Fact; r:gives {("thread_join" skolem:t_3 true) log:herbrand true}]
[ a r:Fact; r:gives {("thread_join" skolem:t_4 true) log:herbrand true}]
} skolem:t_4 ()) log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("thread_join" skolem:t_0 true) log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("thread_join" skolem:t_1 true) log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("thread_join" skolem:t_2 true) log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("thread_join" skolem:t_3 true) log:herbrandInterpretation true}]
[ a r:Fact; r:gives {("thread_join" skolem:t_4 true) log:herbrandInterpretation true}]
);
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo skolem:t_0];
r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo skolem:t_1];
Expand Down Expand Up @@ -73,24 +73,24 @@ skolem:lemma4 a r:Extraction;
@forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4, var:x_5, var:x_6, var:x_7, var:x_8, var:x_9. {
("thread_create" {
:person1 :run (0.1 0.1).
} var:x_0 ()) log:herbrand true.
} var:x_0 ()) log:herbrandInterpretation true.
("thread_create" {
:person2 :run (0.2 0.2).
} var:x_1 ()) log:herbrand true.
} var:x_1 ()) log:herbrandInterpretation true.
("thread_create" {
:person3 :run (0.3 0.3).
} var:x_2 ()) log:herbrand true.
} var:x_2 ()) log:herbrandInterpretation true.
("thread_create" {
:person4 :run (0.25 0.2).
} var:x_3 ()) log:herbrand true.
} var:x_3 ()) log:herbrandInterpretation true.
("thread_create" {
:person5 :run (0.025 0.1).
} var:x_4 ()) log:herbrand true.
("thread_join" var:x_0 var:x_5) log:herbrand true.
("thread_join" var:x_1 var:x_6) log:herbrand true.
("thread_join" var:x_2 var:x_7) log:herbrand true.
("thread_join" var:x_3 var:x_8) log:herbrand true.
("thread_join" var:x_4 var:x_9) log:herbrand true.
} var:x_4 ()) log:herbrandInterpretation true.
("thread_join" var:x_0 var:x_5) log:herbrandInterpretation true.
("thread_join" var:x_1 var:x_6) log:herbrandInterpretation true.
("thread_join" var:x_2 var:x_7) log:herbrandInterpretation true.
("thread_join" var:x_3 var:x_8) log:herbrandInterpretation true.
("thread_join" var:x_4 var:x_9) log:herbrandInterpretation true.
} => {
:all :got :dinner.
}.
Expand Down
Loading

0 comments on commit 2ee08b3

Please sign in to comment.