Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  Refutational Theorem Proving for Hierarchic First-Order Theories

Bachmair, L., Ganzinger, H., & Waldmann, U. (1994). Refutational Theorem Proving for Hierarchic First-Order Theories. Applicable Algebra in Engineering, Communication and Computing (AAECC), 5(3/4), 193-212. doi:10.1007/BF01190829.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-AD9C-E Versions-Permalink: https://hdl.handle.net/21.11116/0000-000E-3459-4
Genre: Zeitschriftenartikel

Externe Referenzen

einblenden:
ausblenden:
externe Referenz:
https://rdcu.be/dttWV (Verlagsversion)
Beschreibung:
-
OA-Status:
Keine Angabe

Urheber

einblenden:
ausblenden:
 Urheber:
Bachmair, Leo1, Autor           
Ganzinger, Harald1, Autor           
Waldmann, Uwe1, 2, Autor                 
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: We extend previous results on theorem proving for first-order clauses with
equality to hierarchic first-order theories. Semantically such theories are
confined to conservative extensions of the base models. It is shown that
superposition together with variable abstraction and constraint refutation is
refutationally complete for theories that are sufficiently complete with
respect to simple instances. For the proof we introduce a concept of
approximation between theorem proving systems, which makes it possible to
reduce the problem to the known case of (flat) first-order theories. These
results allow the modular combination of a superposition-based theorem prover
with an arbitrary refutational prover for the primitive base theory, whose
axiomatic representation in some logic may remain hidden. Furthermore they can
be used to eliminate existentially quantified predicate symbols from certain
second-order formulae.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2010-03-121994
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: Expertenbegutachtung
 Identifikatoren: eDoc: 519899
Anderer: Local-ID: C1256104005ECAFC-DBD34269BBD3C1BFC125614C004A7057-BachmairGanzingerWaldmann-94-aaecc
DOI: 10.1007/BF01190829
BibTex Citekey: Bachmair_AAECC94
 Art des Abschluß: -

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Applicable Algebra in Engineering, Communication and Computing (AAECC)
  Kurztitel : AAECC
Genre der Quelle: Zeitschrift
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 5 (3/4) Artikelnummer: - Start- / Endseite: 193 - 212 Identifikator: ISSN: 0938-1287