BDI: a new decidable clause class

Manuel Lamotte-Schubert 1 Christoph Weidenbach 2, 1
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
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 so 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.
Document type :
Journal articles
Liste complète des métadonnées

https://hal.inria.fr/hal-01098084
Contributor : Stephan Merz <>
Submitted on : Monday, December 22, 2014 - 5:17:38 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM

Identifiers

  • HAL Id : hal-01098084, version 1

Collections

Citation

Manuel Lamotte-Schubert, Christoph Weidenbach. BDI: a new decidable clause class. Journal of Logic and Computation, Oxford University Press (OUP), 2014, 24 (6), pp.28. ⟨http://logcom.oxfordjournals.org/content/early/2014/12/08/logcom.exu074⟩. ⟨hal-01098084⟩

Share

Metrics

Record views

268