Paper Info
Title
Head-Tactics Simplification
Abstract
Abstract: Tactics are commands used to guide goal-directed proofs in interactive proof environments. This paper presents various possible simplifications on tactic expression and provides a justification for these simplifications, based on a precise description of the way tactics operate. In particular, this paper...
Year
DOI
Venue
1997
10.1007/BFb0000460
AMAST
Keywords
Field
DocType
head-tactics simplification
Software tool,Programming language,Computer science,Automated theorem proving,Mathematical proof,User interface,Software development,Proof assistant
Conference
ISBN
Citations 
PageRank 
3-540-63888-1
1
0.38
References 
Authors
7
1
Name
Order
Citations
PageRank
Yves Bertot144240.82