Skip to content

Commit

Permalink
testing s(urface) equ(ivalent) ent(ailment)s
Browse files Browse the repository at this point in the history
  • Loading branch information
josd committed Oct 15, 2023
1 parent 6943c77 commit c778684
Show file tree
Hide file tree
Showing 19 changed files with 26 additions and 21 deletions.
1 change: 1 addition & 0 deletions RELEASE
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
EYE release

v5.0.10 (2023-10-15) testing s(urface) equ(ivalent) ent(ailment)s
v5.0.9 (2023-10-15) Surface Equivalent Entailment - SEE
v5.0.8 (2023-10-15) checking surface equivalent entailment
v5.0.7 (2023-10-09) adding create sequent metarule for blogic
Expand Down
2 changes: 1 addition & 1 deletion VERSION
Original file line number Diff line number Diff line change
@@ -1 +1 @@
5.0.9
5.0.10
31 changes: 16 additions & 15 deletions eye.pl
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
:- use_module(library(pcre)).
:- catch(use_module(library(http/http_open)), _, true).

version_info('EYE v5.0.9 (2023-10-15)').
version_info('EYE v5.0.10 (2023-10-15)').

license_info('MIT License

Expand Down Expand Up @@ -627,10 +627,11 @@
).

%
% Surface Equivalent Entailment - SEE
% Sequents
% See https://en.wikipedia.org/wiki/Sequent
%

see :-
sequents :-
% resolution
assertz(implies((
implies(A, set(B), _),
Expand Down Expand Up @@ -778,7 +779,7 @@
findvars(S, W, beta),
makevars(S, I, beta(W))
), '<http://www.w3.org/2000/10/swap/log#implies>'(Q, I), '<>')),
% create see
% create sequent
assertz(implies((
'<http://www.w3.org/2000/10/swap/log#onNegativeSurface>'(V, G),
is_list(V),
Expand Down Expand Up @@ -1486,11 +1487,11 @@
-> nb_setval(current_scope, Scope)
; true
),
( \+flag(see),
( \+flag(sequents),
\+flag(blogic),
Rt = '<http://www.w3.org/2000/10/swap/log#implies>'(_, set(_))
-> assertz(flag(see)),
see
-> assertz(flag(sequents)),
sequents
; true
),
( functor(Rt, F, _),
Expand Down Expand Up @@ -1935,11 +1936,11 @@
tr_n3p(Z, Src, query).
tr_n3p(['\'<http://www.w3.org/2000/10/swap/log#implies>\''(X, Y)|Z], Src, Mode) :-
!,
( \+flag(see),
( \+flag(sequents),
\+flag(blogic),
Y = set(_)
-> assertz(flag(see)),
see
-> assertz(flag(sequents)),
sequents
; true
),
( flag(tactic, 'linear-select')
Expand Down Expand Up @@ -5179,7 +5180,7 @@
; djiti_assertz(Dn),
( flag('pass-only-new'),
Dn \= answer(_, _, _),
\+ (flag(see), Dn = '<http://www.w3.org/2000/10/swap/log#implies>'(_, _)),
\+ (flag(sequents), Dn = '<http://www.w3.org/2000/10/swap/log#implies>'(_, _)),
\+ (flag(blogic), Dn = '<http://www.w3.org/2000/10/swap/log#implies>'(_, _)),
\+pass_only_new(Dn)
-> assertz(pass_only_new(Dn))
Expand Down Expand Up @@ -5217,7 +5218,7 @@
; djiti_assertz(Cn),
( flag('pass-only-new'),
Cn \= answer(_, _, _),
\+ (flag(see), Cn = '<http://www.w3.org/2000/10/swap/log#implies>'(_, _)),
\+ (flag(sequents), Cn = '<http://www.w3.org/2000/10/swap/log#implies>'(_, _)),
\+ (flag(blogic), Cn = '<http://www.w3.org/2000/10/swap/log#implies>'(_, _)),
\+pass_only_new(Cn)
-> assertz(pass_only_new(Cn))
Expand Down Expand Up @@ -5338,11 +5339,11 @@
!.
djiti_fact('<http://www.w3.org/2000/10/swap/log#implies>'(A, B), C) :-
nonvar(B),
( \+flag(see),
( \+flag(sequents),
\+flag(blogic),
B = set(_)
-> assertz(flag(see)),
see
-> assertz(flag(sequents)),
sequents
; true
),
( conj_list(B, D)
Expand Down
Binary file modified eye.zip
Binary file not shown.
2 changes: 1 addition & 1 deletion reasoning/blogic/version.n3s.out
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
@prefix log: <http://www.w3.org/2000/10/swap/log#>.

() log:version "EYE v5.0.9 (2023-10-15)".
() log:version "EYE v5.0.10 (2023-10-15)".
11 changes: 7 additions & 4 deletions reasoning/see/README → reasoning/sequents/README
Original file line number Diff line number Diff line change
@@ -1,8 +1,11 @@
-----------------------------------
Surface Equivalent Entailment - SEE
-----------------------------------
--------
Sequents
--------

Supporting log:implies with a set of possible conclusions e.g.
See https://en.wikipedia.org/wiki/Sequent
Aka s(urface) equ(ivalent) ent(ailment)s

A sequent is a log:implies with a set of possible conclusions e.g.

# all cars are green or blue
{
Expand Down
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.

0 comments on commit c778684

Please sign in to comment.