Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation

DOI10.1007/11814771_15zbMath1222.68375OpenAlexW1515554225MaRDI QIDQ3613406

Allen van Gelder, Geoff Sutcliffe

Publication date: 12 March 2009

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11814771_15

Mathematics Subject Classification ID

Related Items

The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 ⋮ The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 ⋮ THF0 – The Core of the TPTP Language for Higher-Order Logic ⋮ HOL(y)Hammer: online ATP service for HOL Light ⋮ Progress in the Development of Automated Theorem Proving for Higher-Order Logic ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)

Uses Software

• Coq
• TPTP
• Elf
• ALGOL 60