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

[PVS-Help] begginer's question



Hi,
I'm studying pvs through "A Tutorial Introduction to PVS" by  Crow, Owre, Rushby, Shankar and Srivas.  They gave an example I can't prove. It is "decisions", section 4.3. I'm stuck in arith. What do I do after "(then (skolem!)(ground))" ?
Thanks for any tip!