TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism

DOI10.1007/978-3-642-38574-2_29zbMath1381.68260OpenAlexW1749440414MaRDI QIDQ4928456

Andrei Paskevich, Jasmin Christian Blanchette

Publication date: 14 June 2013

Published in: Automated Deduction – CADE-24 (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-00825086/file/tff1short.pdf

Mathematics Subject Classification ID

Related Items (17)

An Automation-Friendly Set Theory for the B Method ⋮ A decision procedure for (co)datatypes in SMT solvers ⋮ A Polymorphic Vampire ⋮ A First Class Boolean Sort in First-Order Theorem Proving and TPTP ⋮ Formal Logic Definitions for Interchange Languages ⋮ SMTtoTPTP – A Converter for Theorem Proving Formats ⋮ Morphism axioms ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Unnamed Item ⋮ The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 ⋮ Encoding Monomorphic and Polymorphic Types ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ HOL(y)Hammer: online ATP service for HOL Light ⋮ Superposition with lambdas ⋮ Superposition with lambdas ⋮ GRUNGE: a grand unified ATP challenge ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)

Uses Software

• TPTP
• Why3
• SPASS+T
• HOL Light
• Monotonox

This page was built for publication: TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism