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

Re: [work] [PVS-Help] Flatten VS Split



I'm not sure what you mean by "& out". When PVS proofs are expressed in
a sequent calculus, the proof rule (flatten) corresponds to the
bottom-up application of either and-left or or-right, i.e.,

A,B,Gamma |- Delta
------------------------ (and-left)
A /\ B, Gamma |- Delta


Gamma |- Delta, A,B
----------------------- (or-right)
Gamma |- Delta, A \/ B 

On the other hand, the proof rule (split) corresponds to the bottom-up
application of either and-right or or-left, i.e.,


Gamma |- A, Delta     Gamma |- B, Delta
-------------------------------------- (and-right)
Gamma |- A /\ B, Delta


A, Gamma |- Delta  B,Gamma |- Delta
----------------------------------- (or-left)
A \/ B, Gamma |- Delta


Cesar



On Thu, 2007-05-10 at 21:36, Ahmed Abdeen* wrote:
> Hello,
> I have a very simple questions. Given the following subgoal:
> 
> {-1}  (p AND r)
>   |-------
> [1]   q
> [2]   r
> 
> Trivially, you could use "& out" on line {-1} which should result in the
> following:
> 
> {-1}  p
> {-2}  r
>   |-------
> [1]   q
> [2]   r
> 
> I belive this require issuing the (split -1) conjunctive command.  However
> that doesn't work. On the other hand, Flatten works fine. Why is that?
> Thank you,
> Ahmed
> 
> 
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace        mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way, Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4