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

Re: Judgements and TCCs for numerals


We just talked this over at SRI.  The problem is that PVS
automatically supplies some judgements for numerals (e.g., it knows
that 2 is a posnat, and is even) and is thereby able to suppress TCCs
that would otherwise be generated, but there is no facility for the
user to extend this collection of judgements for generic numerals.

We are thinking of adding a facility to PVS 3.0 that will optionally
check whether TCCs are evaluable and will suppress those that can be
discharged by the PVS evaluator.  This will solve your problem but I'm
afraid you'll have to wait for the new version of PVS.  Our goal is to
release it in June.