English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 DetailsSummary
  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

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-C374-D Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0026-A5A5-5
Genre: Conference Paper
Latex : {BDI}: A New Decidable First-order Clause Class

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Lamotte-Schubert, Manuel1, Author           
Weidenbach, Christoph1, Author           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: -
 Abstract: 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

show
hide
Language(s): eng - English
 Dates: 2013
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: BibTex Citekey: Lamotte-SchubertWeidenbach13
URN: http://www.easychair.org/publications/?page=1079461175
 Degree: -

Event

show
hide
Title: 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Place of Event: Stellenbosch, South Africa
Start-/End Date: 2013-12-12 - 2013-12-17

Legal Case

show

Project information

show

Source 1

show
hide
Title: LPAR-19
  Abbreviation : LPAR 2013
  Subtitle : 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, December 12-17, 2013, Stellenbosch, South Africa, Short papers proceedings
Source Genre: Proceedings
 Creator(s):
McMillan, Ken1, Editor
Middeldorp, Aart1, Editor
Sutcliffe, Geoff1, Editor
Voronkov, Andrei1, Editor           
Affiliations:
1 External Organizations, ou_persistent22            
Publ. Info: Manchester, UK : EasyChair
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 62 - 74 Identifier: -

Source 2

show
hide
Title: EasyChair Proceedings in Computing
  Abbreviation : EPiC
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 26 Sequence Number: - Start / End Page: - Identifier: ISSN: 2040-557X