Problem set for first order theorem provers in the TPTP format

Research output: Non-textual formData set/Database

Colleges, School and Institutes

Abstract

In http://afp.sourceforge.net/entries/Vickrey_Clarke_Groves.shtml 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).

Details

Original languageEnglish
Media of outputOnline
Size44k
Publication statusPublished - 16 Jun 2015