Grunge: A grand unified ATP challenge

Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Scopus citations


This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalisms are in higher-order logic (with and without type variables) and first-order logic (possi-bly with types, and possibly with type variables). The resultant problem sets allow us to run automated theorem provers that support different logical formalisms on corresponding problems, and compare their performances. This also results in a new “grand unified” large theory benchmark that emulates the ITP/ATP hammer setting, where systems and metasystems can use multiple formalisms in complementary ways, and jointly learn from the accumulated knowledge.

Original languageEnglish (US)
Title of host publicationAutomated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings
EditorsPascal Fontaine
Number of pages19
ISBN (Print)9783030294359
StatePublished - 2019
Event27th International Conference on Automated Deduction, CADE 2019 - Natal, Brazil
Duration: Aug 27 2019Aug 30 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11716 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference27th International Conference on Automated Deduction, CADE 2019


  • First-order logic
  • Higher-order logic
  • Many-sorted logic
  • Theorem proving

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Grunge: A grand unified ATP challenge'. Together they form a unique fingerprint.

Cite this