3rd BCS-FACS Northern Formal Methods Workshop (NFM)
BCS-FACS Northern Formal Methods Workshop
14-15 September 1998
The syntax and semantics of a particular tactic language are defined. The language uses lazy evaluation to manage backtracking in the search space. It also uses pattern matching to associate names with formulae that will subsequently be passed as arguments to an inference rule. The result of the inference rule is accompanied by a revision of the association, so that corresponding formulae in the result may be passed as arguments to the next inference rule. The combination of this revision with lazy evaluation raises some problems for efficient implementation.