Tactic Trees in eXene
by Roderick Moten
The use of tactics for interactive theorem proving is widespread. Systems based on tactics typically employ an auxiliary data structure, such as a stack or a tee, to help manage such tasks as the composition of validations and selection of subgoals.
This report describes a logic-independent implementation of a tactic trees and its X-windows interface for structure-oriented editing. The system is implemented in Standard ML of New Jersey using CML and eXene.
This is joint work with Timothy Griffin.