Application of ABLP logic

We can evaluate the soundness of Sam's reasoning using ABLP logic.

@keywords is, of, a.
@prefix : <refi_ex#>.

@prefix c: <speech#>.

:Melissa c:says { :Fed :rate 4.5 }.

A basic relation in this logic is says as in:

Melissa c:says _:something.

Sam actually does not hear directly from Melissa, but rather from a telephone connection:

MelissaByPhone c:says _:something.

Sam takes for granted that when Melissa calls, statements that come over that phone were said by Melissa:

{ MelissaByPhone c:says ?X } => { Melissa c:says ?X }.

That is, the phone connection speaks for Melissa:

MelissaByPhone c:speaks_for Melissa.

Sam wasn't sure whether to take Melissa's word for it that the Fed rate was down to 4.5%, but he does accept that the Wall Street Journal is an accurate source of this information; that is, the WSJ controls the Fed rate:

WSJ c:controls { Fed rate ?R }.

TODO: perhaps elaborate WSJ c:controls { Fed rate ?R }. using quoting

Due to limitations in our reasoner, we'll actually use a more specific version of controls:

WSJ c:controls_property rate.

which means that WSJ controls all statements of the form { ?X rate ?Y }.

Sam didn't read the WSJ himself; Melissa read it to him; i.e. over the phone, Sam heard Melissa quoting the WSJ:

MelissaByPhone c:says {
  [ is c:quoting of (Melissa WSJ ) ] c:says { Fed rate 4.5 }
}.

The City Wide brochure gives rates and fees for refinancing:

Citi_Wide_brochure c:says {
  City_Wide offers City_Wide_refi.
  City_Wide_refi cost 3700; rate_offset 0.25.
}.

Sam got the brochure from the bank, so he knows the bank will stand by what it says, and the bank is a reliable source of rates and transaction costs:

Citi_Wide_brochure c:speaks_for City_Wide.

City_Wide c:controls_property rate_offset, cost.

Like any spreadsheet user, Sam trusts his software to do financial calculations:

Spreadsheet c:controls_property payoff_wait.

@forAll M1, M2 .

{ M1 rate 6.125; balance 200000 .
  Fed rate 4.5.
  M2 rate_offset 0.25; cost 3700 . }
=> { Spreadsheet c:says { (M1 M2) payoff_wait 22 } }.

Sam knows his mortgage rate and balance:

Sam_mortgage rate 6.125; balance 200000 .

His goal is to find an offer that pays off within 2 years:

@prefix math: <http://www.w3.org/2000/10/swap/math#>.

{ (Sam_mortgage ?M) payoff_wait [ math:notGreaterThan 24 ] }
=> { ?M a GoodOffer }.

And indeed, the premises above (available in refi_ex.n3), combined with the speech.n3 encoding of ABLP logic, do entail the conclusion:

City_Wide_refi a GoodOffer.

A mechanically generated proof shows the details of the reasoning.

References