Even more generic solution construction in Valuation-Based Systems
This work fixes and generalizes an incremental theoretical framework for automated reasoning, relevant to researchers in formal methods and AI.
The paper identifies a counterexample to a theorem in prior work on solution construction in valuation algebras, which are used for automated reasoning, and corrects the theory by generalizing definitions and providing sufficient conditions for algorithms.
Valuation algebras abstract a large number of formalisms for automated reasoning and enable the definition of generic inference procedures. Many of these formalisms provide some notions of solutions. Typical examples are satisfying assignments in constraint systems, models in logics or solutions to linear equation systems. Recently, formal requirements for the presence of solutions and a generic algorithm for solution construction based on the results of a previously executed inference scheme have been proposed in the literature. Unfortunately, the formalization of Pouly and Kohlas relies on a theorem for which we provide a counter example. In spite of that, the mainline of the theory described is correct, although some of the necessary conditions to apply some of the algorithms have to be revised. To fix the theory, we generalize some of their definitions and provide correct sufficient conditions for the algorithms. As a result, we get a more general and corrected version of the already existing theory.