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

DOI10.1007/11814771_15MaRDI QIDQ3613406zbMATH OpenOpenAlexFDO

Authors 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

Recommendations

• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• scientific article; zbMATH DE number 5850137
• THF0 – The Core of the TPTP Language for Higher-Order Logic
• scientific article; zbMATH DE number 4053062
• The TPTP typed first-order form with arithmetic

Cited in

(10)

• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Using the TPTP Language for Writing Derivations and Finite Interpretations
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• scientific article; zbMATH DE number 5850137 (Why is no real title available?)
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• THF0 – The Core of the TPTP Language for Higher-Order Logic
• The TPTP typed first-order form with arithmetic
• HOL(y)Hammer: online ATP service for HOL Light
• The logic languages of the TPTP world
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)

Describes a project that uses

Uses Software

• ALGOL 60
• Elf
• TPTP
• Coq

This page was built for publication: Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3613406)