Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
The complexity of reasoning with FODD and GFODD
Hescott B., Khardon R. Artificial Intelligence229 1-32,2015.Type:Article
Date Reviewed: Apr 26 2016

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.

Reviewer:  Lalit Saxena Review #: CR144355 (1607-0520)
Bookmark and Share
 
Complexity Hierarchies (F.1.3 ... )
 
 
Deduction And Theorem Proving (I.2.3 )
 
 
Knowledge Representation Formalisms And Methods (I.2.4 )
 
 
Logics And Meanings Of Programs (F.3 )
 
Would you recommend this review?
yes
no
Other reviews under "Complexity Hierarchies": Date
Bounded queries to SAT and the Boolean hierarchy
Beigel R. (ed) Theoretical Computer Science 84(2): 199-223, 1991. Type: Article
Oct 1 1992
Minimal degrees for polynomial reducibilities
Homer S. (ed) Journal of the ACM 34(2): 480-491, 1987. Type: Article
Nov 1 1987
Unambiguity of circuits
Lange K. Theoretical Computer Science 107(1): 77-94, 1993. Type: Article
May 1 1994
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy