SMTtoTPTP – A Converter for Theorem Proving Formats

DOI10.1007/978-3-319-21401-6_19zbMath1465.68276OpenAlexW1604495270MaRDI QIDQ3454101

Peter Baumgartner

Publication date: 2 December 2015

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

Full work available at URL: https://doi.org/10.1007/978-3-319-21401-6_19

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 ⋮ SMTtoTPTP

Uses Software

• SMT-LIB
• TPTP
• z3

Cites Work

• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• The TPTP Typed First-Order Form with Arithmetic
• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism

This page was built for publication: SMTtoTPTP – A Converter for Theorem Proving Formats