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

*Subject*: Re: [PVS-Help] Tree height*From*: Ahmed Abdeen* <ahamed@cs.indiana.edu>*Date*: Tue, 01 Mar 2005 10:57:05 -0500*CC*: pvs-help@csl.sri.com*In-Reply-To*: <BAY1-F2288094B5AFE31BA667198EF590@phx.gbl>*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <BAY1-F2288094B5AFE31BA667198EF590@phx.gbl>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com*User-Agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.5) Gecko/20041221

Hello, I am new to PVS, and I want to find prove my solution to this puzzle down below. I am able to solve it algebraically, but don't know how to start my proof using PVS. I mean, do I have to write my own lemmas? stratigies? Any help will be appreciated, Ahmed th_G: THEORY BEGIN %%% %%% Solve the problem below and prove your solution in PVS. This will involve %%% building the appropriate PVS theory. %%% % % Taken from _Algebra 1_, Glencoe/McGraw-Hill, New York, New York, 1998 % pg. 411, Problem 56 % % There are 8 houses on McArthur St, all in a row. These houses % are numbered from 1 to 8. % % Allison, whose house number is greater than 2, lives next door % to her best friend, Adrienne. Belinda, whose house number is % greater than 5, lives 2 doors away from her boyfriend, Benito. % Cheri, whose house number is greater than Benito's, lives % three doors away from her piano teacher, Mr. Crawford. Daryl, % whose house number is less than 4, lives 4 doors from his % teammate, Don. Who lives in each house? % %%% %%% %%% %%% PPL: TYPE = {a, b, c, d, e, f, g, h} ADR: TYPE = {i:int | 0 < i & i < 9} H: {fn:[PPL -> ADR] | (forall (x,y:PPL): fn(x) = fn(y) => x = y)} a1: axiom H(a) > 2 a2: axiom H(b) = H(a) + 1 OR H(b) = H(a) - 1 a3: axiom H(c) > 5 a4: axiom H(d) = H(c) + 2 OR H(d) = H(c) - 2 a5: axiom H(h) > H(d) a6: axiom H(e) = H(h) + 3 OR H(e) = H(h) - 3 a7: axiom H(f) < 4 a8: axiom H(g) = H(f) + 4 OR H(g) = H(f) - 4 %% %% l9 is obviously true, but is it easy to prove in PVS? %% l9: lemma forall (k:ADR) : k = 1 or k = 2 or k = 3 or k = 4 or k = 5 or k = 6 or k = 7 or k = 8 %% %% Even if you can't prove it you might need to use it, %% or maybe ASSERT understands it...? %% a9: axiom forall (k:ADR) : k = 1 or k = 2 or k = 3 or k = 4 or k = 5 or k = 6 or k = 7 or k = 8 l10: lemma forall (k:ADR) : (exists (p:PPL): H(p) = k) %% %% Solve the problem %% END th_G

**References**:**[PVS-Help] Tree height***From:*"Thijs Kuijpers" <tjh_kuijpers@hotmail.com>

- Prev by Date:
**[PVS-Help] Re: Tree height** - Next by Date:
**[PVS-Help] Pvs sets types** - Prev by thread:
**[PVS-Help] Re: Tree height** - Next by thread:
**[PVS-Help] PVS Help (fwd)** - Index(es):