Showing cs.LOShow all
2 papers · 1 filter
cs.LO2023
A Mathematical Benchmark for Inductive Theorem Provers
Thibault Gauthier, Chad E. Brown, Mikolas Janota +1
We present a benchmark of 29687 problems derived from the On-Line Encyclopedia of Integer Sequences (OEIS). Each problem expresses the equivalence of two syntactically different pr…
cs.LO2014
Matching concepts across HOL libraries
Thibault Gauthier, Cezary Kaliszyk
Many proof assistant libraries contain formalizations of the same mathematical concepts. The concepts are often introduced (defined) in different ways, but the properties that they…