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

Dear Dr. Cesar,
Thank you for your response. Here is a link to a set of rules in a sentential/predicate logic system that I would like to implement in PVS:
http://people.umass.edu/gmhwww/110/text/!RULES_2006.pdf

If you could help me with implementing one strategy for any of those rules in the above system that would be much appreciated.
Sincerely,
Ahmed

On 5/11/07, Cesar A. Munoz <munoz@nianet.org> wrote:
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