The type of tactics in all (procedural) proof assistants is (a variant of) the one introduced in LCF. We discuss why this is inconvenient and we propose a new type for tactics that 1) allows the imple- mentation of more clever tactics; 2) improves the implementation of declarative languages on top of procedural ones; 3) allows for better proof structuring; 4) improves proof automation; 5) allows tactics to rearrange and delay the goals to be proved (e.g. in case of side conditions or PVS subtyping judgements).
A new type for tactics / A. Asperti; W. Ricciotti; E. Tassi; C. Sacerdoti Coen. - ELETTRONICO. - (2009), pp. 22-29. (Intervento presentato al convegno International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS09) tenutosi a Munich, Germany nel August, 21, 2009).
A new type for tactics
ASPERTI, ANDREA;RICCIOTTI, WILMER;TASSI, ENRICO;SACERDOTI COEN, CLAUDIO
2009
Abstract
The type of tactics in all (procedural) proof assistants is (a variant of) the one introduced in LCF. We discuss why this is inconvenient and we propose a new type for tactics that 1) allows the imple- mentation of more clever tactics; 2) improves the implementation of declarative languages on top of procedural ones; 3) allows for better proof structuring; 4) improves proof automation; 5) allows tactics to rearrange and delay the goals to be proved (e.g. in case of side conditions or PVS subtyping judgements).I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.