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

Practicals: Programming with Tacticals



Announcement: Programming with Tacticals in PVS 
-----------------------------------------------
Practicals 2.1, a package for programming strategies in PVS with high
level tacticals, is available for PVS 3.1. Practicals enhances the PVS
proof language (IF, REPEAT, THEN, TRY, ...) with tacticals for looping
(WHILE, FOR), matching terms (MATCH), matching proof contexts (SCREEN),
raising proof failures (THROW), catching proof failures (CATCH), and
more ...

The package and the documentation are available at:
http://research.nianet.org/fm-at-nia/Practicals

We welcome comments and user reports,

Florent Kirchner
fkirchner@nianet.org