First-order logic in a logical language invites undecidable complexity of inference irrespective of the language’s restrictions. First-order decision diagrams (FODDs) and generalized first-order decision diagrams (GFODDs) represent decision-theoretic planning, including “numerical values and numerical generalizations of existential and universal quantification.” This paper explains the complexity involved in FODD and GFODD reasoning.
The authors describe GFODD representation using 12 theorems, ten definitions, two corollaries, one lemma, and one claim. They define the representation of inputs for FODD and GFODD computational problems using evaluation, satisfiability, value, equivalence, and edge removal. Further, they develop FODD results using fewer arguments to provide easy interpretation of the results, stronger results irrespective of the model size, and separate proofs for FODDs and GFODDs.
The authors prove the complexity of reasoning with FODD evaluation, satisfiability, equivalence, edge removal, and value as nondeterministic polynomial-time (NP) complete, NP-complete, Π(2,p)-complete, Π(2,p)-complete, and Σ(2,p)-complete, respectively. They also prove the complexity of reasoning with GFODD evaluation and satisfiability using min-k-alternating and max-k-alternating as Π(k,p)-complete and Σ(k,p)-complete, and Σ(k+1,p)-complete and Σ(k,p)-complete, respectively. The authors find equal complexity for min-k-alternating and max-k-alternating GFODD equivalence. They prove the equivalence problem for min-GFODD is Π(2,p)-complete, GFODD edge removal for diagrams is Π(k+1,p)-complete, and GFODD value for diagrams is Σ(k+1,p)-complete.
In the results, evaluation over finite structures spans the polynomial hierarchy, satisfiability follows a different pattern, and equivalence depends only on quantifier depth. The authors further assert that “equivalence is one level higher in the hierarchy than evaluation and satisfiability.” The authors claim GFODDs can generalize the function-free portion of first-order logic, which makes this paper an interesting read for those who are working in this area.