Problem set for first order theorem provers in the TPTP format

Research output: Non-textual formData set/Database

Colleges, School and Institutes


In we
describe an Isabelle formalization of combinatorial auctions. In this
directory you find one axiom file and 17 problem files for first order
theorem provers in TPTP format, which are first order translations of
some of the theorems in the Isabelle formalization (labels preserved).


Original languageEnglish
Media of outputOnline
Publication statusPublished - 16 Jun 2015