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

Re: [work] Re: [PVS-Help] Proof By Contradition - How to do thisin PVS?



A simple clarification:
  
P1 AND P2 => C1

is equivalent to

P1 AND P2 AND NOT C1 => FALSE.

Indeed, PVS is based on classical higher-order logic (see Chapter 7 of
"The Formal Semantics of PVS" for the precise set of rules). Therefore,
formulas can be freely moved from the antecedent to the consequent, and
viceversa, by negating them. Empty in the antecedent means TRUE, while
empty in the consequent means FALSE.

The PVS logic system cannot be customized to an arbitrary set of rules.
However, particular deductive rules can be implemented as strategies.

A proof by contradiction in PVS is not different from a direct proof.
Assume that you have

    [-1]  P1
    [-2]  P2
    |-----------
    [+1]   C1

If you type the proof command (case "NOT C1"), you get two sequents

[-1] NOT C1
[-2] P1
[-3] P2
|------------
[+1] C1

and

[-2] P1
[-3] P2
|------------
[+1] NOT C1
[+2] C1


The first sequent will be automatically transformed by PVS into the
original one and the second sequent will be automatically proven by PVS
as it's an instance of the excluded middle.

Cesar

On Mon, 2007-04-23 at 14:36, Ahmed Abdeen* wrote:
> The answer to this question has lead me to have these following questions:
> What logic system is PVS based upon? If you have a logic system with well
> defined derivation rules, can you customize PVS to understand those derivation
> rules of that system? The system inlcudes rules such as
> "modus tollens" and "modus ponens".
> Thank you,
> Ahmed
> 
> 
> On Mon, 23 Apr 2007, Ricky W. Butler wrote:
> 
> > Mark,
> >     Consider the sequent is
> >
> >    [-1]  P1
> >    [-2]  P2
> >    |-----------
> >     [+1]   C1
> >
> > This is equivalent to
> >
> >        P1 AND P2 => C1
> >
> > which is equivalent to
> >
> >        P1 AND P2 AND NOT C1 => TRUE
> >
> > If you can create a contradiction among the premises,
> > the sequent is proved.
> >
> > So in effect proof by contradiction is handled automatically.
> > You have to get used to the idea that you can move a premise
> > from + to - side or vice versa if you negate it.  In fact PVS always
> > does this with an expression that begins with NOT.
> >
> > You could split the proof into two pieces by introducing a
> > case expression, e.g.
> >
> >     (case "NOT C1")
> >
> > This will produce two subgoals, which might help you
> > think this through.
> >
> > R
> >
> > At 06:40 PM 4/20/2007, Janney, Mark-P26816 wrote:
> >
> > >I'm trying to reconstruct a manual proof that used proof by contradition,
> > >i.e assume the negation of your thesis and then derive a contradition.
> > >
> > >It's not clear to me how to accomplish this in the PVS prover.  Any
> > >suggestions would be most welcome.
> > >
> > >Thanks - Mark Janney
> >
> > Ricky W. Butler
> > NASA Langley Research Center
> > Hampton, VA  23681-2199
> > R.W.Butler@larc.nasa.gov
> > http://shemesh.larc.nasa.gov/fm/
> > phone: 757-864-6198
> > fax: 757-864-4234
-- 
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