BDI: A New Decidable First-order Clause Class
Keyword(s):
BDI (Bounded Depth Increase) is a new decidablefirst-order clause class. It strictly includesknown classes such as PVD. The arityof function and predicate symbols as well as theshape of atoms is not restricted in BDI. Insteadthe shape of "cycles" in resolution inferences isrestricted such that the depth of generated clausesmay increase but is still finitely bound.The BDI class is motivated by real world problemswhere function terms are used to represent record structures.We show that the hyper-resolution calculus moduloredundancy 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.
Keyword(s):
2020 ◽
Vol 20
(10)
◽
pp. 1061-1083
Keyword(s):
Keyword(s):