TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
From MaRDI portal
Publication:4928456
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
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
This page was built for publication: TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
