Meta-reasoning: An incremental compilation approach

An incremental compilation approach to meta-reasoning is presented together with a method to update dynamically changing knowledge bases. The compilation process translates meta-level specification of facts and hypotheses into sentences of clausal logic. It then incrementally computes inconsistent sets of instances of hypotheses and records potential crucial literals. The extra information computed during compilation enables the theorem prover to avoid redundant computations and to efficiently update the compiled knowledge. Whenever a new fact is learned the effects of the fact are computed incrementally, without recompiling. A relationship between potential crucial literals and Reiter and de Kleer´s prime implicants shows that this approach may be useful in incrementally computing and maintaining the prime implicants, as well