# Decision making in ABLP logic
# =============================
# 
# .. header::
#    This is part of `A Model of Authority in the Web <story.html>`_.
# 
# Before we look in detail at Web protocols, let's look at an ordinary
# decision based on input from various sources of information:
# 
#   Sam has been considering refinancing his house for a while when his
#   wife, Melissa, calls on the phone and says "The Fed rate is down to
#   4.5%; now is the time!"
# 
#   "Wow. Really? Are you sure?" says Sam.
# 
#   "Yes, I read it in this morning's Wall Street Journal," she says.
# 
#   Sam gets out a spreadsheet to figure out if that meets his goal of
#   paying off the transaction cost within two years.  A brochure from
#   his bank, Citi Wide, shows they charge about $3,700 in transaction
#   fees and they lend money at a quarter point (0.25%) over the Fed
#   rate.  The balance of his mortage is $200K and his present rate is
#   6.125%, which makes the monthly payment $1,215. At 4.75%, the
#   payment would be $1,043, a savings of $172 per month, which makes up
#   for the $3,700 in fees in 22 months.
# 
#   So yes, now is the time.
# 
# Application of ABLP logic
# -------------------------
# 
# We can evaluate the soundness of Sam's reasoning using ABLP logic.
# 
# .. sidebar::
#    Webizing ABLP logic
# 
#    We borrow relationships such as `says` from ABLP and give them URIs
#    in the Semantic Web using using Notation3.  The primer [N3P]_
#    explains basic statements and abbreviating URIs with namespaces.
#    The default prefix is bound to ``<refi_ex#>`` and we use
#    ``@keywords`` to elide colons as explained in [N3Spec]_::

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

#    The `c:` prefix is mnemonic for *communication*::

     @prefix c: <speech#>.
   
#    To express ABLP modal statements such as ::

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

#    we use Notation3 formula terms as explained in [N3Logic]_.
# 
# .. examples
# 
# 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 }.
# 
# .. output
# 
# That is, the phone connection `speaks for` Melissa::

  MelissaByPhone c:speaks_for Melissa.

# .. examples
# 
# 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*
# 
# .. output
# 
# 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 }.
# 
# .. sidebar::
#    Functions and operators in Notation3
# 
#    Read ``[ is c:quoting of (Melissa WSJ ) ]`` as `quoting(Melissa,
#    WSJ)` following the Notation3 convention of writing `op(arg1,
#    arg2)` as **[is op of (arg1 arg2)]** where **op** is an
#    ``owl:FunctionalProperty``. This applies to `arg1 op arg2` as well;
#    in the ABLP papers, `quoting(A, B)` is written `A|B`.
# 
# 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
# <refi_ex.n3>`_), combined with the `speech.n3 <speech.n3>`_ encoding
# of ABLP logic, do entail the conclusion:
# 
#   City_Wide_refi a GoodOffer.
# 
# A `mechanically generated proof <refi-pf.html>`_ shows the details of
# the reasoning.
# 
# 
# References
# ----------
# 
# .. [N3P] `Primer: Getting into RDF & Semantic Web using N3`__
#    Berners-Lee, Hawke, and Connolly WWW2003 (Budapest) tutorial 
# 
# __ http://www.w3.org/2000/10/swap/Primer
# 
# .. [N3Spec] `Notation3 (N3): A readable RDF syntax`__
#    Berners-Lee work in progress 2000-2006
# 
# __ http://www.w3.org/DesignIssues/Notation3.html
# 
# .. [N3Logic] `N3Logic: A Logical Framework for the World Wide Web`__
#    Berners-Lee, Tim, Connolly, Dan, Kagal, Lalana, Hendler, Jim, and
#    Schraf, Yosi Journal of Theory and Practice of Logic Programming
#    (TPLP), Special Issue on Logic Programming and the Web, 2008
# 
# __ http://arxiv.org/abs/0711.1533 
# 
# .. [TTL] `Turtle - Terse RDF Triple Language`__
#     David Beckett and Tim Berners-Lee 14 January 2008
#     http://www.w3.org/TeamSubmission/2008/SUBM-turtle-20080114/
# 
# __ http://www.w3.org/TeamSubmission/2008/SUBM-turtle-20080114/
# 
#