Beagle – A hierarchic superposition theorem prover

Peter Baumgartner*, Joshua Bax, Uwe Waldmann

*Corresponding author for this work

    Research output: Contribution to journalConference articlepeer-review

    12 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 languageEnglish
    Pages (from-to)367-377
    Number of pages11
    JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume9195
    DOIs
    Publication statusPublished - 2015
    Event25th International Conference on Automated Deduction CADE 2015 - Berlin, Germany
    Duration: 1 Aug 20157 Aug 2015

    Fingerprint

    Dive into the research topics of 'Beagle – A hierarchic superposition theorem prover'. Together they form a unique fingerprint.

    Cite this