Skip to main content
PRL Project

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.