Beagle – A Hierarchic Superposition Theorem Prover

DOI10.1007/978-3-319-21401-6_25zbMath1465.68277OpenAlexW995310127MaRDI QIDQ3454107

Peter Baumgartner, Joshua Bax, Uwe Waldmann

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_25

Mathematics Subject Classification ID

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

Related Items (3)

The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Beagle

Uses Software

• SMT-LIB
• TPTP
• SPASS+T
• z3
• CVC4
• SMTtoTPTP

Cites Work

• Unnamed Item
• Refutational theorem proving for hierarchic first-order theories
• 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
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Hierarchic Superposition with Weak Abstraction
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic

This page was built for publication: Beagle – A Hierarchic Superposition Theorem Prover