TPS-GOOD1

Overview

• Peter Andrews' higher-order theorem proving system
• Mating search, expansion trees, higher-order pre-unification
• Flags affect behaviour, a set of flags is a TPS mode
• Strategy schedules 53 49 modes

TPTP-THF Features

• Uses TPTP2X to convert problem to TPS format
• Strategy scheduling controlled externally by a perl script
• Different modes are successful on different types of problems