First International Workshop on

Design and Application of Strategies/Tactics in Higher Order Logics
STRATA 2003
Focus on PVS Experiences

Roma, Italy
September 8, 2003
In conjunction with TPHOLs 2003

Workshop Proceedings and Preliminary Agenda are Available Now

Scope of the Conference

There has been a series of workshops on strategies in automated deduction associated with CADE. Much of the emphasis in these workshops has been on proof strategies and heuristic based proof search/planning in first-order automatic theorem proving.

In principle, first-order theorem proving does not require user guidance; in this context, strategies aim at faster proof discovery.

By contrast, theorem proving in higher order logics typically requires interactive user guidance. Higher order logic theorem provers support this style of reasoning by providing the user with a set of basic proof commands. To further support their users:

Strategies in higher order logics are aimed at more efficient interactive proof construction. The first property listed above can interfere with fine control in user strategies, but does allow simple strategies to be relatively powerful. The second property can balance this by enhancing the fine control.

As a result of such differences, the art of strategy writing in PVS and other higher order logic theorem provers is worth studying in its own right. Current knowledge about writing PVS strategies in particular has been limited to folklore, despite the powerful capabilities provided in PVS for implementing user-defined strategies. Thus, for PVS, we wish to distill what is known from successful efforts, move beyond the folklore stage, and spawn more widespread practice of the strategic arts.

User-defined strategies permit special-purpose user interfaces to higher order logic theorem provers to be designed that help liberate developers from dependence on specialists in formal methods and theorem proving. Thus, the expected audience includes users of PVS and other higher order logic theorem provers at all levels, particularly those with an interest in making higher order logic theorem proving both easier for themselves and more accessible to others outside the narrow theorem proving community.

Submissions

Topics for paper submissions cover all aspects of development and use of user-defined strategies or tactics in higher order logic theorem provers. Papers (maximum 20 pages, LNCS style fullpage option) concentrating either on experience with PVS strategies or on comparisons with strategy and tactic development in other theorem proving systems are especially encouraged. Short (3-4 page) position papers suitable for panel presentation are also solicited. An informal proceedings will be published as NASA Conference Proceedings, which will also be made available on line.

Important Dates for Authors

Registration

Participants must register for TPHOLs 2003. There is no additional fee for the workshop.

Organizing Committee

STRATA 2003 is organized by the Naval Research Laboratory (NRL), NASA Langley Research Center (NASA LaRC), and the National Institute of Aerospace (NIA).
Myla Archer, NRL
Ben DiVito, NASA LaRC
César Muñoz, NIA

Program Committee

Myla Archer, Naval Research Laboratory, USA
Ben DiVito, NASA Langley Research Center, USA
Herman Geuvers, University of Nijmegen, Netherlands
Peter Homeier, Department of Defense, USA
John Harrison, Intel, USA
Ralph Jeffords, Naval Research Laboratory, USA
Pertti Kellomaki, Tampere University of Technology, Finland
César Muñoz, National Institute of Aerospace, USA
Sylvan Pinsky, Department of Defense, USA
Natarajan Shankar, SRI International, USA

César A. Muñoz H. : munoz