LEO II

Overview

• Resolution based higher-order ATP system
• Cooperates with first-order subsystem
• Implemented in OCaml

TPTP-THF Features

• THF0 is the native language for input and output
• Communication with first-order subsystem using TPTP standards
  • TPTP language for formulae
  • SZS ontologies for status
• Debugged using THF problems in the TPTP
• Will merge higher-order and first-order TPTP format proofs

See the LEO II page online