Hierarchic Superposition with Weak Abstraction
Date
2013
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
Keywords
Keywords: Automated deduction; Background theory; First order logic; Function symbols; Integer arithmetic; Internal operations; Research challenges; Superposition calculus; Abstracting; Automation; Calculations; Theorem proving; Automata theory
Citation
Collections
Source
CADE 2013
Type
Conference paper
Book Title
Entity type
Access Statement
License Rights
Restricted until
2037-12-31