Pith. sign in

REVIEW 1 cited by

Propositional Independence - Formula-Variable Independence and Forgetting

Not yet reviewed by Pith; the record is open.

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1106.4578 v1 pith:LIB6FUPB submitted 2011-06-22 cs.AI

classification cs.AI
keywords independencerelevantreasoningbasecomputationallyconsiderforgettingform
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
read the original abstract

Independence -- the study of what is relevant to a given problem of reasoning -- has received an increasing attention from the AI community. In this paper, we consider two basic forms of independence, namely, a syntactic one and a semantic one. We show features and drawbacks of them. In particular, while the syntactic form of independence is computationally easy to check, there are cases in which things that intuitively are not relevant are not recognized as such. We also consider the problem of forgetting, i.e., distilling from a knowledge base only the part that is relevant to the set of queries constructed from a subset of the alphabet. While such process is computationally hard, it allows for a simplification of subsequent reasoning, and can thus be viewed as a form of compilation: once the relevant part of a knowledge base has been extracted, all reasoning tasks to be performed can be simplified.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Knowledge Compilation for Boolean Functional Synthesis

    cs.LO 2019-08 conditional novelty 8.0 of 10

    A new normal form, SynNNF, guarantees polynomial-time Skolem function synthesis and existential quantification, subsumes wDNNF/DNNF/ROBDD, and supports a CNF-to-SynNNF compiler that solves benchmarks beyond current tools.

Pith tools