# * Tactic Trees in eXene *

## by Roderick Moten

1992-1993

Abstract

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.