BDI: A New Decidable First-order Clause Class

Lamotte-Schubert, Manuel; Weidenbach, Christoph

Item

ITEM ACTIONSEXPORT

Add to Basket

Please note that a newer version of this item is available:
https://pure.mpg.de/pubman/item/item_2095134_6

DetailsSummary

Released

Conference Paper

BDI: A New Decidable First-order Clause Class

MPS-Authors

/persons/resource/persons44881

Lamotte-Schubert, Manuel
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons45719

Weidenbach, Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

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.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0024-C374-D

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.