Isabelle and Refute and Nitpick

Overview

• Based on the well known Isabelle proof assistant
• Uses the automated tactics, blast, metis, auto, etc.
• Strategy schedules ten tactics

TPTP-THF Features

• Uses TPTP2X to convert problem to Isabelle format
• Isabelle file augmented with ML strategy scheduling code
• Different tactics are successful on different types of problems

Refute and Nitpick

• Refute finds models using the refute command
• Nitpick finds models using the nitpick command