Hierarchic Superposition with Weak Abstraction

Date

Authors

Baumgartner, Peter
Waldmann, Uwe

Journal Title

Journal ISSN

Volume Title

Publisher

Springer

Abstract

Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arithmetic. A major unsolved research challenge is to design theorem provers that are "reasonably complete" even

Description

Citation

Source

CADE 2013

Book Title

Entity type

Access Statement

License Rights

Restricted until

2037-12-31