Beagle – A Hierarchic Superposition Prover

Peter Baumgartner 1 Joshua Bax 2 Uwe Waldmann 3, 4
4 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Beagle is an automated theorem prover for first-order logic modulo built-in theories. It implements a refined version of the hierarchic superposition calculus. This system description focuses on Beagle ’s proof procedure, background reasoning facilities, implementation, and experimental results.
Document type :
Conference papers
Liste complète des métadonnées

https://hal.inria.fr/hal-01251377
Contributor : Stephan Merz <>
Submitted on : Wednesday, January 6, 2016 - 10:12:33 AM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM

Links full text

Identifiers

Collections

Citation

Peter Baumgartner, Joshua Bax, Uwe Waldmann. Beagle – A Hierarchic Superposition Prover. 25th International Conference on Automated Deduction (CADE-25), Aug 2015, Berlin, Germany. pp.367-377, ⟨10.1007/978-3-319-21401-6_25⟩. ⟨hal-01251377⟩

Share

Metrics

Record views

172