Proceedings STRATA 2003. First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics; Focus on PVS experiences

摘要

This report contains the Proceedings of STRATA 2003, the First International Workshop on the Design and Application of Strategies/Tactics in Higher Order Logics. In contrast to the Strategies in Automated Deduction workshop series that is associated with CADE (the International Conference on Automated Deduction), STRATA focuses on theorem proving strategies for higher order logic theorem provers rather than on theorem proving strategies for (primarily) first order logic theorem proving. This first STRATA workshop focuses in particular on PVS experiences. The Proceedings contains both a paper on strategy writing from the PVS developers and a tutorial on strategy writing written by the editors. It also contains a set of papers presented at STRATA 2003 by users of PVS and other higher order logic provers.