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.

Tactic Trees in eXene

by Roderick Moten 1992-1993

by Roderick Moten
1992-1993