| Step | Formula | Justification | Bindings |
|---|---|---|---|
| 1 | 22 :notGreaterThan 24 . | built-in Axiom math:notGreaterThan | |
| 2 | { ( :Sam_mortgage :City_Wide_refi ) :payoff_wait 22 . } log:includes { ( :Sam_mortgage :City_Wide_refi ) :payoff_wait 22 . } . | built-in Axiom log:includes | |
| 3 | ... | parsing <refi_ex.n3> | |
| 4 | :Spreadsheet c:controls_property :payoff_wait . | erasure from step 3 | |
| 5 | { :City_Wide :offers :City_Wide_refi . :City_Wide_refi :cost 3700; :rate_offset 0.25 . } log:includes {:City_Wide_refi :cost 3700 . } . | built-in Axiom log:includes | |
| 6 | :Citi_Wide_brochure c:says {:City_Wide :offers :City_Wide_refi . :City_Wide_refi :cost 3700; :rate_offset 0.25 . }; c:speaks_for :City_Wide . | erasure from step 3 | |
| 7 | ... | parsing <speech.n3> | |
| 8 | @forAll :A, :B, :s . { :A c:says :s; c:speaks_for :B . } log:implies {:B c:says :s . } . | erasure from step 7 | |
| 9 | ... | rule from step 8 applied to steps (6,) | {'A': u'<refi_ex#Citi_Wide_brochure>', 's': '{3}', 'B': u'<refi_ex#City_Wide>'} |
| 10 | :City_Wide c:says {:City_Wide :offers :City_Wide_refi . :City_Wide_refi :cost 3700; :rate_offset 0.25 . } . | erasure from step 9 | |
| 11 | :City_Wide c:controls_property :cost . | erasure from step 3 | |
| 12 | @forAll :obj, :pred, :subj, spe:A . { @forSome run:_g11 . run:_g11 log:includes {:subj :pred :obj . } . spe:A :controls_property :pred; :says run:_g11 . } log:implies {:subj :pred :obj . } . | erasure from step 7 | |
| 13 | ... | rule from step 12 applied to steps (5, 10, 11) | {'A': u'<refi_ex#City_Wide>', 'pred': u'<refi_ex#cost>', 'obj': '"3700"', 'subj': u'<refi_ex#City_Wide_refi>', '_g_L91C13': '{3}'} |
| 14 | :City_Wide_refi :cost 3700 . | erasure from step 13 | |
| 15 | :Sam_mortgage :balance 200000; :rate 6.125 . | erasure from step 3 | |
| 16 | { :Fed :rate 4.5 . } log:includes {:Fed :rate 4.5 . } . | built-in Axiom log:includes | |
| 17 | :WSJ c:controls_property :rate . | erasure from step 3 | |
| 18 | :MelissaByPhone c:says { @forSome run:_g12 . ( :Melissa :WSJ ) c:quoting run:_g12 . run:_g12 c:says {:Fed :rate 4.5 . } . }; c:speaks_for :Melissa . | erasure from step 3 | |
| 19 | @forAll :A, :B, :s . { :A c:says :s; c:speaks_for :B . } log:implies {:B c:says :s . } . | erasure from step 7 | |
| 20 | ... | rule from step 19 applied to steps (18,) | {'A': u'<refi_ex#MelissaByPhone>', 's': '{2}', 'B': u'<refi_ex#Melissa>'} |
| 21 | :Melissa c:says { @forSome run:_g12 . ( :Melissa :WSJ ) c:quoting run:_g12 . run:_g12 c:says {:Fed :rate 4.5 . } . } . | erasure from step 20 | |
| 22 | @forAll :A, :B, :s . { :A :says { ( :A :B ) :quoting [ :says :s ] . } . } log:implies {:B :says :s . } . | erasure from step 7 | |
| 23 | ... | rule from step 22 applied to steps (21,) | {'A': u'<refi_ex#Melissa>', 's': '{Fed rate "4.5"}', 'B': u'<refi_ex#WSJ>'} |
| 24 | :WSJ c:says {:Fed :rate 4.5 . } . | erasure from step 23 | |
| 25 | @forAll :obj, :pred, :subj, spe:A . { @forSome run:_g11 . run:_g11 log:includes {:subj :pred :obj . } . spe:A :controls_property :pred; :says run:_g11 . } log:implies {:subj :pred :obj . } . | erasure from step 7 | |
| 26 | ... | rule from step 25 applied to steps (16, 17, 24) | {'A': u'<refi_ex#WSJ>', 'pred': u'<refi_ex#rate>', 'obj': '"4.5"', 'subj': u'<refi_ex#Fed>', '_g_L91C13': '{Fed rate "4.5"}'} |
| 27 | :Fed :rate 4.5 . | erasure from step 26 | |
| 28 | { :City_Wide :offers :City_Wide_refi . :City_Wide_refi :cost 3700; :rate_offset 0.25 . } log:includes {:City_Wide_refi :rate_offset 0.25 . } . | built-in Axiom log:includes | |
| 29 | :City_Wide c:says {:City_Wide :offers :City_Wide_refi . :City_Wide_refi :cost 3700; :rate_offset 0.25 . } . | erasure from step 9 | |
| 30 | :City_Wide c:controls_property :rate_offset . | erasure from step 3 | |
| 31 | @forAll :obj, :pred, :subj, spe:A . { @forSome run:_g11 . run:_g11 log:includes {:subj :pred :obj . } . spe:A :controls_property :pred; :says run:_g11 . } log:implies {:subj :pred :obj . } . | erasure from step 7 | |
| 32 | ... | rule from step 31 applied to steps (28, 29, 30) | {'A': u'<refi_ex#City_Wide>', 'pred': u'<refi_ex#rate_offset>', 'obj': '"0.25"', 'subj': u'<refi_ex#City_Wide_refi>', '_g_L91C13': '{3}'} |
| 33 | :City_Wide_refi :rate_offset 0.25 . | erasure from step 32 | |
| 34 | @forAll :M1, :M2 . { :Fed :rate 4.5 . :M1 :balance 200000; :rate 6.125 . :M2 :cost 3700; :rate_offset 0.25 . } log:implies {:Spreadsheet c:says { ( :M1 :M2 ) :payoff_wait 22 . } . } . | erasure from step 3 | |
| 35 | ... | rule from step 34 applied to steps (14, 15, 27, 33) | {'M1': u'<refi_ex#Sam_mortgage>', 'M2': u'<refi_ex#City_Wide_refi>'} |
| 36 | :Spreadsheet c:says { ( :Sam_mortgage :City_Wide_refi ) :payoff_wait 22 . } . | erasure from step 35 | |
| 37 | @forAll :obj, :pred, :subj, spe:A . { @forSome run:_g11 . run:_g11 log:includes {:subj :pred :obj . } . spe:A :controls_property :pred; :says run:_g11 . } log:implies {:subj :pred :obj . } . | erasure from step 7 | |
| 38 | ... | rule from step 37 applied to steps (2, 4, 36) | {'A': u'<refi_ex#Spreadsheet>', 'pred': u'<refi_ex#payoff_wait>', 'obj': '"22"', 'subj': '?', '_g_L91C13': '{li2 payoff_wait "22"}'} |
| 39 | ( :Sam_mortgage :City_Wide_refi ) :payoff_wait 22 . | erasure from step 38 | |
| 40 | @forAll <refi_ex.n3#M> . { ( :Sam_mortgage <refi_ex.n3#M> ) :payoff_wait [ math:notGreaterThan 24 ] . } log:implies {<refi_ex.n3#M> a :GoodOffer . } . | erasure from step 3 | |
| 41 | ... | rule from step 40 applied to steps (1, 39) | {'M': u'<refi_ex#City_Wide_refi>', '_g_L147C35': '"22"'} |
| 42 | :City_Wide_refi a :GoodOffer . | erasure from step 41 | |
| 43 | ... | parsing <refi_goal.n3> | |
| 44 | @forAll :X . { :X a <refi_ex#GoodOffer> . } log:implies {:X a <refi_ex#GoodOffer> . } . | erasure from step 43 | |
| 45 | :City_Wide_refi a :GoodOffer . | rule from step 44 applied to steps (42,) | {'X': u'<refi_ex#City_Wide_refi>'} |
Conclusion:
@prefix : <refi_ex#> . :City_Wide_refi a :GoodOffer .