Beagle – A hierarchic superposition theorem prover

Peter Baumgartner; Joshua Bax; Uwe Waldmann

doi:10.1007/978-3-319-21401-6_25

Beagle – A hierarchic superposition theorem prover

Peter Baumgartner^*
, Joshua Bax
, Uwe Waldmann

^*Corresponding author for this work

Research output: Contribution to journal › Conference article › peer-review

13 Citations (Scopus)

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.

Original language	English
Pages (from-to)	367-377
Number of pages	11
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9195
DOIs	https://doi.org/10.1007/978-3-319-21401-6_25
Publication status	Published - 2015
Event	25th International Conference on Automated Deduction CADE 2015 - Berlin, Germany Duration: 1 Aug 2015 → 7 Aug 2015

Access to Document

10.1007/978-3-319-21401-6_25

Cite this

@article{d905bdc672554062b832de865835757f,

title = "Beagle – A hierarchic superposition theorem prover",

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{\textquoteright}s proof procedure, background reasoning facilities, implementation, and experimental results.",

author = "Peter Baumgartner and Joshua Bax and Uwe Waldmann",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; 25th International Conference on Automated Deduction CADE 2015 ; Conference date: 01-08-2015 Through 07-08-2015",

year = "2015",

doi = "10.1007/978-3-319-21401-6\_25",

language = "English",

volume = "9195",

pages = "367--377",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

publisher = "Springer Verlag",

}

TY - JOUR

T1 - Beagle – A hierarchic superposition theorem prover

AU - Baumgartner, Peter

AU - Bax, Joshua

AU - Waldmann, Uwe

N1 - Publisher Copyright: © Springer International Publishing Switzerland 2015.

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/84984666922

U2 - 10.1007/978-3-319-21401-6_25

DO - 10.1007/978-3-319-21401-6_25

M3 - Conference article

AN - SCOPUS:84984666922

SN - 0302-9743

VL - 9195

SP - 367

EP - 377

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

T2 - 25th International Conference on Automated Deduction CADE 2015

Y2 - 1 August 2015 through 7 August 2015

ER -

Beagle – A hierarchic superposition theorem prover

Abstract

Access to Document

Other files and links

Fingerprint

Cite this