SMTtoTPTP -- a converter for theorem proving formats

DOI10.1007/978-3-319-21401-6_19MaRDI QIDQ3454101zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• The TPTP problem library
• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• MPTP 0.1 -- system description

Cites work

• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
• 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

Cited in

(3)

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

Describes a project that uses

Uses Software

• z3
• TPTP
• SMT-LIB

This page was built for publication: SMTtoTPTP -- a converter for theorem proving formats

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