[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs@csl.sri.com*Subject*: Proof assistant needed for non-linear arithmetic*From*: "Ricky W. Butler" <rwb@air58.larc.nasa.gov>*Date*: Mon, 10 Aug 1998 08:33:01 -0400 (EDT)*Reply-to*: R.W.Butler@larc.nasa.gov

One of the more frustrating aspects of using PVS is the machinations one must go through to prove sequents that involve non-linear arithmetic. For example, suppose you are faced with: {-1} n!1 < m!1 |------- {1} n!1 / m!1 < 1 One must scan through dozens of lemmas in the prelude such as both_sides_plus_lt1: LEMMA x + z < y + z IFF x < y both_sides_plus_lt2: LEMMA z + x < z + y IFF x < y both_sides_minus_lt1: LEMMA x - z < y - z IFF x < y both_sides_minus_lt2: LEMMA z - x < z - y IFF y < x both_sides_times_pos_lt1: LEMMA x * pz < y * pz IFF x < y both_sides_times_pos_lt2: LEMMA pz * x < pz * y IFF x < y both_sides_times_neg_lt1: LEMMA x * nz < y * nz IFF y < x both_sides_times_neg_lt2: LEMMA nz * x < nz * y IFF y < x both_sides_div_pos_lt1: LEMMA x/pz < y/pz IFF x < y both_sides_div_pos_lt2: LEMMA pz/px < pz/py IFF py < px both_sides_div_pos_lt3: LEMMA nz/px < nz/py IFF px < py both_sides_div_neg_lt1: LEMMA x/nz < y/nz IFF y < x both_sides_div_neg_lt2: LEMMA pz/nx < pz/ny IFF ny < nx both_sides_div_neg_lt3: LEMMA nz/nx < nz/ny IFF nx < ny till you recognize one that might help, say Rule? (LEMMA "both_sides_div_pos_lt1") Applying both_sides_div_pos_lt1 this simplifies to: foo : {-1} (FORALL (pz: posreal, x: real, y: real): x / pz < y / pz IFF x < y) [-2] n!1 < m!1 |------- [1] n!1 / m!1 < 1 then you have to carefully instantiate the beast because (INST?) rarely guesses the right ones: Rule? (INST -1 "m!1" "n!1" "m!1") Instantiating the top quantifier in -1 with the terms: m!1, n!1, m!1, this simplifies to: foo : {-1} n!1 / m!1 < m!1 / m!1 IFF n!1 < m!1 [-2] n!1 < m!1 |------- [1] n!1 / m!1 < 1 then of course (FLATTEN) (ASSERT) prove it. Now wouldn't it be nice if there were a proof assistant running on top of PVS that you could use as follows: {-1} n!1 < m!1 |------- {1} n!1 / m!1 < 1 Rule? (DIVIDE_BOTH_SIDES_BY "m!1" -1) The proof assistant would then look through the prelude, find the appropriate LEMMA and instantiate it for you. The proof assistant would accept commands that manipulate formulas in the way one does in an algebra class, such as: MULTIPLY_BOTH_SIDES_BY DIVIDE_BOTH_SIDES_BY ... It seems to me that this could be developed by graduate students as a class project or a Master's thesis.? There are many places where a proof assistant could help. For example, Suppose you have an IMPORTED relation (e.g. (total_order?[T]) ): A_theory[N: nat, <= : (total_order?[T])] Inside this theory, the decision procedures can NOT take advantage of the fact that this relation is a total order, so formulas such as a <= b b <= c |----- a <= c must be proved by manually instantiating the formulas that are in the relations theory in the prelude: once again a big pain! eq: pred[[T, T]] = (LAMBDA x, y: x = y) reflexive?(R): bool = FORALL x: R(x, x) irreflexive?(R): bool = FORALL x: NOT R(x, x) symmetric?(R): bool = FORALL x, y: R(x, y) IMPLIES R(y, x) antisymmetric?(R): bool = FORALL x, y: R(x, y) & R(y, x) => x = y connected?(R): bool = FORALL x, y: x /= y IMPLIES R(x, y) OR R(y, x) transitive?(R): bool = FORALL x, y, z: R(x, y) & R(y, z) => R(x, z) A command like (TRANSITIVE "a <= b") could figure out the appropriate instantiations to establish that a <= b. Does the PVS community think this would be helpful? practical? Rick Butler

**Follow-Ups**:**Re: Proof assistant needed for non-linear arithmetic***From:*Harald Ruess <ruess@csl.sri.com>

- Prev by Date:
**new PVS papers available** - Next by Date:
**Re: Proof assistant needed for non-linear arithmetic** - Prev by thread:
**new PVS papers available** - Next by thread:
**Re: Proof assistant needed for non-linear arithmetic** - Index(es):