Problem set for first order theorem provers in the TPTP format

Marco B. Caminati; Manfred Kerber; Colin Rowat

Problem set for first order theorem provers in the TPTP format

Marco B. Caminati, Manfred Kerber, Colin Rowat

Research output: Non-textual form › Data set/Database

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).

Original language	English
Media of output	Online
Size	44k
Publication status	Published - 16 Jun 2015

Access to Document

https://github.com/formare/auctions/blob/master/tptp

Cite this

@misc{99825bb7e92c459dabea0896c3a69ff5,

title = "Problem set for first order theorem provers in the TPTP format",

abstract = "In http://afp.sourceforge.net/entries/Vickrey_Clarke_Groves.shtml wedescribe an Isabelle formalization of combinatorial auctions. In thisdirectory you find one axiom file and 17 problem files for first ordertheorem provers in TPTP format, which are first order translations ofsome of the theorems in the Isabelle formalization (labels preserved).",

author = "Caminati, {Marco B.} and Manfred Kerber and Colin Rowat",

year = "2015",

month = jun,

day = "16",

language = "English",

}

TY - ADVS

T1 - Problem set for first order theorem provers in the TPTP format

AU - Caminati, Marco B.

AU - Kerber, Manfred

AU - Rowat, Colin

PY - 2015/6/16

Y1 - 2015/6/16

N2 - In http://afp.sourceforge.net/entries/Vickrey_Clarke_Groves.shtml wedescribe an Isabelle formalization of combinatorial auctions. In thisdirectory you find one axiom file and 17 problem files for first ordertheorem provers in TPTP format, which are first order translations ofsome of the theorems in the Isabelle formalization (labels preserved).

AB - In http://afp.sourceforge.net/entries/Vickrey_Clarke_Groves.shtml wedescribe an Isabelle formalization of combinatorial auctions. In thisdirectory you find one axiom file and 17 problem files for first ordertheorem provers in TPTP format, which are first order translations ofsome of the theorems in the Isabelle formalization (labels preserved).

M3 - Data set/Database

ER -

Problem set for first order theorem provers in the TPTP format

Abstract

Access to Document

Fingerprint

Cite this