Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 DetailsÜbersicht
  BDI: A New Decidable First-order Clause Class

Lamotte-Schubert, M., & Weidenbach, C. (2013). BDI: A New Decidable First-order Clause Class. In K. McMillan, A. Middeldorp, G. Sutcliffe, & A. Voronkov (Eds.), LPAR-19 (pp. 62-74). Manchester, UK: EasyChair.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-C374-D Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-0026-A5A5-5
Genre: Konferenzbeitrag
Latex : {BDI}: A New Decidable First-order Clause Class

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Lamotte-Schubert, Manuel1, Autor           
Weidenbach, Christoph1, Autor           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: BDI (Bounded Depth Increase) is a new decidable first-order clause class. It strictly includes known classes such as PVD. The arity of function and predicate symbols as well as the shape of atoms is not restricted in BDI. Instead the shape of "cycles" in resolution inferences is restricted such that the depth of generated clauses may increase but is still finitely bound. The BDI class is motivated by real world problems where function terms are used to represent record structures. We show that the hyper-resolution calculus modulo redundancy elimination terminates on BDI clause sets. Employing this result to the ordered resolution calculus, we can also prove termination of ordered resolution on BDI, yielding a more efficient decision procedure.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2013
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: BibTex Citekey: Lamotte-SchubertWeidenbach13
URN: http://www.easychair.org/publications/?page=1079461175
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Veranstaltungsort: Stellenbosch, South Africa
Start-/Enddatum: 2013-12-12 - 2013-12-17

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: LPAR-19
  Kurztitel : LPAR 2013
  Untertitel : 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, December 12-17, 2013, Stellenbosch, South Africa, Short papers proceedings
Genre der Quelle: Konferenzband
 Urheber:
McMillan, Ken1, Herausgeber
Middeldorp, Aart1, Herausgeber
Sutcliffe, Geoff1, Herausgeber
Voronkov, Andrei1, Herausgeber           
Affiliations:
1 External Organizations, ou_persistent22            
Ort, Verlag, Ausgabe: Manchester, UK : EasyChair
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 62 - 74 Identifikator: -

Quelle 2

einblenden:
ausblenden:
Titel: EasyChair Proceedings in Computing
  Kurztitel : EPiC
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 26 Artikelnummer: - Start- / Endseite: - Identifikator: ISSN: 2040-557X