diff --git a/RELEASE b/RELEASE index 9be160105..81afbb505 100644 --- a/RELEASE +++ b/RELEASE @@ -1,5 +1,6 @@ EYE release +v10.30.7 (2024-11-26) changing --proof-explanation to --ether (explain the reasoning) v10.30.6 (2024-11-25) adding --proof-explanation command line switch to output proof explanation using log:proves v10.30.5 (2024-11-22) experimental (functor; args) compound terms v10.30.4 (2024-11-19) simplify negative answer surfaces diff --git a/VERSION b/VERSION index 4fd39801a..a8207bfd2 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -10.30.6 +10.30.7 diff --git a/eye.pl b/eye.pl index 9f558d4c2..750283765 100644 --- a/eye.pl +++ b/eye.pl @@ -22,7 +22,7 @@ :- catch(use_module(library(process)), _, true). :- catch(use_module(library(http/http_open)), _, true). -version_info('EYE v10.30.6 (2024-11-25)'). +version_info('EYE v10.30.7 (2024-11-26)'). license_info('MIT License @@ -56,6 +56,7 @@ --debug-djiti output debug info about DJITI on stderr --debug-implies output debug info about implies on stderr --debug-pvm output debug info about PVM code on stderr + --ether explain the reasoning using log:proves --help show help info --hmac-key HMAC key used in e:hmac-sha built-in --ignore-inference-fuse do not halt in case of inference fuse @@ -72,7 +73,6 @@ --nope no proof explanation --output write reasoner output to --profile output profile info on stderr - --proof-explanation output proof explanation using log:proves --quantify quantify uris with in the output --quiet quiet mode --random-seed create random seed for e:random built-in @@ -424,7 +424,7 @@ ; true ), ( flag(intermediate, Out) - -> format(Out, 'flag(\'quantify\', \'~w\').~n', [Sns]) + -> format(Out, 'flag(quantify, \'~w\').~n', [Sns]) ; true ), args(Args), @@ -646,6 +646,13 @@ retractall(flag('debug-pvm')), assertz(flag('debug-pvm')), opts(Argus, Args). +opts(['--ether'|Argus], Args) :- + !, + retractall(flag(nope)), + assertz(flag(nope)), + retractall(flag(ether)), + assertz(flag(ether)), + opts(Argus, Args). opts(['--help'|_], _) :- \+flag(image, _), \+flag('debug-pvm'), @@ -669,11 +676,6 @@ retractall(flag(image, _)), assertz(flag(image, File)), opts(Argus, Args). -opts(['--legacy'|Argus], Args) :- - !, - retractall(flag(legacy)), - assertz(flag(legacy)), - opts(Argus, Args). opts(['--license'|_], _) :- !, license_info(License), @@ -695,9 +697,6 @@ retractall(flag('max-inferences', _)), assertz(flag('max-inferences', Limit)), opts(Argus, Args). -opts(['--no-bnode-relabeling'|Argus], Args) :- - !, - opts(Argus, Args). opts(['--no-distinct-input'|Argus], Args) :- !, retractall(flag('no-distinct-input')), @@ -766,16 +765,9 @@ retractall(flag(profile)), assertz(flag(profile)), opts(Argus, Args). -opts(['--proof-explanation'|Argus], Args) :- - !, - retractall(flag(nope)), - assertz(flag(nope)), - retractall(flag('proof-explanation')), - assertz(flag('proof-explanation')), - opts(Argus, Args). opts(['--quantify', Prefix|Argus], Args) :- !, - assertz(flag('quantify', Prefix)), + assertz(flag(quantify, Prefix)), opts(Argus, Args). opts(['--quiet'|Argus], Args) :- !, @@ -792,6 +784,11 @@ retractall(flag('rdf-list-output')), assertz(flag('rdf-list-output')), opts(Argus, Args). +opts(['--rdf-trig-output'|Argus], Args) :- + !, + retractall(flag('rdf-trig-output')), + assertz(flag('rdf-trig-output')), + opts(Argus, Args). opts(['--restricted'|Argus], Args) :- !, retractall(flag(restricted)), @@ -840,11 +837,6 @@ opts(['--tactic', Tactic|_], _) :- !, throw(not_supported_tactic(Tactic)). -opts(['--rdf-trig-output'|Argus], Args) :- - !, - retractall(flag('rdf-trig-output')), - assertz(flag('rdf-trig-output')), - opts(Argus, Args). opts(['--version'|_], _) :- !, throw(halt(0)). @@ -860,7 +852,7 @@ assertz(wcache(Arg, File)), opts(Argus, Args). opts([Arg|_], _) :- - \+memberchk(Arg, ['--entail', '--help', '--n3', '--n3p', '--not-entail', '--pass', '--pass-all', '--proof', '--query', '--trig', '--turtle']), + \+memberchk(Arg, ['--entail', '--help', '--n3', '--n3p', '--no-bnode-relabeling', '--not-entail', '--pass', '--pass-all', '--proof', '--query', '--trig', '--turtle']), sub_atom(Arg, 0, 2, _, '--'), !, throw(not_supported_option(Arg)). @@ -3658,7 +3650,7 @@ ( answer('', _, _) -> nl, writeln('#'), - writeln('# Proof Explanation'), + writeln('# Explain the reasoning'), writeln('#'), ( answer('', S, O), labelvars(''(S, O), 0, _, avar), @@ -4089,7 +4081,7 @@ ) ; ( \+flag('no-qvars') -> true - ; flag('quantify', Prefix), + ; flag(quantify, Prefix), sub_atom(X, 1, _, _, Prefix) ), write('_:') @@ -4104,14 +4096,14 @@ ), !. wt0(X) :- - flag('quantify', Prefix), + flag(quantify, Prefix), flag(nope), atom(X), sub_atom(X, 1, _, _, Prefix), !, ( getlist(X, M) -> wt(M) - ; ''(Y, ['quantify', Prefix, X]), + ; ''(Y, [quantify, Prefix, X]), wt0(Y) ). wt0(X) :- @@ -4913,10 +4905,10 @@ write(B). wcf(A, _) :- atom(A), - flag('quantify', Prefix), + flag(quantify, Prefix), sub_atom(A, 1, _, _, Prefix), !, - ''(B, ['quantify', Prefix, A]), + ''(B, [quantify, Prefix, A]), wt0(B). wcf(A, B) :- atom(A), @@ -4988,7 +4980,7 @@ ignore(Prem = true), ( flag(nope), \+flag('rule-histogram'), - \+flag('proof-explanation') + \+flag(ether) -> true ; copy_term_nat(''(Prem, Conc), Rule) ), @@ -5088,7 +5080,7 @@ conj_list(Concs, Ls), conj_list(Conce, Le), astep(Src, Prem, Concd, Conce, Rule), - ( flag('proof-explanation'), + ( flag(ether), Concd \=answer(_, _, _), Concd \= (answer(_, _, _), _) -> assertz(answer('', (Rule, Prem), Concd)) diff --git a/eye.zip b/eye.zip index d98efe025..a4b2d0b12 100644 Binary files a/eye.zip and b/eye.zip differ diff --git a/reasoning/ackermann/test b/reasoning/ackermann/test index fd1dc167c..bad785883 100755 --- a/reasoning/ackermann/test +++ b/reasoning/ackermann/test @@ -1,3 +1,3 @@ #!/bin/bash eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --nope https://eyereasoner.github.io/eye/reasoning/ackermann/ackermann.n3 --query https://eyereasoner.github.io/eye/reasoning/ackermann/ackermann-query.n3 --output ackermann-answer.n3 -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --proof-explanation https://eyereasoner.github.io/eye/reasoning/ackermann/ackermann.n3 --query https://eyereasoner.github.io/eye/reasoning/ackermann/ackermann-query.n3 --output ackermann-proof.n3 +eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --ether https://eyereasoner.github.io/eye/reasoning/ackermann/ackermann.n3 --query https://eyereasoner.github.io/eye/reasoning/ackermann/ackermann-query.n3 --output ackermann-proof.n3 diff --git a/reasoning/workplace-benchmark/test b/reasoning/workplace-benchmark/test index cba530be7..a37940b9c 100755 --- a/reasoning/workplace-benchmark/test +++ b/reasoning/workplace-benchmark/test @@ -1,3 +1,3 @@ #!/bin/bash eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --nope https://eyereasoner.github.io/eye/reasoning/workplace-benchmark/workplace.n3 --turtle https://eyereasoner.github.io/eye/reasoning/workplace-benchmark/workplace-data.ttl --query https://eyereasoner.github.io/eye/reasoning/workplace-benchmark/workplace-query.n3 --output workplace-answer.n3 -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --proof-explanation https://eyereasoner.github.io/eye/reasoning/workplace-benchmark/workplace.n3 --turtle https://eyereasoner.github.io/eye/reasoning/workplace-benchmark/workplace-data.ttl --query https://eyereasoner.github.io/eye/reasoning/workplace-benchmark/workplace-query.n3 --output workplace-proof.n3 +eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --ether https://eyereasoner.github.io/eye/reasoning/workplace-benchmark/workplace.n3 --turtle https://eyereasoner.github.io/eye/reasoning/workplace-benchmark/workplace-data.ttl --query https://eyereasoner.github.io/eye/reasoning/workplace-benchmark/workplace-query.n3 --output workplace-proof.n3 diff --git a/reasoning/workplace-benchmark/workplace-proof.n3 b/reasoning/workplace-benchmark/workplace-proof.n3 index 69dac1f7a..31e1c7859 100644 --- a/reasoning/workplace-benchmark/workplace-proof.n3 +++ b/reasoning/workplace-benchmark/workplace-proof.n3 @@ -30004,7 +30004,7 @@ :carol10000 :complies false. # -# Proof Explanation +# Explain the reasoning # { diff --git a/reasoning/workplace/test b/reasoning/workplace/test index 1a2076730..b78e093d1 100755 --- a/reasoning/workplace/test +++ b/reasoning/workplace/test @@ -1,3 +1,3 @@ #!/bin/bash eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --nope https://eyereasoner.github.io/eye/reasoning/workplace/workplace.n3 --turtle https://eyereasoner.github.io/eye/reasoning/workplace/workplace-data.ttl --query https://eyereasoner.github.io/eye/reasoning/workplace/workplace-query.n3 --output workplace-answer.n3 -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --proof-explanation https://eyereasoner.github.io/eye/reasoning/workplace/workplace.n3 --turtle https://eyereasoner.github.io/eye/reasoning/workplace/workplace-data.ttl --query https://eyereasoner.github.io/eye/reasoning/workplace/workplace-query.n3 --output workplace-proof.n3 +eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. --ether https://eyereasoner.github.io/eye/reasoning/workplace/workplace.n3 --turtle https://eyereasoner.github.io/eye/reasoning/workplace/workplace-data.ttl --query https://eyereasoner.github.io/eye/reasoning/workplace/workplace-query.n3 --output workplace-proof.n3 diff --git a/reasoning/workplace/workplace-proof.n3 b/reasoning/workplace/workplace-proof.n3 index fd64f2241..444b05af0 100644 --- a/reasoning/workplace/workplace-proof.n3 +++ b/reasoning/workplace/workplace-proof.n3 @@ -7,7 +7,7 @@ :bob :complies false. # -# Proof Explanation +# Explain the reasoning # {