diff --git a/reasoning/control-system/README b/reasoning/control-system/README new file mode 100644 index 000000000..f71e68292 --- /dev/null +++ b/reasoning/control-system/README @@ -0,0 +1,5 @@ +-------------- +Control System +-------------- + +Examples of a control system. diff --git a/reasoning/control-system/answer-001.n3 b/reasoning/control-system/answer-001.n3 new file mode 100644 index 000000000..45dc0284a --- /dev/null +++ b/reasoning/control-system/answer-001.n3 @@ -0,0 +1,3 @@ +@prefix : . + +:actuator1 :control1 26.08 . diff --git a/reasoning/cs/data-001.n3 b/reasoning/control-system/data-001.n3 similarity index 100% rename from reasoning/cs/data-001.n3 rename to reasoning/control-system/data-001.n3 diff --git a/reasoning/control-system/proof-001.n3 b/reasoning/control-system/proof-001.n3 new file mode 100644 index 000000000..cf53a4eae --- /dev/null +++ b/reasoning/control-system/proof-001.n3 @@ -0,0 +1,105 @@ +@prefix skolem: . +@prefix r: . +@prefix : . +@prefix n3: . +@prefix math: . +@prefix var: . + +skolem:proof a r:Proof, r:Conjunction; + r:component skolem:lemma1; + r:gives { + :actuator1 :control1 26.08 . + }. + +skolem:lemma1 a r:Inference; + r:gives { + :actuator1 :control1 26.08 . + }; + r:evidence ( + skolem:lemma2 + ); + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/cs#actuator1"]]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo 26.08]; + r:rule skolem:lemma3. + +skolem:lemma2 a r:Inference; + r:gives { + :actuator1 :control1 26.08 . + }; + r:evidence ( + skolem:lemma4 + skolem:lemma5 + skolem:lemma6 + skolem:lemma7 + [ a r:Fact; r:gives {(29 24) math:difference 5}] + [ a r:Fact; r:gives {(22 24) math:difference -2}] + [ a r:Fact; r:gives {(5.8 5) math:product 29.0}] + [ a r:Fact; r:gives {(7.3 5) math:quotient 1.46}] + [ a r:Fact; r:gives {(1.46 -2) math:product -2.92}] + [ a r:Fact; r:gives {(29.0 -2.92) math:sum 26.08}] + ); + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo 56967]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo 22]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo 24]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo 29]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo 5]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo -2]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo 29.0]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo 1.46]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_8"]; r:boundTo -2.92]; + r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_9"]; r:boundTo 26.08]; + r:rule skolem:lemma8. + +skolem:lemma3 a r:Extraction; + r:gives { + @forAll var:x_0, var:x_1. { + var:x_0 :control1 var:x_1. + } => { + var:x_0 :control1 var:x_1. + }. + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma4 a r:Extraction; + r:gives { + :input3 :measurement3 56967 . + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma5 a r:Extraction; + r:gives { + :state3 :observation3 22 . + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma6 a r:Extraction; + r:gives { + :output2 :measurement4 24 . + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma7 a r:Extraction; + r:gives { + :output2 :target2 29 . + }; + r:because [ a r:Parsing; r:source ]. + +skolem:lemma8 a r:Extraction; + r:gives { + @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. { + :input3 :measurement3 var:x_0. + :state3 :observation3 var:x_1. + :output2 :measurement4 var:x_2. + :output2 :target2 var:x_3. + (var:x_3 var:x_2) math:difference var:x_4. + (var:x_1 var:x_2) math:difference var:x_5. + (5.8 var:x_4) math:product var:x_6. + (7.3 var:x_4) math:quotient var:x_7. + (var:x_7 var:x_5) math:product var:x_8. + (var:x_6 var:x_8) math:sum var:x_9. + } => { + :actuator1 :control1 var:x_9. + }. + }; + r:because [ a r:Parsing; r:source ]. + diff --git a/reasoning/cs/query-001.n3 b/reasoning/control-system/query-001.n3 similarity index 100% rename from reasoning/cs/query-001.n3 rename to reasoning/control-system/query-001.n3 diff --git a/reasoning/cs/rules-001.n3 b/reasoning/control-system/rules-001.n3 similarity index 72% rename from reasoning/cs/rules-001.n3 rename to reasoning/control-system/rules-001.n3 index 674b398ac..08aa53d62 100644 --- a/reasoning/cs/rules-001.n3 +++ b/reasoning/control-system/rules-001.n3 @@ -1,20 +1,7 @@ @prefix math: . @prefix : . -# forward rules -{ - :input1 :measurement10 ?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 -} -=> -{ - :actuator1 :control1 ?C. -}. - +# forward rule { :input3 :measurement3 ?M3. :state3 :observation3 ?P3. @@ -29,7 +16,7 @@ } => { - :actuator2 :control1 ?C. + :actuator1 :control1 ?C. }. # backward rules diff --git a/reasoning/control-system/test b/reasoning/control-system/test new file mode 100755 index 000000000..34c444b64 --- /dev/null +++ b/reasoning/control-system/test @@ -0,0 +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/control-system/data-001.n3 https://eyereasoner.github.io/eye/reasoning/control-system/rules-001.n3 --query https://eyereasoner.github.io/eye/reasoning/control-system/query-001.n3 --output answer-001.n3 +eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. https://eyereasoner.github.io/eye/reasoning/control-system/data-001.n3 https://eyereasoner.github.io/eye/reasoning/control-system/rules-001.n3 --query https://eyereasoner.github.io/eye/reasoning/control-system/query-001.n3 --output proof-001.n3 diff --git a/reasoning/cs/README b/reasoning/cs/README deleted file mode 100644 index fd2968707..000000000 --- a/reasoning/cs/README +++ /dev/null @@ -1,5 +0,0 @@ ---------------- -Control Systems ---------------- - -Examples of control systems. diff --git a/reasoning/cs/answer-001.n3 b/reasoning/cs/answer-001.n3 deleted file mode 100644 index dc6ea3c2c..000000000 --- a/reasoning/cs/answer-001.n3 +++ /dev/null @@ -1,4 +0,0 @@ -@prefix : . - -:actuator1 :control1 39.27346198678276 . -:actuator2 :control1 26.08 . diff --git a/reasoning/cs/proof-001.n3 b/reasoning/cs/proof-001.n3 deleted file mode 100644 index 69ab324df..000000000 --- a/reasoning/cs/proof-001.n3 +++ /dev/null @@ -1,200 +0,0 @@ -@prefix skolem: . -@prefix r: . -@prefix : . -@prefix n3: . -@prefix math: . -@prefix var: . - -skolem:proof a r:Proof, r:Conjunction; - r:component skolem:lemma1; - r:component skolem:lemma2; - r:gives { - :actuator1 :control1 39.27346198678276 . - :actuator2 :control1 26.08 . - }. - -skolem:lemma1 a r:Inference; - r:gives { - :actuator1 :control1 39.27346198678276 . - }; - r:evidence ( - skolem:lemma3 - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/cs#actuator1"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo 39.27346198678276]; - r:rule skolem:lemma4. - -skolem:lemma2 a r:Inference; - r:gives { - :actuator2 :control1 26.08 . - }; - r:evidence ( - skolem:lemma5 - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/cs#actuator2"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo 26.08]; - r:rule skolem:lemma4. - -skolem:lemma3 a r:Inference; - r:gives { - :actuator1 :control1 39.27346198678276 . - }; - r:evidence ( - skolem:lemma6 - skolem:lemma7 - skolem:lemma8 - [ a r:Fact; r:gives {(2.23606797749979 19.6) math:product 43.82693235899588}] - [ a r:Fact; r:gives {(10 4.553470372213121) math:exponentiation 35766}] - [ a r:Fact; r:gives {(43.82693235899588 4.553470372213121) math:difference 39.27346198678276}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo 2.23606797749979]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo 35766]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo 43.82693235899588]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo 4.553470372213121]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo 39.27346198678276]; - r:rule skolem:lemma9. - -skolem:lemma4 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1. { - var:x_0 :control1 var:x_1. - } => { - var:x_0 :control1 var:x_1. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma5 a r:Inference; - r:gives { - :actuator2 :control1 26.08 . - }; - r:evidence ( - skolem:lemma10 - skolem:lemma11 - skolem:lemma12 - skolem:lemma13 - [ a r:Fact; r:gives {(29 24) math:difference 5}] - [ a r:Fact; r:gives {(22 24) math:difference -2}] - [ a r:Fact; r:gives {(5.8 5) math:product 29.0}] - [ a r:Fact; r:gives {(7.3 5) math:quotient 1.46}] - [ a r:Fact; r:gives {(1.46 -2) math:product -2.92}] - [ a r:Fact; r:gives {(29.0 -2.92) math:sum 26.08}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo 56967]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo 22]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo 24]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo 29]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo 5]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo -2]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo 29.0]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo 1.46]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_8"]; r:boundTo -2.92]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_9"]; r:boundTo 26.08]; - r:rule skolem:lemma14. - -skolem:lemma6 a r:Inference; - r:gives { - :input1 :measurement10 2.23606797749979 . - }; - r:evidence ( - skolem:lemma15 - [ a r:Fact; r:gives {6 math:lessThan 11}] - [ a r:Fact; r:gives {(11 6) math:difference 5}] - [ a r:Fact; r:gives {(5 0.5) math:exponentiation 2.23606797749979}] - ); - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "https://eyereasoner.github.io/eye/reasoning/cs#input1"]]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo 6]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo 11]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo 5]; - r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo 2.23606797749979]; - r:rule skolem:lemma16. - -skolem:lemma7 a r:Extraction; - r:gives { - :input2 :measurement2 true. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma8 a r:Extraction; - r:gives { - :disturbance1 :measurement3 35766 . - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma9 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4. { - :input1 :measurement10 var:x_0. - :input2 :measurement2 true. - :disturbance1 :measurement3 var:x_1. - (var:x_0 19.6) math:product var:x_2. - (10 var:x_3) math:exponentiation var:x_1. - (var:x_2 var:x_3) math:difference var:x_4. - } => { - :actuator1 :control1 var:x_4. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma10 a r:Extraction; - r:gives { - :input3 :measurement3 56967 . - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma11 a r:Extraction; - r:gives { - :state3 :observation3 22 . - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma12 a r:Extraction; - r:gives { - :output2 :measurement4 24 . - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma13 a r:Extraction; - r:gives { - :output2 :target2 29 . - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma14 a r:Extraction; - r:gives { - @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. { - :input3 :measurement3 var:x_0. - :state3 :observation3 var:x_1. - :output2 :measurement4 var:x_2. - :output2 :target2 var:x_3. - (var:x_3 var:x_2) math:difference var:x_4. - (var:x_1 var:x_2) math:difference var:x_5. - (5.8 var:x_4) math:product var:x_6. - (7.3 var:x_4) math:quotient var:x_7. - (var:x_7 var:x_5) math:product var:x_8. - (var:x_6 var:x_8) math:sum var:x_9. - } => { - :actuator2 :control1 var:x_9. - }. - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma15 a r:Extraction; - r:gives { - :input1 :measurement1 (6 11). - }; - r:because [ a r:Parsing; r:source ]. - -skolem:lemma16 a r:Extraction; - r:gives { - @forAll var:x_0, var:x_1, var:x_2, var:x_3, var:x_4. { - var:x_0 :measurement10 var:x_4. - } <= { - var:x_0 :measurement1 (var:x_1 var:x_2). - var:x_1 math:lessThan var:x_2. - (var:x_2 var:x_1) math:difference var:x_3. - (var:x_3 0.5) math:exponentiation var:x_4. - }. - }; - r:because [ a r:Parsing; r:source ]. - diff --git a/reasoning/cs/test b/reasoning/cs/test deleted file mode 100755 index 19d82c96d..000000000 --- a/reasoning/cs/test +++ /dev/null @@ -1,3 +0,0 @@ -#!/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/cs/data-001.n3 https://eyereasoner.github.io/eye/reasoning/cs/rules-001.n3 --query https://eyereasoner.github.io/eye/reasoning/cs/query-001.n3 --output answer-001.n3 -eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --wcache https://eyereasoner.github.io/eye/reasoning .. https://eyereasoner.github.io/eye/reasoning/cs/data-001.n3 https://eyereasoner.github.io/eye/reasoning/cs/rules-001.n3 --query https://eyereasoner.github.io/eye/reasoning/cs/query-001.n3 --output proof-001.n3