diff --git a/RELEASE b/RELEASE index d1cd2a378..b0eb1deb6 100644 --- a/RELEASE +++ b/RELEASE @@ -1,5 +1,6 @@ EYE release +v9.0.13 (2023-12-12) using lingua variables in the var: namespace v9.0.12 (2023-12-12) reverting lingua v9.0.11 (2023-12-11) for isomorphic rules use the rule with the least blank nodes v9.0.10 (2023-12-11) using lingua:varCount to make rules safe diff --git a/VERSION b/VERSION index 95f98aa67..ec9af0e71 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -9.0.12 +9.0.13 diff --git a/eye.pl b/eye.pl index c65742190..ac1e6487f 100644 --- a/eye.pl +++ b/eye.pl @@ -21,7 +21,7 @@ :- use_module(library(pcre)). :- catch(use_module(library(http/http_open)), _, true). -version_info('EYE v9.0.12 (2023-12-12)'). +version_info('EYE v9.0.13 (2023-12-12)'). license_info('MIT License @@ -645,34 +645,23 @@ ), % forward rule assertz(implies(( - ''(R, ''), - ''(R, U), - getlist(U, V), - ''(R, K), + ''(R, ''), + ''(R, K), getconj(K, A), - ''(R, H), + ''(R, H), getconj(H, B), - ( flag(explain), - B \= false - -> conj_append(B, remember(answer('', R, U)), D) - ; D = B - ), - makevars([A, D], [Q, I], beta(V)) + findvars([A, B], V, alpha), + makevars([A, B], [Q, I], beta(V)) ), ''(Q, I), '<>')), % backward rule assertz(implies(( - ''(R, ''), - ''(R, U), - getlist(U, V), - ''(R, K), + ''(R, ''), + ''(R, K), getconj(K, A), - ''(R, H), + ''(R, H), getconj(H, B), - ( flag(explain) - -> conj_append(A, remember(answer('', R, U)), D) - ; D = A - ), - makevars(':-'(B, D), C, beta(V)), + findvars([A, B], V, alpha), + makevars(':-'(B, A), C, beta(V)), copy_term_nat(C, CC), labelvars(CC, 0, _, avar), ( \+cc(CC) @@ -683,19 +672,14 @@ )), true, '<>')), % query rule assertz(implies(( - ''(R, ''), - ''(R, U), - getlist(U, V), - ''(R, K), + ''(R, ''), + ''(R, K), getconj(K, A), - ''(R, H), + ''(R, H), getconj(H, B), djiti_answer(answer(B), J), - ( flag(explain) - -> conj_append(A, remember(answer('', R, U)), D) - ; D = A - ), - makevars(implies(D, J, '<>'), C, beta(V)), + findvars([A, B], V, alpha), + makevars(implies(A, J, '<>'), C, beta(V)), copy_term_nat(C, CC), labelvars(CC, 0, _, avar), ( \+cc(CC) @@ -1504,7 +1488,7 @@ ttl_n3p(O, Object), Triple =.. [Predicate, Subject, Object], djiti_assertz(Triple), - ( Predicate = '', + ( Predicate = '', \+flag(lingua) -> assertz(flag(lingua)) ; true @@ -1566,7 +1550,7 @@ -> nb_setval(current_scope, Scope) ; true ), - ( Rt = ''(_, _), + ( Rt = ''(_, _), \+flag(lingua) -> assertz(flag(lingua)) ; true @@ -2628,7 +2612,7 @@ verb(Item, Triples1), { prolog_verb(Item, Verb), ( atomic(Verb), - Verb = '\'\'', + Verb = '\'\'', \+flag(lingua) -> assertz(flag(lingua)) ; true @@ -11105,7 +11089,7 @@ recursion(B) ), ( flag(lingua) - -> A = '' + -> A = '' ; nb_getval(scope, A) ). @@ -12076,7 +12060,8 @@ !, distinct(C, D), findvars(D, G, beta), - ( D \= G + ( flag(blogic), + D \= G -> throw(invalid_graffiti(D, in(A))) ; true ), diff --git a/eye.zip b/eye.zip index 1c9b2df7b..386a46337 100644 Binary files a/eye.zip and b/eye.zip differ diff --git a/reasoning/lingua/acp.ttl b/reasoning/lingua/acp.ttl index 1111e349a..b6b66593f 100644 --- a/reasoning/lingua/acp.ttl +++ b/reasoning/lingua/acp.ttl @@ -1,7 +1,8 @@ @prefix rdf: . @prefix list: . @prefix log: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . :test1 @@ -15,89 +16,65 @@ :noneOf :D. :acp_rule1 a lingua:BackwardRule; - lingua:vars ( - _:Pol - _:Test - _:Field - _:X - ); lingua:conclusion ( - _:Pol :pass :allOfTest + var:Pol :pass :allOfTest ); lingua:premise ( - _:Test :policy _:Pol - _:Pol rdf:type :Policy + var:Test :policy var:Pol + var:Pol rdf:type :Policy ( ( - _:Pol :allOf _:Field + var:Pol :allOf var:Field ) ( - _:Test :has _:Field + var:Test :has var:Field ) - ) log:forAllIn _:X + ) log:forAllIn var:X ). :acp_rule2 a lingua:BackwardRule; - lingua:vars ( - _:Pol - _:Test - _:Field - _:List - _:X - _:L - );lingua:conclusion ( - _:Pol :pass :anyOfTest + lingua:conclusion ( + var:Pol :pass :anyOfTest ); lingua:premise ( - _:Test :policy _:Pol - _:Pol rdf:type :Policy + var:Test :policy var:Pol + var:Pol rdf:type :Policy ( - _:Field + var:Field ( - _:Pol :anyOf _:Field - _:Test :has _:Field + var:Pol :anyOf var:Field + var:Test :has var:Field ) - _:List - ) log:collectAllIn _:X - _:List list:length _:L - _:L log:notEqualTo 0 + var:List + ) log:collectAllIn var:X + var:List list:length var:L + var:L log:notEqualTo 0 ). :acp_rule3 a lingua:BackwardRule; - lingua:vars ( - _:Pol - _:Test - _:Field - _:List - _:X - _:L - ); lingua:conclusion ( - _:Pol :pass :noneOfTest + var:Pol :pass :noneOfTest ); lingua:premise ( - _:Test :policy _:Pol - _:Pol rdf:type :Policy - (_:Field ( - _:Pol :noneOf _:Field - _:Test :has _:Field - ) _:List) log:collectAllIn _:X - _:List list:length _:L - _:L log:equalTo 0 + var:Test :policy var:Pol + var:Pol rdf:type :Policy + (var:Field ( + var:Pol :noneOf var:Field + var:Test :has var:Field + ) var:List) log:collectAllIn var:X + var:List list:length var:L + var:L log:equalTo 0 ). # query :acp_query a lingua:QueryRule; - lingua:vars ( - _:Pol - ); lingua:premise ( - _:Pol rdf:type :Policy - _:Pol :pass :allOfTest - _:Pol :pass :anyOfTest - _:Pol :pass :noneOfTest + var:Pol rdf:type :Policy + var:Pol :pass :allOfTest + var:Pol :pass :anyOfTest + var:Pol :pass :noneOfTest ); lingua:conclusion ( - :test :for _:Pol + :test :for var:Pol :test :is true ). diff --git a/reasoning/lingua/append.ttl b/reasoning/lingua/append.ttl index 0fd6c9ac6..7221b31cf 100644 --- a/reasoning/lingua/append.ttl +++ b/reasoning/lingua/append.ttl @@ -1,6 +1,7 @@ @prefix list: . @prefix log: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . :Let :param1 ( @@ -16,16 +17,11 @@ # query :append_query a lingua:QueryRule; - lingua:vars ( - _:X1 - _:X2 - _:Y - ); lingua:premise ( - :Let :param1 _:X1 - :Let :param2 _:X2 - (_:X1 _:X2) list:append _:Y + :Let :param1 var:X1 + :Let :param2 var:X2 + (var:X1 var:X2) list:append var:Y ); lingua:conclusion ( - (_:X1 _:X2) :append _:Y + (var:X1 var:X2) :append var:Y ). diff --git a/reasoning/lingua/backward.ttl b/reasoning/lingua/backward.ttl index c63fa0be5..acced66a2 100644 --- a/reasoning/lingua/backward.ttl +++ b/reasoning/lingua/backward.ttl @@ -1,24 +1,20 @@ @prefix math: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # see https://www.w3.org/2000/10/swap/doc/tutorial-1.pdf page 17 # something is more interesting if it is greater :backward_rule a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - ); lingua:conclusion ( - _:X :moreInterestingThan _:Y + var:X :moreInterestingThan var:Y ); lingua:premise ( - _:X math:greaterThan _:Y + var:X math:greaterThan var:Y ). # query :backward_query a lingua:QueryRule; - lingua:vars (); lingua:premise ( 5 :moreInterestingThan 3 ); diff --git a/reasoning/lingua/complex.ttl b/reasoning/lingua/complex.ttl index b4e7faede..0393c89d8 100644 --- a/reasoning/lingua/complex.ttl +++ b/reasoning/lingua/complex.ttl @@ -1,269 +1,158 @@ @prefix math: . @prefix complex: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # exponentiation :complex_numbers_exponentiation_rule a lingua:BackwardRule; - lingua:vars ( - _:A - _:B - _:C - _:D - _:E - _:F - _:R - _:T - _:Z1 - _:Z2 - _:Z3 - _:Z4 - _:Z5 - _:Z6 - _:Z7 - _:Z8 - _:Z9 - _:Z10 - ); lingua:conclusion ( - ((_:A _:B) (_:C _:D)) complex:exponentiation (_:E _:F) + ((var:A var:B) (var:C var:D)) complex:exponentiation (var:E var:F) ); lingua:premise ( - (_:A _:B) complex:polar (_:R _:T) - (_:R _:C) math:exponentiation _:Z1 - _:D math:negation _:Z2 - (_:Z2 _:T) math:product _:Z3 - (2.718281828459045 _:Z3) math:exponentiation _:Z4 - (2.718281828459045 _:Z5) math:exponentiation _:R - (_:D _:Z5) math:product _:Z6 - (_:C _:T) math:product _:Z7 - (_:Z6 _:Z7) math:sum _:Z8 - _:Z8 math:cos _:Z9 - (_:Z1 _:Z4 _:Z9) math:product _:E - _:Z8 math:sin _:Z10 - (_:Z1 _:Z4 _:Z10) math:product _:F + (var:A var:B) complex:polar (var:R var:T) + (var:R var:C) math:exponentiation var:Z1 + var:D math:negation var:Z2 + (var:Z2 var:T) math:product var:Z3 + (2.718281828459045 var:Z3) math:exponentiation var:Z4 + (2.718281828459045 var:Z5) math:exponentiation var:R + (var:D var:Z5) math:product var:Z6 + (var:C var:T) math:product var:Z7 + (var:Z6 var:Z7) math:sum var:Z8 + var:Z8 math:cos var:Z9 + (var:Z1 var:Z4 var:Z9) math:product var:E + var:Z8 math:sin var:Z10 + (var:Z1 var:Z4 var:Z10) math:product var:F ). # asin :complex_numbers_asin_rule a lingua:BackwardRule; - lingua:vars ( - _:A - _:B - _:C - _:D - _:E - _:F - _:Z1 - _:Z2 - _:Z3 - _:Z4 - _:Z5 - _:Z6 - _:Z7 - _:Z8 - _:Z9 - _:Z10 - _:Z11 - _:Z12 - _:Z13 - _:Z14 - _:Z15 - ); lingua:conclusion ( - (_:A _:B) complex:asin (_:C _:D) + (var:A var:B) complex:asin (var:C var:D) ); lingua:premise ( - (1 _:A) math:sum _:Z1 - (_:Z1 2) math:exponentiation _:Z2 - (_:B 2) math:exponentiation _:Z3 - (_:Z2 _:Z3) math:sum _:Z4 - (_:Z4 0.5) math:exponentiation _:Z5 - (1 _:A) math:difference _:Z6 - (_:Z6 2) math:exponentiation _:Z7 - (_:Z7 _:Z3) math:sum _:Z8 - (_:Z8 0.5) math:exponentiation _:Z9 - (_:Z5 _:Z9) math:difference _:Z10 - (_:Z10 2) math:quotient _:E - (_:Z5 _:Z9) math:sum _:Z11 - (_:Z11 2) math:quotient _:F - _:E math:asin _:C - (_:F 2) math:exponentiation _:Z12 - (_:Z12 1) math:difference _:Z13 - (_:Z13 0.5) math:exponentiation _:Z14 - (_:F _:Z14) math:sum _:Z15 - (2.718281828459045 _:D) math:exponentiation _:Z15 + (1 var:A) math:sum var:Z1 + (var:Z1 2) math:exponentiation var:Z2 + (var:B 2) math:exponentiation var:Z3 + (var:Z2 var:Z3) math:sum var:Z4 + (var:Z4 0.5) math:exponentiation var:Z5 + (1 var:A) math:difference var:Z6 + (var:Z6 2) math:exponentiation var:Z7 + (var:Z7 var:Z3) math:sum var:Z8 + (var:Z8 0.5) math:exponentiation var:Z9 + (var:Z5 var:Z9) math:difference var:Z10 + (var:Z10 2) math:quotient var:E + (var:Z5 var:Z9) math:sum var:Z11 + (var:Z11 2) math:quotient var:F + var:E math:asin var:C + (var:F 2) math:exponentiation var:Z12 + (var:Z12 1) math:difference var:Z13 + (var:Z13 0.5) math:exponentiation var:Z14 + (var:F var:Z14) math:sum var:Z15 + (2.718281828459045 var:D) math:exponentiation var:Z15 ). # acos :complex_numbers_acos_rule a lingua:BackwardRule; - lingua:vars ( - _:A - _:B - _:C - _:D - _:E - _:F - _:Z1 - _:Z2 - _:Z3 - _:Z4 - _:Z5 - _:Z6 - _:Z7 - _:Z8 - _:Z9 - _:Z10 - _:Z11 - _:Z12 - _:Z13 - _:Z14 - _:Z15 - _:U - ); lingua:conclusion ( - (_:A _:B) complex:acos (_:C _:D) + (var:A var:B) complex:acos (var:C var:D) ); lingua:premise ( - (1 _:A) math:sum _:Z1 - (_:Z1 2) math:exponentiation _:Z2 - (_:B 2) math:exponentiation _:Z3 - (_:Z2 _:Z3) math:sum _:Z4 - (_:Z4 0.5) math:exponentiation _:Z5 - (1 _:A) math:difference _:Z6 - (_:Z6 2) math:exponentiation _:Z7 - (_:Z7 _:Z3) math:sum _:Z8 - (_:Z8 0.5) math:exponentiation _:Z9 - (_:Z5 _:Z9) math:difference _:Z10 - (_:Z10 2) math:quotient _:E - (_:Z5 _:Z9) math:sum _:Z11 - (_:Z11 2) math:quotient _:F - _:E math:acos _:C - (_:F 2) math:exponentiation _:Z12 - (_:Z12 1) math:difference _:Z13 - (_:Z13 0.5) math:exponentiation _:Z14 - (_:F _:Z14) math:sum _:Z15 - (2.718281828459045 _:U) math:exponentiation _:Z15 - _:U math:negation _:D + (1 var:A) math:sum var:Z1 + (var:Z1 2) math:exponentiation var:Z2 + (var:B 2) math:exponentiation var:Z3 + (var:Z2 var:Z3) math:sum var:Z4 + (var:Z4 0.5) math:exponentiation var:Z5 + (1 var:A) math:difference var:Z6 + (var:Z6 2) math:exponentiation var:Z7 + (var:Z7 var:Z3) math:sum var:Z8 + (var:Z8 0.5) math:exponentiation var:Z9 + (var:Z5 var:Z9) math:difference var:Z10 + (var:Z10 2) math:quotient var:E + (var:Z5 var:Z9) math:sum var:Z11 + (var:Z11 2) math:quotient var:F + var:E math:acos var:C + (var:F 2) math:exponentiation var:Z12 + (var:Z12 1) math:difference var:Z13 + (var:Z13 0.5) math:exponentiation var:Z14 + (var:F var:Z14) math:sum var:Z15 + (2.718281828459045 var:U) math:exponentiation var:Z15 + var:U math:negation var:D ). # polar :complex_numbers_polar_rule a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - _:R - _:Tp - _:Z1 - _:Z2 - _:Z3 - _:Z4 - _:Z5 - _:T - ); lingua:conclusion ( - (_:X _:Y) complex:polar(_:R _:Tp) + (var:X var:Y) complex:polar(var:R var:Tp) ); lingua:premise ( - (_:X 2) math:exponentiation _:Z1 - (_:Y 2) math:exponentiation _:Z2 - (_:Z1 _:Z2) math:sum _:Z3 - (_:Z3 0.5) math:exponentiation _:R - _:X math:absoluteValue _:Z4 - (_:Z4 _:R) math:quotient _:Z5 - _:Z5 math:acos _:T - (_:X _:Y _:T) complex:dial _:Tp + (var:X 2) math:exponentiation var:Z1 + (var:Y 2) math:exponentiation var:Z2 + (var:Z1 var:Z2) math:sum var:Z3 + (var:Z3 0.5) math:exponentiation var:R + var:X math:absoluteValue var:Z4 + (var:Z4 var:R) math:quotient var:Z5 + var:Z5 math:acos var:T + (var:X var:Y var:T) complex:dial var:Tp ). # dial :complex_numbers_dial_rule1 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - _:T - _:Tp - ); lingua:conclusion ( - (_:X _:Y _:T) complex:dial _:Tp + (var:X var:Y var:T) complex:dial var:Tp ); lingua:premise ( - _:X math:notLessThan 0 - _:Y math:notLessThan 0 - (0 _:T) math:sum _:Tp + var:X math:notLessThan 0 + var:Y math:notLessThan 0 + (0 var:T) math:sum var:Tp ). :complex_numbers_dial_rule2 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - _:T - _:Tp - ); lingua:conclusion ( - (_:X _:Y _:T) complex:dial _:Tp + (var:X var:Y var:T) complex:dial var:Tp ); lingua:premise ( - _:X math:lessThan 0 - _:Y math:notLessThan 0 - (3.141592653589793 _:T) math:difference _:Tp + var:X math:lessThan 0 + var:Y math:notLessThan 0 + (3.141592653589793 var:T) math:difference var:Tp ). :complex_numbers_dial_rule3 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - _:T - _:Tp - ); lingua:conclusion ( - (_:X _:Y _:T) complex:dial _:Tp + (var:X var:Y var:T) complex:dial var:Tp ); lingua:premise ( - _:X math:lessThan 0 - _:Y math:lessThan 0 - (3.141592653589793 _:T) math:sum _:Tp + var:X math:lessThan 0 + var:Y math:lessThan 0 + (3.141592653589793 var:T) math:sum var:Tp ). :complex_numbers_dial_rule4 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - _:T - _:Tp - _:Z1 - ); lingua:conclusion ( - (_:X _:Y _:T) complex:dial _:Tp + (var:X var:Y var:T) complex:dial var:Tp ); lingua:premise ( - _:X math:notLessThan 0 - _:Y math:lessThan 0 - (3.141592653589793 2) math:product _:Z1 - (_:Z1 _:T) math:difference _:Tp + var:X math:notLessThan 0 + var:Y math:lessThan 0 + (3.141592653589793 2) math:product var:Z1 + (var:Z1 var:T) math:difference var:Tp ). # query :complex_numbers_query a lingua:QueryRule; - lingua:vars ( - _:C1 - _:C2 - _:C3 - _:C4 - _:C5 - _:C6 - ); lingua:premise ( - ((-1 0) (0.5 0)) complex:exponentiation _:C1 - ((2.718281828459045 0) (0 3.141592653589793)) complex:exponentiation _:C2 - ((0 1) (0 1)) complex:exponentiation _:C3 - ((2.718281828459045 0) (-1.57079632679 0)) complex:exponentiation _:C4 - (2 0) complex:asin _:C5 - (2 0) complex:acos _:C6 + ((-1 0) (0.5 0)) complex:exponentiation var:C1 + ((2.718281828459045 0) (0 3.141592653589793)) complex:exponentiation var:C2 + ((0 1) (0 1)) complex:exponentiation var:C3 + ((2.718281828459045 0) (-1.57079632679 0)) complex:exponentiation var:C4 + (2 0) complex:asin var:C5 + (2 0) complex:acos var:C6 ); lingua:conclusion ( - ((-1 0) (0.5 0)) complex:exponentiation _:C1 - ((2.718281828459045 0) (0 3.141592653589793)) complex:exponentiation _:C2 - ((0 1) (0 1)) complex:exponentiation _:C3 - ((2.718281828459045 0) (-1.57079632679 0)) complex:exponentiation _:C4 - (2 0) complex:asin _:C5 - (2 0) complex:acos _:C6 + ((-1 0) (0.5 0)) complex:exponentiation var:C1 + ((2.718281828459045 0) (0 3.141592653589793)) complex:exponentiation var:C2 + ((0 1) (0 1)) complex:exponentiation var:C3 + ((2.718281828459045 0) (-1.57079632679 0)) complex:exponentiation var:C4 + (2 0) complex:asin var:C5 + (2 0) complex:acos var:C6 ). diff --git a/reasoning/lingua/control.ttl b/reasoning/lingua/control.ttl index d2eda89d5..8955b4165 100644 --- a/reasoning/lingua/control.ttl +++ b/reasoning/lingua/control.ttl @@ -1,5 +1,6 @@ @prefix math: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # input @@ -22,97 +23,61 @@ # forward rules :control_rule1 a lingua:ForwardRule; - lingua:vars ( - _:M1 - _:D1 - _:C1 - _:C2 - _:C - ); lingua:premise ( - :input1 :measurement10 _:M1 + :input1 :measurement10 var:M1 :input2 :measurement2 true - :disturbance1 :measurement3 _:D1 - (_:M1 19.6) math:product _:C1 # proportial part - (10 _:C2) math:exponentiation _:D1 # compensation part - (_:C1 _:C2) math:difference _:C # simple feedforward control + :disturbance1 :measurement3 var:D1 + (var:M1 19.6) math:product var:C1 # proportial part + (10 var:C2) math:exponentiation var:D1 # compensation part + (var:C1 var:C2) math:difference var:C # simple feedforward control ); lingua:conclusion ( - :actuator1 :control1 _:C + :actuator1 :control1 var:C ). :control_rule2 a lingua:ForwardRule; - lingua:vars ( - _:M3 - _:P3 - _:M4 - _:T2 - _:E - _:D - _:C1 - _:N - _:C2 - _:C - ); lingua:premise ( - :input3 :measurement3 _:M3 - :state3 :observation3 _:P3 - :output2 :measurement4 _:M4 - :output2 :target2 _:T2 - (_:T2 _:M4) math:difference _:E # error - (_:P3 _:M4) math:difference _:D # differential error - (5.8 _:E) math:product _:C1 # proportial part - (7.3 _:E) math:quotient _:N # nonlinear factor - (_:N _:D) math:product _:C2 # nonlinear differential part - (_:C1 _:C2) math:sum _:C # PND feedback control + :input3 :measurement3 var:M3 + :state3 :observation3 var:P3 + :output2 :measurement4 var:M4 + :output2 :target2 var:T2 + (var:T2 var:M4) math:difference var:E # error + (var:P3 var:M4) math:difference var:D # differential error + (5.8 var:E) math:product var:C1 # proportial part + (7.3 var:E) math:quotient var:N # nonlinear factor + (var:N var:D) math:product var:C2 # nonlinear differential part + (var:C1 var:C2) math:sum var:C # PND feedback control ); lingua:conclusion ( - :actuator2 :control1 _:C + :actuator2 :control1 var:C ). # backward rules :control_rule3 a lingua:BackwardRule; - lingua:vars ( - _:I - _:M - _:M1 - _:M2 - _:M3 - _:M - ); lingua:conclusion ( - _:I :measurement10 _:M + var:I :measurement10 var:M ); lingua:premise ( - _:I :measurement1 (_:M1 _:M2) - _:M1 math:lessThan _:M2 - (_:M2 _:M1) math:difference _:M3 - (_:M3 0.5) math:exponentiation _:M + var:I :measurement1 (var:M1 var:M2) + var:M1 math:lessThan var:M2 + (var:M2 var:M1) math:difference var:M3 + (var:M3 0.5) math:exponentiation var:M ). :control_rule4 a lingua:BackwardRule; - lingua:vars ( - _:I - _:M1 - _:M2 - ); lingua:conclusion ( - _:I :measurement10 _:M1 + var:I :measurement10 var:M1 ); lingua:premise ( - _:I :measurement1 (_:M1 _:M2) - _:M1 math:notLessThan _:M2 + var:I :measurement1 (var:M1 var:M2) + var:M1 math:notLessThan var:M2 ). # query :control_query a lingua:QueryRule; - lingua:vars ( - _:O - _:C - ); lingua:premise ( - _:O :control1 _:C + var:O :control1 var:C ); lingua:conclusion ( - _:O :control1 _:C + var:O :control1 var:C ). diff --git a/reasoning/lingua/fibonacci.ttl b/reasoning/lingua/fibonacci.ttl index e70203e54..7b906a91c 100644 --- a/reasoning/lingua/fibonacci.ttl +++ b/reasoning/lingua/fibonacci.ttl @@ -1,79 +1,55 @@ @prefix math: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # backward rules :fibonacci_rule1 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - ); lingua:conclusion ( - _:X :fibonacci _:Y + var:X :fibonacci var:Y ); lingua:premise ( - (_:X 0 1) :fib _:Y + (var:X 0 1) :fib var:Y ). :fibonacci_rule2 a lingua:BackwardRule; - lingua:vars ( - _:A - _:B - ); lingua:conclusion ( - (0 _:A _:B) :fib _:A + (0 var:A var:B) :fib var:A ); lingua:premise (). :fibonacci_rule3 a lingua:BackwardRule; - lingua:vars ( - _:A - _:B - ); lingua:conclusion ( - (1 _:A _:B) :fib _:B + (1 var:A var:B) :fib var:B ); lingua:premise (). :fibonacci_rule4 a lingua:BackwardRule; - lingua:vars ( - _:X - _:A - _:B - _:Y - _:C - _:D - ); lingua:conclusion ( - (_:X _:A _:B) :fib _:Y + (var:X var:A var:B) :fib var:Y ); lingua:premise ( - _:X math:greaterThan 1 - (_:X 1) math:difference _:C - (_:A _:B) math:sum _:D - (_:C _:B _:D) :fib _:Y + var:X math:greaterThan 1 + (var:X 1) math:difference var:C + (var:A var:B) math:sum var:D + (var:C var:B var:D) :fib var:Y ). # query :fibonacci_query a lingua:QueryRule; - lingua:vars ( - _:F1 - _:F2 - _:F3 - _:F4 - _:F5 - ); lingua:premise ( - 0 :fibonacci _:F1 - 1 :fibonacci _:F2 - 6 :fibonacci _:F3 - 91 :fibonacci _:F4 - 283 :fibonacci _:F5 + 0 :fibonacci var:F1 + 1 :fibonacci var:F2 + 6 :fibonacci var:F3 + 91 :fibonacci var:F4 + 283 :fibonacci var:F5 + 3674 :fibonacci var:F6 ); lingua:conclusion ( - () :fibonacci (0 _:F1) - () :fibonacci (1 _:F2) - () :fibonacci (6 _:F3) - () :fibonacci (91 _:F4) - () :fibonacci (283 _:F5) + () :fibonacci (0 var:F1) + () :fibonacci (1 var:F2) + () :fibonacci (6 var:F3) + () :fibonacci (91 var:F4) + () :fibonacci (283 var:F5) + () :fibonacci (3674 var:F6) ). diff --git a/reasoning/lingua/forward.ttl b/reasoning/lingua/forward.ttl index 3881aff56..d1cda7722 100644 --- a/reasoning/lingua/forward.ttl +++ b/reasoning/lingua/forward.ttl @@ -1,5 +1,6 @@ @prefix rdf: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # facts @@ -7,24 +8,18 @@ # humans are mortal :forward_rule a lingua:ForwardRule; - lingua:vars ( - _:S - ); lingua:premise ( - _:S rdf:type :Human + var:S rdf:type :Human ); lingua:conclusion ( - _:S rdf:type :Mortal + var:S rdf:type :Mortal ). # query :forward_query a lingua:QueryRule; - lingua:vars ( - _:S - ); lingua:premise ( - _:S rdf:type :Mortal + var:S rdf:type :Mortal ); lingua:conclusion ( - _:S rdf:type :Mortal + var:S rdf:type :Mortal ). diff --git a/reasoning/lingua/gen.ttl b/reasoning/lingua/gen.ttl index c3b0534d9..391fc2337 100644 --- a/reasoning/lingua/gen.ttl +++ b/reasoning/lingua/gen.ttl @@ -1,35 +1,27 @@ @prefix rdf: . @prefix rdfs: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . :gen_rule a lingua:ForwardRule; - lingua:vars (); lingua:premise (); lingua:conclusion ( :Socrates rdf:type :Human :Human rdfs:subClassOf :Mortal :rdfs_subclass_rule rdf:type lingua:ForwardRule - :rdfs_subclass_rule lingua:vars ( - _:A - _:B - _:S - ) :rdfs_subclass_rule lingua:premise ( - _:A rdfs:subClassOf _:B - _:S rdf:type _:A + var:A rdfs:subClassOf var:B + var:S rdf:type var:A ) :rdfs_subclass_rule lingua:conclusion ( - _:S rdf:type _:B + var:S rdf:type var:B ) :socrates_query rdf:type lingua:QueryRule - :socrates_query lingua:vars ( - _:S - ) :socrates_query lingua:premise ( - _:S rdf:type :Mortal + var:S rdf:type :Mortal ) :socrates_query lingua:conclusion ( - _:S rdf:type :Mortal + var:S rdf:type :Mortal ) ). diff --git a/reasoning/lingua/gps.ttl b/reasoning/lingua/gps.ttl index 83328e731..249a94872 100644 --- a/reasoning/lingua/gps.ttl +++ b/reasoning/lingua/gps.ttl @@ -2,183 +2,94 @@ @prefix list: . @prefix log: . @prefix gps: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # find paths in the state space from initial state to goal state within limits :gps_rule1 a lingua:BackwardRule; - lingua:vars ( - _:Goal - _:Path - _:Duration - _:Cost - _:Belief - _:Comfort - _:MaxDuration - _:MaxCost - _:MinBelief - _:MinComfort - ); lingua:conclusion ( - () gps:findpath (_:Goal _:Path _:Duration _:Cost _:Belief _:Comfort - (_:MaxDuration _:MaxCost _:MinBelief _:MinComfort)) + () gps:findpath (var:Goal var:Path var:Duration var:Cost var:Belief var:Comfort + (var:MaxDuration var:MaxCost var:MinBelief var:MinComfort)) ); lingua:premise ( - () gps:findpaths (() _:Goal () 0.0 0.0 1.0 1.0 _:Path _:Duration _:Cost _:Belief _:Comfort - (_:MaxDuration _:MaxCost _:MinBelief _:MinComfort 1)) + () gps:findpaths (() var:Goal () 0.0 0.0 1.0 1.0 var:Path var:Duration var:Cost var:Belief var:Comfort + (var:MaxDuration var:MaxCost var:MinBelief var:MinComfort 1)) ). :gps_rule2 a lingua:BackwardRule; - lingua:vars ( - _:Goal - _:Path - _:Duration - _:Cost - _:Belief - _:Comfort - _:MaxDuration - _:MaxCost - _:MinBelief - _:MinComfort - _:MaxStagecount - ); lingua:conclusion ( - () gps:findpath (_:Goal _:Path _:Duration _:Cost _:Belief _:Comfort - (_:MaxDuration _:MaxCost _:MinBelief _:MinComfort _:MaxStagecount)) + () gps:findpath (var:Goal var:Path var:Duration var:Cost var:Belief var:Comfort + (var:MaxDuration var:MaxCost var:MinBelief var:MinComfort var:MaxStagecount)) ); lingua:premise ( - () gps:findpaths (() _:Goal () 0.0 0.0 1.0 1.0 _:Path _:Duration _:Cost _:Belief _:Comfort - (_:MaxDuration _:MaxCost _:MinBelief _:MinComfort _:MaxStagecount)) + () gps:findpaths (() var:Goal () 0.0 0.0 1.0 1.0 var:Path var:Duration var:Cost var:Belief var:Comfort + (var:MaxDuration var:MaxCost var:MinBelief var:MinComfort var:MaxStagecount)) ). :gps_rule3 a lingua:BackwardRule; - lingua:vars ( - _:Maps - _:Goal - _:Path - _:Duration - _:Cost - _:Belief - _:Comfort - _:MaxDuration - _:MaxCost - _:MinBelief - _:MinComfort - _:MaxStagecount - ); lingua:conclusion ( - () gps:findpaths (_:Maps _:Goal _:Path _:Duration _:Cost _:Belief _:Comfort _:Path _:Duration _:Cost _:Belief _:Comfort - (_:MaxDuration _:MaxCost _:MinBelief _:MinComfort _:MaxStagecount)) + () gps:findpaths (var:Maps var:Goal var:Path var:Duration var:Cost var:Belief var:Comfort var:Path var:Duration var:Cost var:Belief var:Comfort + (var:MaxDuration var:MaxCost var:MinBelief var:MinComfort var:MaxStagecount)) ); lingua:premise ( - _:Goal log:call true + var:Goal log:call true ). :gps_rule4 a lingua:BackwardRule; - lingua:vars ( - _:Maps_s - _:Goal - _:Path_s - _:Duration_s - _:Cost_s - _:Belief_s - _:Comfort_s - _:Path - _:Duration - _:Cost - _:Belief - _:Comfort - _:MaxDuration - _:MaxCost - _:MinBelief - _:MinComfort - _:MaxStagecount - _:Map - _:From - _:Transition - _:To - _:Action - _:Duration_n - _:Cost_n - _:Belief_n - _:Comfort_n - _:Maps_t - _:Stagecount - _:Duration_t - _:Cost_t - _:Belief_t - _:Comfort_t - _:Path_t - ); lingua:conclusion ( - () gps:findpaths (_:Maps_s _:Goal _:Path_s _:Duration_s _:Cost_s _:Belief_s _:Comfort_s _:Path _:Duration _:Cost _:Belief _:Comfort - (_:MaxDuration _:MaxCost _:MinBelief _:MinComfort _:MaxStagecount)) + () gps:findpaths (var:Maps_s var:Goal var:Path_s var:Duration_s var:Cost_s var:Belief_s var:Comfort_s var:Path var:Duration var:Cost var:Belief var:Comfort + (var:MaxDuration var:MaxCost var:MinBelief var:MinComfort var:MaxStagecount)) ); lingua:premise ( - _:Map gps:description (_:From _:Transition _:To _:Action _:Duration_n _:Cost_n _:Belief_n _:Comfort_n) - (_:Maps_s (_:Map)) list:append _:Maps_t - _:Maps_t gps:stagecount _:Stagecount - _:Stagecount math:notGreaterThan _:MaxStagecount - (_:Duration_s _:Duration_n) math:sum _:Duration_t - _:Duration_t math:notGreaterThan _:MaxDuration - (_:Cost_s _:Cost_n) math:sum _:Cost_t - _:Cost_t math:notGreaterThan _:MaxCost - (_:Belief_s _:Belief_n) math:product _:Belief_t - _:Belief_t math:notLessThan _:MinBelief - (_:Comfort_s _:Comfort_n) math:product _:Comfort_t - _:Comfort_t math:notLessThan _:MinComfort - (_:Path_s (_:Action)) list:append _:Path_t - _:From log:becomes _:To + var:Map gps:description (var:From var:Transition var:To var:Action var:Duration_n var:Cost_n var:Belief_n var:Comfort_n) + (var:Maps_s (var:Map)) list:append var:Maps_t + var:Maps_t gps:stagecount var:Stagecount + var:Stagecount math:notGreaterThan var:MaxStagecount + (var:Duration_s var:Duration_n) math:sum var:Duration_t + var:Duration_t math:notGreaterThan var:MaxDuration + (var:Cost_s var:Cost_n) math:sum var:Cost_t + var:Cost_t math:notGreaterThan var:MaxCost + (var:Belief_s var:Belief_n) math:product var:Belief_t + var:Belief_t math:notLessThan var:MinBelief + (var:Comfort_s var:Comfort_n) math:product var:Comfort_t + var:Comfort_t math:notLessThan var:MinComfort + (var:Path_s (var:Action)) list:append var:Path_t + var:From log:becomes var:To ( - () gps:findpaths (_:Maps_t _:Goal _:Path_t _:Duration_t _:Cost_t _:Belief_t _:Comfort_t _:Path _:Duration _:Cost _:Belief _:Comfort - (_:MaxDuration _:MaxCost _:MinBelief _:MinComfort _:MaxStagecount)) + () gps:findpaths (var:Maps_t var:Goal var:Path_t var:Duration_t var:Cost_t var:Belief_t var:Comfort_t var:Path var:Duration var:Cost var:Belief var:Comfort + (var:MaxDuration var:MaxCost var:MinBelief var:MinComfort var:MaxStagecount)) ) log:callWithCleanup ( - _:To log:becomes _:From + var:To log:becomes var:From ) ). # counting the number of stages (a stage is a sequence of steps in the same map) :gps_rule5 a lingua:BackwardRule; - lingua:vars (); lingua:conclusion ( () gps:stagecount 1 ); lingua:premise (). :gps_rule6 a lingua:BackwardRule; - lingua:vars ( - _:A - _:B - _:C - _:D - _:E - _:F - _:G - ); lingua:conclusion ( - _:A gps:stagecount _:B + var:A gps:stagecount var:B ); lingua:premise ( - _:A list:firstRest (_:C _:D) - _:D list:firstRest (_:E _:F) - _:C log:notEqualTo _:E - _:D gps:stagecount _:G - (_:G 1) math:sum _:B + var:A list:firstRest (var:C var:D) + var:D list:firstRest (var:E var:F) + var:C log:notEqualTo var:E + var:D gps:stagecount var:G + (var:G 1) math:sum var:B ). :gps_rule7 a lingua:BackwardRule; - lingua:vars ( - _:A - _:B - _:C - _:D - ); lingua:conclusion ( - _:A gps:stagecount _:B + var:A gps:stagecount var:B ); lingua:premise ( - _:A list:firstRest (_:C _:D) - _:D gps:stagecount _:B + var:A list:firstRest (var:C var:D) + var:D gps:stagecount var:B ). # current state as practical example @@ -186,66 +97,42 @@ # map of Belgium :gps_rule8 a lingua:BackwardRule; - lingua:vars ( - _:S - _:L - ); lingua:conclusion ( - :map-BE gps:description ((_:S :location :Gent) () (_:S :location :Brugge) :drive_gent_brugge 1500.0 0.006 0.96 0.99) + :map-BE gps:description ((var:S :location :Gent) () (var:S :location :Brugge) :drive_gent_brugge 1500.0 0.006 0.96 0.99) ); lingua:premise ( - _:S :location _:L + var:S :location var:L ). :gps_rule9 a lingua:BackwardRule; - lingua:vars ( - _:S - _:L - ); lingua:conclusion ( - :map-BE gps:description ((_:S :location :Gent) () (_:S :location :Kortrijk) :drive_gent_kortrijk 1600.0 0.007 0.96 0.99) + :map-BE gps:description ((var:S :location :Gent) () (var:S :location :Kortrijk) :drive_gent_kortrijk 1600.0 0.007 0.96 0.99) ); lingua:premise ( - _:S :location _:L + var:S :location var:L ). :gps_rule10 a lingua:BackwardRule; - lingua:vars ( - _:S - _:L - ); lingua:conclusion ( - :map-BE gps:description ((_:S :location :Kortrijk) () (_:S :location :Brugge) :drive_kortrijk_brugge 1600.0 0.007 0.96 0.99) + :map-BE gps:description ((var:S :location :Kortrijk) () (var:S :location :Brugge) :drive_kortrijk_brugge 1600.0 0.007 0.96 0.99) ); lingua:premise ( - _:S :location _:L + var:S :location var:L ). :gps_rule11 a lingua:BackwardRule; - lingua:vars ( - _:S - _:L - ); lingua:conclusion ( - :map-BE gps:description ((_:S :location :Brugge) () (_:S :location :Oostende) :drive_brugge_oostende 900.0 0.004 0.98 1.0) + :map-BE gps:description ((var:S :location :Brugge) () (var:S :location :Oostende) :drive_brugge_oostende 900.0 0.004 0.98 1.0) ); lingua:premise ( - _:S :location _:L + var:S :location var:L ). # query :gps_query a lingua:QueryRule; - lingua:vars ( - _:SUBJECT - _:PATH - _:DURATION - _:COST - _:BELIEF - _:COMFORT - ); lingua:premise ( - () gps:findpath ((_:SUBJECT :location :Oostende) _:PATH _:DURATION _:COST _:BELIEF _:COMFORT (5000.0 5.0 0.2 0.4 1)) + () gps:findpath ((var:SUBJECT :location :Oostende) var:PATH var:DURATION var:COST var:BELIEF var:COMFORT (5000.0 5.0 0.2 0.4 1)) ); lingua:conclusion ( - _:SUBJECT gps:path (_:PATH _:DURATION _:COST _:BELIEF _:COMFORT) + var:SUBJECT gps:path (var:PATH var:DURATION var:COST var:BELIEF var:COMFORT) ). diff --git a/reasoning/lingua/graph.ttl b/reasoning/lingua/graph.ttl index 1961e4cac..e3a2126d8 100644 --- a/reasoning/lingua/graph.ttl +++ b/reasoning/lingua/graph.ttl @@ -1,4 +1,5 @@ -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # French roads @@ -15,40 +16,28 @@ # oneway subproperty of path :graph_rule1 a lingua:ForwardRule; - lingua:vars ( - _:A - _:B - ); lingua:premise ( - _:A :oneway _:B + var:A :oneway var:B ); lingua:conclusion ( - _:A :path _:B + var:A :path var:B ). # path transitive property :graph_rule2 a lingua:ForwardRule; - lingua:vars ( - _:A - _:B - _:C - ); lingua:premise ( - _:A :path _:B - _:B :path _:C + var:A :path var:B + var:B :path var:C ); lingua:conclusion ( - _:A :path _:C + var:A :path var:C ). # query :graph_query a lingua:QueryRule; - lingua:vars ( - _:A - ); lingua:premise ( - _:A :path :nantes + var:A :path :nantes ); lingua:conclusion ( - _:A :path :nantes + var:A :path :nantes ). diff --git a/reasoning/lingua/hanoi.ttl b/reasoning/lingua/hanoi.ttl index 74897f22c..72966ed5a 100644 --- a/reasoning/lingua/hanoi.ttl +++ b/reasoning/lingua/hanoi.ttl @@ -1,50 +1,33 @@ @prefix math: . @prefix list: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . -# _:M is the sequence of moves to move _:N disks from _:X to _:Y using _:Z as intermediary +# var:M is the sequence of moves to move var:N disks from var:X to var:Y using var:Z as intermediary :hanoi_rule1 a lingua:BackwardRule; - lingua:vars ( - _:N - _:X - _:Y - _:Z - _:M - _:N1 - _:M1 - _:M2 - ); lingua:conclusion ( - (_:N _:X _:Y _:Z) :moves _:M + (var:N var:X var:Y var:Z) :moves var:M ); lingua:premise ( - _:N math:greaterThan 1 - (_:N 1) math:difference _:N1 - (_:N1 _:X _:Z _:Y) :moves _:M1 - (_:N1 _:Z _:Y _:X) :moves _:M2 - (_:M1 ((_:X _:Y)) _:M2) list:append _:M + var:N math:greaterThan 1 + (var:N 1) math:difference var:N1 + (var:N1 var:X var:Z var:Y) :moves var:M1 + (var:N1 var:Z var:Y var:X) :moves var:M2 + (var:M1 ((var:X var:Y)) var:M2) list:append var:M ). :hanoi_rule2 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - _:Z - ); lingua:conclusion ( - (1 _:X _:Y _:Z) :moves ((_:X _:Y)) + (1 var:X var:Y var:Z) :moves ((var:X var:Y)) ); lingua:premise (). # query :hanoi_query a lingua:QueryRule; - lingua:vars ( - _:M - ); lingua:premise ( - (7 :left :right :center) :moves _:M + (7 :left :right :center) :moves var:M ); lingua:conclusion ( - (7 :left :right :center) :moves _:M + (7 :left :right :center) :moves var:M ). diff --git a/reasoning/lingua/negation.ttl b/reasoning/lingua/negation.ttl index 9bf672ebf..44a69ffc9 100644 --- a/reasoning/lingua/negation.ttl +++ b/reasoning/lingua/negation.ttl @@ -1,70 +1,56 @@ -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # saying A means saying C :negation_predicates_rule1 a lingua:ForwardRule; - lingua:vars ( - _:S - ); lingua:premise ( - _:S :saying :A + var:S :saying :A ); lingua:conclusion ( - _:S :saying :C + var:S :saying :C ). :negation_predicates_rule2 a lingua:ForwardRule; - lingua:vars ( - _:S - ); lingua:premise ( - _:S :not_saying :C + var:S :not_saying :C ); lingua:conclusion ( - _:S :not_saying :A + var:S :not_saying :A ). # saying B means saying C :negation_predicates_rule3 a lingua:ForwardRule; - lingua:vars ( - _:S - ); lingua:premise ( - _:S :saying :B + var:S :saying :B ); lingua:conclusion ( - _:S :saying :C + var:S :saying :C ). :negation_predicates_rule4 a lingua:ForwardRule; lingua:premise ( - _:S :not_saying :C + var:S :not_saying :C ); lingua:conclusion ( - _:S :not_saying :B + var:S :not_saying :B ). # saying A or saying B :negation_predicates_rule5 a lingua:ForwardRule; - lingua:vars ( - _:S - ); lingua:premise ( - _:S :not_saying :A + var:S :not_saying :A ); lingua:conclusion ( - _:S :saying :B + var:S :saying :B ). :negation_predicates_rule6 a lingua:ForwardRule; - lingua:vars ( - _:S - ); lingua:premise ( - _:S :not_saying :B + var:S :not_saying :B ); lingua:conclusion ( - _:S :saying :A + var:S :saying :A ). # assuming the negation of the query so that @@ -73,7 +59,6 @@ # query :negation_predicates_query a lingua:QueryRule; - lingua:vars (); lingua:premise ( :alice :saying :C ); diff --git a/reasoning/lingua/notequal.ttl b/reasoning/lingua/notequal.ttl index eddc70e59..db8e1ef5b 100644 --- a/reasoning/lingua/notequal.ttl +++ b/reasoning/lingua/notequal.ttl @@ -1,6 +1,7 @@ @prefix graph: . @prefix log: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . :Let :param1 ( @@ -18,22 +19,14 @@ #query :union_query a lingua:QueryRule; - lingua:vars ( - _:X1 - _:X2 - _:X3 - _:Y - _:Y_RT - _:X3_RT - ); lingua:premise ( - :Let :param1 _:X1 - :Let :param2 _:X2 - :Let :param3 _:X3 - (_:X1 _:X2) graph:union _:Y - _:Y log:rawType _:Y_RT - _:X3 log:rawType _:X3_RT - _:Y log:notEqualTo _:X3 + :Let :param1 var:X1 + :Let :param2 var:X2 + :Let :param3 var:X3 + (var:X1 var:X2) graph:union var:Y + var:Y log:rawType var:Y_RT + var:X3 log:rawType var:X3_RT + var:Y log:notEqualTo var:X3 ); lingua:conclusion ( :test :is true diff --git a/reasoning/lingua/out/fibonacci.ttl b/reasoning/lingua/out/fibonacci.ttl index 1fbba576f..4b8136bbd 100644 --- a/reasoning/lingua/out/fibonacci.ttl +++ b/reasoning/lingua/out/fibonacci.ttl @@ -5,3 +5,4 @@ () :fibonacci (6 8). () :fibonacci (91 4660046610375530309). () :fibonacci (283 62232491515607091882574410635924603070626544377175485625797). +() :fibonacci (3674 295872959797101479478634366815157108100573212705250690577871041398423606408217262643449728342664061812585639168722421830407677671667740585806703531229882783069925750619720511808616484846128237251921414441458265138672827487722512845223115526738192067144721087756159352711138340620702266509343657403678256247195010013499661223527119909308682062873140767135468966093474944529418214755911968500799987099146489838560114063096775586903976827512299123202488315139397181279903459556726060805948910609527571241968534269554079076649680403030083743420820438603816095671532163428933363322524736324029745871445486444623006627119156710782085648303485296149604974010598940800770684835758031137479033374229914629583184427269638360355586190323578625395157899987377625662075558684705457). diff --git a/reasoning/lingua/out/peano.ttl b/reasoning/lingua/out/peano.ttl index d3f369ed4..33bd62a99 100644 --- a/reasoning/lingua/out/peano.ttl +++ b/reasoning/lingua/out/peano.ttl @@ -1,3 +1,3 @@ @prefix : . -:result :is (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s 0)))))))))))))))))))))))). +:result :is (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s (:s 0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). diff --git a/reasoning/lingua/out/pi.ttl b/reasoning/lingua/out/pi.ttl index 710c709a7..0239792e8 100644 --- a/reasoning/lingua/out/pi.ttl +++ b/reasoning/lingua/out/pi.ttl @@ -1,3 +1,3 @@ @prefix : . -(1000 3.141592653839793) :pi true. +(10000 3.141592653590042) :pi true. diff --git a/reasoning/lingua/patch.ttl b/reasoning/lingua/patch.ttl index 0d7d0be56..fe4dba613 100644 --- a/reasoning/lingua/patch.ttl +++ b/reasoning/lingua/patch.ttl @@ -1,7 +1,8 @@ @prefix rdf: . @prefix solid: . @prefix log: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # sample data @@ -12,31 +13,23 @@ # patch rule :patch_rule a lingua:ForwardRule; - lingua:vars ( - _:person - ); lingua:premise ( - _:person :familyName "Garcia" + var:person :familyName "Garcia" ( - _:person :givenName "Claudia" + var:person :givenName "Claudia" ) log:becomes ( - _:person :givenName "Alex" + var:person :givenName "Alex" ) ); lingua:conclusion (). # query :patch_query a lingua:QueryRule; - lingua:vars ( - _:person - _:fname - _:gname - ); lingua:premise ( - _:person :familyName _:fname - _:person :givenName _:gname + var:person :familyName var:fname + var:person :givenName var:gname ); lingua:conclusion ( - _:person :familyName _:fname - _:person :givenName _:gname + var:person :familyName var:fname + var:person :givenName var:gname ). diff --git a/reasoning/lingua/peano.ttl b/reasoning/lingua/peano.ttl index 97fca3802..4b1414e0c 100644 --- a/reasoning/lingua/peano.ttl +++ b/reasoning/lingua/peano.ttl @@ -1,103 +1,69 @@ -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # add :peano_add_rule1 a lingua:BackwardRule; - lingua:vars ( - _:A - ); lingua:conclusion ( - (_:A 0) :add _:A + (var:A 0) :add var:A ); lingua:premise (). :peano_add_rule2 a lingua:BackwardRule; - lingua:vars ( - _:A - _:B - _:C - ); lingua:premise ( - (_:A _:B) :add _:C + (var:A var:B) :add var:C ); lingua:conclusion ( - (_:A (:s _:B)) :add (:s _:C) + (var:A (:s var:B)) :add (:s var:C) ). # multiply :peano_multiply_rule1 a lingua:BackwardRule; - lingua:vars ( - _:A - ); lingua:conclusion ( - (_:A 0) :multiply 0 + (var:A 0) :multiply 0 ); lingua:premise (). :peano_multiply_rule2 a lingua:BackwardRule; - lingua:vars ( - _:A - _:B - _:C - _:D - ); lingua:conclusion ( - (_:A (:s _:B)) :multiply _:C + (var:A (:s var:B)) :multiply var:C ); lingua:premise ( - (_:A _:B) :multiply _:D - (_:A _:D) :add _:C + (var:A var:B) :multiply var:D + (var:A var:D) :add var:C ). # factorial :peano_factorial_rule1 a lingua:BackwardRule; - lingua:vars ( - _:A - _:B - ); lingua:conclusion ( - _:A :factorial _:B + var:A :factorial var:B ); lingua:premise ( - (_:A (:s 0)) :fac _:B + (var:A (:s 0)) :fac var:B ). :peano_factorial_rule2 a lingua:BackwardRule; - lingua:vars ( - _:A - ); lingua:conclusion ( - (0 _:A) :fac _:A + (0 var:A) :fac var:A ); lingua:premise (). :peano_factorial_rule3 a lingua:BackwardRule; - lingua:vars ( - _:A - _:B - _:C - _:D - ); lingua:conclusion ( - ((:s _:A) _:B) :fac _:C + ((:s var:A) var:B) :fac var:C ); lingua:premise ( - (_:B (:s _:A)) :multiply _:D - (_:A _:D) :fac _:C + (var:B (:s var:A)) :multiply var:D + (var:A var:D) :fac var:C ). # query :peano_query a lingua:QueryRule; - lingua:vars ( - _:A - _:B - _:C - ); lingua:premise ( - ((:s 0) (:s 0)) :add _:A - (_:A (:s (:s 0))) :multiply _:B - _:B :factorial _:C + ((:s 0) (:s (:s 0))) :add var:A + (var:A (:s (:s 0))) :multiply var:B + var:B :factorial var:C ); lingua:conclusion ( - :result :is _:C + :result :is var:C ). diff --git a/reasoning/lingua/pi.ttl b/reasoning/lingua/pi.ttl index 074d9bfb0..5fe3ac704 100644 --- a/reasoning/lingua/pi.ttl +++ b/reasoning/lingua/pi.ttl @@ -1,74 +1,46 @@ @prefix math: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . :pi_rule1 a lingua:BackwardRule; - lingua:vars ( - _:N - _:Pi - _:P - _:A - ); lingua:conclusion ( - (_:N _:Pi) :pi true + (var:N var:Pi) :pi true ); lingua:premise ( - (1 _:N 0 _:P 1) :pi true - (4 _:P) math:product _:A - (3 _:A) math:sum _:Pi + (1 var:N 0 var:P 1) :pi true + (4 var:P) math:product var:A + (3 var:A) math:sum var:Pi ). :pi_rule2 a lingua:BackwardRule; - lingua:vars ( - _:N - _:P - _:S - ); lingua:conclusion ( - (_:N _:N _:P _:P _:S) :pi true + (var:N var:N var:P var:P var:S) :pi true ); lingua:premise (). :pi_rule3 a lingua:BackwardRule; - lingua:vars ( - _:K - _:N - _:P0 - _:P - _:S - _:K1 - _:K2 - _:A - _:B - _:C - _:D - _:P1 - _:S1 - ); lingua:conclusion ( - (_:K _:N _:P0 _:P _:S) :pi true + (var:K var:N var:P0 var:P var:S) :pi true ); lingua:premise ( - _:K math:notEqualTo _:N - (_:K 1) math:sum _:K1 - (2 _:K) math:product _:K2 - (_:K2 1) math:sum _:A - (_:K2 2) math:sum _:B - (_:K2 _:A _:B) math:product _:C - (_:S _:C) math:quotient _:D - (_:P0 _:D) math:sum _:P1 - _:S math:negation _:S1 - (_:K1 _:N _:P1 _:P _:S1) :pi true + var:K math:notEqualTo var:N + (var:K 1) math:sum var:K1 + (2 var:K) math:product var:K2 + (var:K2 1) math:sum var:A + (var:K2 2) math:sum var:B + (var:K2 var:A var:B) math:product var:C + (var:S var:C) math:quotient var:D + (var:P0 var:D) math:sum var:P1 + var:S math:negation var:S1 + (var:K1 var:N var:P1 var:P var:S1) :pi true ). # query :pi_query a lingua:QueryRule; - lingua:vars ( - _:Pi - ); lingua:premise ( - (1000 _:Pi) :pi true + (10000 var:Pi) :pi true ); lingua:conclusion ( - (1000 _:Pi) :pi true + (10000 var:Pi) :pi true ). diff --git a/reasoning/lingua/sdcoding.ttl b/reasoning/lingua/sdcoding.ttl index 260779a0d..de954ae4f 100644 --- a/reasoning/lingua/sdcoding.ttl +++ b/reasoning/lingua/sdcoding.ttl @@ -1,7 +1,8 @@ @prefix list: . @prefix math: . @prefix log: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # |R) = |0, 0) + |1, 1 @@ -40,174 +41,116 @@ # KG :sdcoding_rule1 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - _:Z - ); lingua:conclusion ( - _:X :kg _:Y + var:X :kg var:Y ); lingua:premise ( - _:X :g _:Z - _:Z :k _:Y + var:X :g var:Z + var:Z :k var:Y ). # GK :sdcoding_rule2 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - _:Z - ); lingua:conclusion ( - _:X :gk _:Y + var:X :gk var:Y ); lingua:premise ( - _:X :k _:Z - _:Z :g _:Y + var:X :k var:Z + var:Z :g var:Y ). # Alice :sdcoding_rule3 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - ); lingua:conclusion ( - 0 :alice (_:X _:Y) + 0 :alice (var:X var:Y) ); lingua:premise ( - _:X :id _:Y + var:X :id var:Y ). :sdcoding_rule4 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - ); lingua:conclusion ( - 1 :alice (_:X _:Y) + 1 :alice (var:X var:Y) ); lingua:premise ( - _:X :g _:Y + var:X :g var:Y ). :sdcoding_rule5 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - ); lingua:conclusion ( - 2 :alice (_:X _:Y) + 2 :alice (var:X var:Y) ); lingua:premise ( - _:X :k _:Y + var:X :k var:Y ). :sdcoding_rule6 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - ); lingua:conclusion ( - 3 :alice (_:X _:Y) + 3 :alice (var:X var:Y) ); lingua:premise ( - _:X :kg _:Y + var:X :kg var:Y ). # Bob :sdcoding_rule7 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - ); lingua:conclusion ( - (_:X _:Y) :bob 0 + (var:X var:Y) :bob 0 ); lingua:premise ( - _:X :gk _:Y + var:X :gk var:Y ). :sdcoding_rule8 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - ); lingua:conclusion ( - (_:X _:Y) :bob 1 + (var:X var:Y) :bob 1 ); lingua:premise ( - _:X :k _:Y + var:X :k var:Y ). :sdcoding_rule9 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - ); lingua:conclusion ( - (_:X _:Y) :bob 2 + (var:X var:Y) :bob 2 ); lingua:premise ( - _:X :g _:Y + var:X :g var:Y ). :sdcoding_rule10 a lingua:BackwardRule; - lingua:vars ( - _:X - _:Y - ); lingua:conclusion ( - (_:X _:Y) :bob 3 + (var:X var:Y) :bob 3 ); lingua:premise ( - _:X :id _:Y + var:X :id var:Y ). # superdense coding :sdcoding_rule11 a lingua:ForwardRule; - lingua:vars ( - _:N - _:A - _:B - _:M - _:X - _:Y - _:Z - _:L - _:S - _:I - ); lingua:premise ( - _:N :alice _:A - _:B :bob _:M + var:N :alice var:A + var:B :bob var:M ( 1 ( - _:X :r _:Y - _:N :alice (_:X _:Z) - (_:Z _:Y) :bob _:M + var:X :r var:Y + var:N :alice (var:X var:Z) + (var:Z var:Y) :bob var:M ) - _:L - ) log:collectAllIn _:S - _:L list:length _:I - (_:I 2) math:remainder 1 + var:L + ) log:collectAllIn var:S + var:L list:length var:I + (var:I 2) math:remainder 1 ); lingua:conclusion ( - _:N :sdcoding _:M + var:N :sdcoding var:M ). # query :sdcoding_query a lingua:QueryRule; - lingua:vars ( - _:N - _:M - ); lingua:premise ( - _:N :sdcoding _:M + var:N :sdcoding var:M ); lingua:conclusion ( - () :sdcoding (_:N _:M) + () :sdcoding (var:N var:M) ). diff --git a/reasoning/lingua/sha512.ttl b/reasoning/lingua/sha512.ttl index b6ad78515..f0592febe 100644 --- a/reasoning/lingua/sha512.ttl +++ b/reasoning/lingua/sha512.ttl @@ -1,19 +1,16 @@ @prefix crypto: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . :Let :param "hello world". # query :sha512_query a lingua:QueryRule; - lingua:vars ( - _:X - _:Y - ); lingua:premise ( - :Let :param _:X - _:X crypto:sha512 _:Y + :Let :param var:X + var:X crypto:sha512 var:Y ); lingua:conclusion ( - () :sha512 (_:X _:Y) + () :sha512 (var:X var:Y) ). diff --git a/reasoning/lingua/socrates.ttl b/reasoning/lingua/socrates.ttl index 2d0b36313..e9a6475dd 100644 --- a/reasoning/lingua/socrates.ttl +++ b/reasoning/lingua/socrates.ttl @@ -1,6 +1,7 @@ @prefix rdf: . @prefix rdfs: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # facts @@ -9,27 +10,19 @@ # rdfs subclass :rdfs_subclass_rule a lingua:ForwardRule; - lingua:vars ( - _:A - _:B - _:S - ); lingua:premise ( - _:A rdfs:subClassOf _:B - _:S rdf:type _:A + var:A rdfs:subClassOf var:B + var:S rdf:type var:A ); lingua:conclusion ( - _:S rdf:type _:B + var:S rdf:type var:B ). # query :socrates_query a lingua:QueryRule; - lingua:vars ( - _:S - ); lingua:premise ( - _:S rdf:type :Mortal + var:S rdf:type :Mortal ); lingua:conclusion ( - _:S rdf:type :Mortal + var:S rdf:type :Mortal ). diff --git a/reasoning/lingua/turing.ttl b/reasoning/lingua/turing.ttl index 5bad6ae64..9a5804855 100644 --- a/reasoning/lingua/turing.ttl +++ b/reasoning/lingua/turing.ttl @@ -1,190 +1,111 @@ @prefix list: . @prefix log: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # interpreter for Turing machine :turing_rule1 a lingua:BackwardRule; - lingua:vars ( - _:OutTape - _:Machine - _:I - ); lingua:conclusion ( - () :compute _:OutTape + () :compute var:OutTape ); lingua:premise ( - _:Machine :start _:I - (_:I () "#" ()) :find _:OutTape + var:Machine :start var:I + (var:I () "#" ()) :find var:OutTape ). :turing_rule2 a lingua:BackwardRule; - lingua:vars ( - _:List - _:OutTape - _:Head - _:Tail - _:Machine - _:I - ); lingua:conclusion ( - _:List :compute _:OutTape + var:List :compute var:OutTape ); lingua:premise ( - _:List list:firstRest (_:Head _:Tail) - _:Machine :start _:I - (_:I () _:Head _:Tail) :find _:OutTape + var:List list:firstRest (var:Head var:Tail) + var:Machine :start var:I + (var:I () var:Head var:Tail) :find var:OutTape ). :turing_rule3 a lingua:BackwardRule; - lingua:vars ( - _:State - _:Left - _:Cell - _:Right - _:OutTape - _:Write - _:Move - _:Next - _:A - _:B - _:C - ); lingua:conclusion ( - (_:State _:Left _:Cell _:Right) :find _:OutTape + (var:State var:Left var:Cell var:Right) :find var:OutTape ); lingua:premise ( - (_:State _:Cell _:Write _:Move) :tape _:Next - (_:Move _:Left _:Write _:Right _:A _:B _:C) :move true - (_:Next _:A _:B _:C) :continue _:OutTape + (var:State var:Cell var:Write var:Move) :tape var:Next + (var:Move var:Left var:Write var:Right var:A var:B var:C) :move true + (var:Next var:A var:B var:C) :continue var:OutTape ). :turing_rule4 a lingua:BackwardRule; - lingua:vars ( - _:Left - _:Cell - _:Right - _:OutTape - _:R - _:List - ); lingua:conclusion ( - (:halt _:Left _:Cell _:Right) :continue _:OutTape + (:halt var:Left var:Cell var:Right) :continue var:OutTape ); lingua:premise ( - _:Left :reverse _:R - _:List list:firstRest (_:Cell _:Right) - (_:R _:List) list:append _:OutTape + var:Left :reverse var:R + var:List list:firstRest (var:Cell var:Right) + (var:R var:List) list:append var:OutTape ). :turing_rule5 a lingua:BackwardRule; - lingua:vars ( - _:State - _:Left - _:Cell - _:Right - _:OutTape - ); lingua:conclusion ( - (_:State _:Left _:Cell _:Right) :continue _:OutTape + (var:State var:Left var:Cell var:Right) :continue var:OutTape ); lingua:premise ( - (_:State _:Left _:Cell _:Right) :find _:OutTape + (var:State var:Left var:Cell var:Right) :find var:OutTape ). :turing_rule6 a lingua:BackwardRule; - lingua:vars ( - _:Cell - _:Right - _:L - ); lingua:conclusion ( - (:left () _:Cell _:Right () "#" _:L) :move true + (:left () var:Cell var:Right () "#" var:L) :move true ); lingua:premise ( - _:L list:firstRest (_:Cell _:Right) + var:L list:firstRest (var:Cell var:Right) ). :turing_rule7 a lingua:BackwardRule; - lingua:vars ( - _:List - _:Cell - _:Right - _:Tail - _:Head - _:L - ); lingua:conclusion ( - (:left _:List _:Cell _:Right _:Tail _:Head _:L) :move true + (:left var:List var:Cell var:Right var:Tail var:Head var:L) :move true ); lingua:premise ( - _:List list:firstRest (_:Head _:Tail) - _:L list:firstRest (_:Cell _:Right) + var:List list:firstRest (var:Head var:Tail) + var:L list:firstRest (var:Cell var:Right) ). :turing_rule8 a lingua:BackwardRule; - lingua:vars ( - _:Left - _:Cell - _:Right - ); lingua:conclusion ( - (:stop _:Left _:Cell _:Right _:Left _:Cell _:Right) :move true + (:stop var:Left var:Cell var:Right var:Left var:Cell var:Right) :move true ); lingua:premise (). :turing_rule9 a lingua:BackwardRule; - lingua:vars ( - _:Left - _:Cell - _:L - ); lingua:conclusion ( - (:right _:Left _:Cell () _:L "#" ()) :move true + (:right var:Left var:Cell () var:L "#" ()) :move true ); lingua:premise ( - _:L list:firstRest (_:Cell _:Left) + var:L list:firstRest (var:Cell var:Left) ). :turing_rule10 a lingua:BackwardRule; - lingua:vars ( - _:Left - _:Cell - _:List - _:L - _:Head - _:Tail - ); lingua:conclusion ( - (:right _:Left _:Cell _:List _:L _:Head _:Tail) :move true + (:right var:Left var:Cell var:List var:L var:Head var:Tail) :move true ); lingua:premise ( - _:List list:firstRest (_:Head _:Tail) - _:L list:firstRest (_:Cell _:Left) + var:List list:firstRest (var:Head var:Tail) + var:L list:firstRest (var:Cell var:Left) ). :turing_rule11 a lingua:BackwardRule; - lingua:vars (); lingua:conclusion ( () :reverse () ); lingua:premise (). :turing_rule12 a lingua:BackwardRule; - lingua:vars ( - _:List - _:Reverse - _:Head - _:Tail - _:R - ); lingua:conclusion ( - _:List :reverse _:Reverse + var:List :reverse var:Reverse ); lingua:premise ( - _:List list:firstRest (_:Head _:Tail) - _:Tail :reverse _:R - (_:R (_:Head)) list:append _:Reverse + var:List list:firstRest (var:Head var:Tail) + var:Tail :reverse var:R + (var:R (var:Head)) list:append var:Reverse ). # a Turing machine to add 1 to a binary number @@ -199,21 +120,15 @@ # query :turing_query a lingua:QueryRule; - lingua:vars ( - _:A1 - _:A2 - _:A3 - _:A4 - ); lingua:premise ( - (1 0 1 0 0 1) :compute _:A1 - (1 0 1 1 1 1) :compute _:A2 - (1 1 1 1 1 1) :compute _:A3 - () :compute _:A4 + (1 0 1 0 0 1) :compute var:A1 + (1 0 1 1 1 1) :compute var:A2 + (1 1 1 1 1 1) :compute var:A3 + () :compute var:A4 ); lingua:conclusion ( - (1 0 1 0 0 1) :compute _:A1 - (1 0 1 1 1 1) :compute _:A2 - (1 1 1 1 1 1) :compute _:A3 - () :compute _:A4 + (1 0 1 0 0 1) :compute var:A1 + (1 0 1 1 1 1) :compute var:A2 + (1 1 1 1 1 1) :compute var:A3 + () :compute var:A4 ). diff --git a/reasoning/lingua/union.ttl b/reasoning/lingua/union.ttl index d531952cb..556d27586 100644 --- a/reasoning/lingua/union.ttl +++ b/reasoning/lingua/union.ttl @@ -1,6 +1,7 @@ @prefix graph: . @prefix log: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . :Let :param1 ( @@ -16,16 +17,11 @@ #query :union_query a lingua:QueryRule; - lingua:vars ( - _:X1 - _:X2 - _:Y - ); lingua:premise ( - :Let :param1 _:X1 - :Let :param2 _:X2 - (_:X1 _:X2) graph:union _:Y + :Let :param1 var:X1 + :Let :param2 var:X2 + (var:X1 var:X2) graph:union var:Y ); lingua:conclusion ( - (_:X1 _:X2) :union _:Y + (var:X1 var:X2) :union var:Y ). diff --git a/reasoning/lingua/universal.ttl b/reasoning/lingua/universal.ttl index 59d94421a..6c7829986 100644 --- a/reasoning/lingua/universal.ttl +++ b/reasoning/lingua/universal.ttl @@ -1,47 +1,36 @@ @prefix rdf: . @prefix rdfs: . @prefix log: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # \Every x: type(x, Resource :universal_statements_rule1 a lingua:BackwardRule; - lingua:vars ( - _:X - ); lingua:conclusion ( - _:X rdf:type rdfs:Resource + var:X rdf:type rdfs:Resource ); lingua:premise (). # Everybody loves somebody who is lonely :universal_statements_rule2 a lingua:BackwardRule; - lingua:vars ( - _:A - _:B - ); lingua:conclusion ( - _:A :loves _:B + var:A :loves var:B ); lingua:premise ( - (_:A) log:skolem _:B + (var:A) log:skolem var:B ). :universal_statements_rule3 a lingua:BackwardRule; - lingua:vars ( - _:B - _:A - ); lingua:conclusion ( - _:B :is :lonely + var:B :is :lonely ); lingua:premise ( - (_:A) log:skolem _:B + (var:A) log:skolem var:B ). # queries :universal_statements_query1 a lingua:QueryRule; - lingua:vars (); lingua:premise ( :pat rdf:type rdfs:Resource ); @@ -50,14 +39,11 @@ ). :universal_statements_query2 a lingua:QueryRule; - lingua:vars ( - _:X - ); lingua:premise ( - :bob :loves _:X - _:X :is :lonely + :bob :loves var:X + var:X :is :lonely ); lingua:conclusion ( - :bob :loves _:X - _:X :is :lonely + :bob :loves var:X + var:X :is :lonely ). diff --git a/reasoning/lingua/unpack.ttl b/reasoning/lingua/unpack.ttl index de5a792f3..699c4c582 100644 --- a/reasoning/lingua/unpack.ttl +++ b/reasoning/lingua/unpack.ttl @@ -1,142 +1,98 @@ @prefix list: . @prefix log: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # sample data from RubenD -_:b1 :data ( - _:b2 :package ( - _:b3 :content ( +var:b1 :data ( + var:b2 :package ( + var:b3 :content ( :a :b _:c - _:b4 :package ( - _:b5 :content ( + var:b4 :package ( + var:b5 :content ( :u :v _:w - _:b6 :package ( - _:b7 :content ( + var:b6 :package ( + var:b7 :content ( :x :y _:z ) - _:b7 :usable_until :yesterday + var:b7 :usable_until :yesterday ) - _:b6 :tag :invalid + var:b6 :tag :invalid ) - _:b5 :usable_until :tomorrow - _:b5 :p :o + var:b5 :usable_until :tomorrow + var:b5 :p :o ) - _:b4 :tag :valid + var:b4 :tag :valid ) - _:b3 :usable_until :next_week + var:b3 :usable_until :next_week ) - _:b2 :tag :valid + var:b2 :tag :valid ). # the logic for unpack using backward rules :unpack_rule1 a lingua:BackwardRule; - lingua:vars (); lingua:conclusion ( () :unpackl () ); lingua:premise (). :unpack_rule2 a lingua:BackwardRule; - lingua:vars ( - _:g - _:h - _:f - _:r - _:a - _:b - ); lingua:conclusion ( - _:g :unpackl _:h + var:g :unpackl var:h ); lingua:premise ( - _:g list:firstRest (_:f _:r) - _:f :unpack _:a - _:r :unpackl _:b - (_:a _:b) list:append _:h + var:g list:firstRest (var:f var:r) + var:f :unpack var:a + var:r :unpackl var:b + (var:a var:b) list:append var:h ). :unpack_rule3 a lingua:BackwardRule; - lingua:vars ( - _:b - _:p - _:f - _:l - _:a - _:c - _:t - _:d - ); lingua:conclusion ( - (_:b :package _:p) :unpack _:f + (var:b :package var:p) :unpack var:f ); lingua:premise ( - _:p list:lott _:l - _:l list:member (_:a :content _:c) - _:l list:member (_:a :usable_until _:t) - (:tomorrow :next_week) list:member _:t - _:c list:lott _:d - _:d :unpackl _:f + var:p list:lott var:l + var:l list:member (var:a :content var:c) + var:l list:member (var:a :usable_until var:t) + (:tomorrow :next_week) list:member var:t + var:c list:lott var:d + var:d :unpackl var:f ). :unpack_rule4 a lingua:BackwardRule; - lingua:vars ( - _:b - _:p - _:l - _:a - _:c - _:t - ); lingua:conclusion ( - (_:b :package _:p) :unpack () + (var:b :package var:p) :unpack () ); lingua:premise ( - _:p list:lott _:l - _:l list:member (_:a :content _:c) - _:l list:member (_:a :usable_until _:t) - (:yesterday :last_week) list:member _:t + var:p list:lott var:l + var:l list:member (var:a :content var:c) + var:l list:member (var:a :usable_until var:t) + (:yesterday :last_week) list:member var:t ). :unpack_rule5 a lingua:BackwardRule; - lingua:vars ( - _:b - _:p - ); lingua:conclusion ( - (_:b :tag _:p) :unpack () + (var:b :tag var:p) :unpack () ); lingua:premise (). :unpack_rule6 a lingua:BackwardRule; - lingua:vars ( - _:g - _:a - _:p - _:b - _:q - ); lingua:conclusion ( - _:g :unpack (_:g) + var:g :unpack (var:g) ); lingua:premise ( - (_:g) list:notMember (_:a :package _:p) - (_:g) list:notMember (_:b :tag _:q) + (var:g) list:notMember (var:a :package var:p) + (var:g) list:notMember (var:b :tag var:q) ). # unpack the triples that are usable in the future :unpack_query a lingua:QueryRule; - lingua:vars ( - _:b - _:g - _:l - _:m - _:u - ); lingua:premise ( - _:b :data _:g - _:g list:lott _:l - _:l :unpackl _:m - _:u list:lott _:m + var:b :data var:g + var:g list:lott var:l + var:l :unpackl var:m + var:u list:lott var:m ); - lingua:conclusion _:u. + lingua:conclusion var:u. diff --git a/reasoning/lingua/witch.ttl b/reasoning/lingua/witch.ttl index c815dea1e..67c9f2b18 100644 --- a/reasoning/lingua/witch.ttl +++ b/reasoning/lingua/witch.ttl @@ -1,18 +1,16 @@ @prefix rdf: . -@prefix lingua: . +@prefix lingua: . +@prefix var: . @prefix : . # \forall x : BURNS(x) /\ WOMAN(x) => WITCH(x :witch_rule1 a lingua:ForwardRule; - lingua:vars ( - _:X - ); lingua:premise ( - _:X rdf:type :BURNS - _:X rdf:type :WOMAN + var:X rdf:type :BURNS + var:X rdf:type :WOMAN ); lingua:conclusion ( - _:X rdf:type :WITCH + var:X rdf:type :WITCH ). # WOMAN(GIRL @@ -20,26 +18,20 @@ # \forall x : ISMADEOFWOOD(x) => BURNS(x :witch_rule2 a lingua:ForwardRule; - lingua:vars ( - _:X - ); lingua:premise ( - _:X rdf:type :ISMADEOFWOOD + var:X rdf:type :ISMADEOFWOOD ); lingua:conclusion ( - _:X rdf:type :BURNS + var:X rdf:type :BURNS ). # \forall x : FLOATS(x) => ISMADEOFWOOD(x :witch_rule3 a lingua:ForwardRule; - lingua:vars ( - _:X - ); lingua:premise ( - _:X rdf:type :FLOATS + var:X rdf:type :FLOATS ); lingua:conclusion ( - _:X rdf:type :ISMADEOFWOOD + var:X rdf:type :ISMADEOFWOOD ). # FLOATS(DUCK @@ -47,16 +39,12 @@ # \forall x,y : FLOATS(x) /\ SAMEWEIGHT(x,y) => FLOATS(y :witch_rule4 a lingua:ForwardRule; - lingua:vars ( - _:X - _:Y - ); lingua:premise ( - _:X rdf:type :FLOATS - _:X :SAMEWEIGHT _:Y + var:X rdf:type :FLOATS + var:X :SAMEWEIGHT var:Y ); lingua:conclusion ( - _:Y rdf:type :FLOATS + var:Y rdf:type :FLOATS ). # and, by experiment @@ -65,12 +53,9 @@ # who's a witch? :witch_query a lingua:QueryRule; - lingua:vars ( - _:S - ); lingua:premise ( - _:S rdf:type :WITCH + var:S rdf:type :WITCH ); lingua:conclusion ( - _:S rdf:type :WITCH + var:S rdf:type :WITCH ).