English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  Hierarchic Superposition Revisited

Baumgartner, P., & Waldmann, U. (2019). Hierarchic Superposition Revisited. Retrieved from http://arxiv.org/abs/1904.03776.

Item is

Basic

show hide
Item Permalink: http://hdl.handle.net/21.11116/0000-0004-03C0-F Version Permalink: http://hdl.handle.net/21.11116/0000-0004-03C1-E
Genre: Paper

Files

show Files
hide Files
:
arXiv:1904.03776.pdf (Preprint), 500KB
Name:
arXiv:1904.03776.pdf
Description:
File downloaded from arXiv at 2019-07-10 13:12
Visibility:
Public
MIME-Type / Checksum:
application/pdf / [MD5]
Technical Metadata:
Copyright Date:
-
Copyright Info:
-

Locators

show

Creators

show
hide
 Creators:
Baumgartner, Peter1, Author              
Waldmann, Uwe2, Author              
Affiliations:
1External Organizations, ou_persistent22              
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: Computer Science, Logic in Computer Science, cs.LO
 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 in the presence of free function symbols ranging into a background theory sort. The hierarchic superposition calculus of Bachmair, Ganzinger, and Waldmann already supports such symbols, but, as we demonstrate, not optimally. This paper aims to rectify the situation by introducing a novel form of clause abstraction, a core component in the hierarchic superposition calculus for transforming clauses into a form needed for internal operation. We argue for the benefits of the resulting calculus and provide two new completeness results: one for the fragment where all background-sorted terms are ground and another one for a special case of linear (integer or rational) arithmetic as a background theory.

Details

show
hide
Language(s): eng - English
 Dates: 2019-04-072019-04-162019
 Publication Status: Published online
 Pages: 48 p.
 Publishing info: -
 Table of Contents: -
 Rev. Method: -
 Identifiers: arXiv: 1904.03776
URI: http://arxiv.org/abs/1904.03776
BibTex Citekey: Baumgartner_arXIv1904.03776
 Degree: -

Event

show

Legal Case

show

Project information

show

Source

show