[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] begginer's question
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!