Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.2 9/18/84; site lsuc.UUCP
Path: utzoo!lsuc!dave
From: dave@lsuc.UUCP (David Sherman)
Newsgroups: net.lang.prolog
Subject: Re: Degrees of provability - Re: "assert" considered harmful?
Message-ID: <1284@lsuc.UUCP>
Date: Sun, 6-Jul-86 22:56:27 EDT
Article-I.D.: lsuc.1284
Posted: Sun Jul  6 22:56:27 1986
Date-Received: Sun, 6-Jul-86 23:55:30 EDT
References: <1754@utai.UUCP> <269@ubc-cs.UUCP> <1245@lsuc.UUCP> <506@ccird1.UUCP>
Reply-To: dave@lsuc.UUCP (David Sherman)
Organization: Law Society of Upper Canada, Toronto
Lines: 54
Summary: this will be a planning system, not a real-time system

In article <506@ccird1.UUCP> rb@ccird1.UUCP (Rex Ballard) writes:
>The issue of dynamic binding is not new.  Theoretically, to be "provably
>correct" only the absolute facts should ever be bound, but for practical
>reasons, this is rarely the case.  The process of reproving a theorem
>in which the axioms are rarely changed can be quite costly.
>
>The point here is that it is necessary to know when the axioms have been
>changed, a mechanism that prolog seems to lack.  When using assert, you
>are effectively saying that these rules are valid for "the current set
>of facts".

What I'm planning to do is use something like Kowalski's "holds"
formulism, to state that something either stated or derived as
true at a given time is still true at a later time unless we know
otherwise, and have a number (from zero up) of ways for each
predicate to possibly become untrue.  For example, an assertion
about sharesoutstanding(Corp, Class, Numshares) can become untrue
in at least three ways: if new shares are issued; if shares are
redeemed; and if the corporation is wound up.

>Using your "controls" example, if someone makes the transition from
>"not controls" to "controls" after you have made your assertions,
>and inductions have been made before the reassertions have been made,
>then the solution is provably wrong.  Suppose your algorithm for
>"controls" depends on purchases of stock, suppose also that there
>are certain tax benefits or penalties that go into effect at the
>time the person takes control.  You might retract/assert at the
>end of each day, but between the time someone took control, and
>the time you re-asserted, the man made 2 million in capital gains
>profits.  Or conversely he make the money at 10:00 AM, and takes
>control at 1:00 PM.  Again you've missed the benefits/penalties.

I should point out that I'm not designing a "real-time" system
here which will chug along each day and tell you what the current
state of the world is.  My system will be an analysis tool, which
can be used either to review past facts or to consider proposed
facts.  So the granularity of the events which are relevant
is determined by the person specifying the facts, and of course
the program has to adjust its conception of what is true at
each point in time at which anything happens.

>To answer your question, yes it should be "legally correct" rather
>than "mathematically correct" before lawyers use it.  This may mean
>that you MUST use retract/assert.  The law is not always logical.

Canadian income tax law is highly logical, which is why I'm using
Prolog.  I think I may need to use retract/assert, but I don't
think the reason is that the law is not logical.

Dave Sherman
The Law Society of Upper Canada
Toronto
-- 
{ ihnp4!utzoo  pesnta  utcs  hcr  decvax!utcsri  } !lsuc!dave