Description

A WYSIWYG editor for the higher-order logic format THF of the TPTP library [1] with support for local and remote theorem provers.

Editor Features

• Edit THF and WYSIWYG presentation simultaneously
• Syntax highlighting
• Representation of a problem's structure
• File browser

Theorem Prover Features

• Supports the remote provers of the TPTP infrastructure [1]
• Supports execution of local provers and ships with state-of-the-art provers
• Support for multiple conjectures
• Exclude axioms/conjectures from problems by toggling them on/off

[1] http://www.tptp.org