ETR-NAT : CONTEXT

ETR-NAT is a context.
Concerning translation between expansion proofs and natural
deduction proofs.

TPS documentation homepage


ETR-NAT : MODULE

ETR-NAT is a module.

It is loaded.
Defines functions needed for conversion from expansion tree proofs
to natural deduction proofs and vice versa.

NEEDED-MODULES MATING-TRANSFORM TACTICS

FILES ETR-NAT-MACROS DIY NAT-ETR SYMSIMP SYMSIMP2

TPS documentation homepage


ETR-NAT : REVIEW-SUBJECT

ETR-NAT is a subject.
Pertaining to the translation from expansion tree proofs to
natural deduction proofs.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage