A prime implicates-based formulae forgetting

This paper proposes a novel operation called formulae forgetting by extending literals forgetting, which is popular in reasoning about knowledge, to ignore or hide those irrelevant formulae for given tasks. First, prime implicates are employed to capture variables forgetting and literals forgetting; and literals forgetting could be taken as particular cases of formulae forgetting. Clauses forgetting are then introduced to build a uniform framework for variables forgetting via prime implicates. Based on this uniform framework, a formula could be forgotten by using clauses forgetting on the resolution closure of all prime implicates of the formula. As an extension of variables forgetting, formulae forgetting might be more flexible in reasoning about knowledge since formulae are the most general forms of knowledge. In technology, our operator for formulae forgetting is based on prime implicates and clauses forgetting while variables forgetting is simply based on variables assignment. In addition, our operator could keep the syntax-independency which is an important semantic feature in representing knowledge.