An Incremental Knowledge Compilation in First Order Logic

TL;DR

This paper introduces an incremental algorithm for updating the set of prime implicates in a dynamic first-order logic knowledge base, ensuring correctness when new clauses are added.

Contribution

It presents the first incremental algorithm for computing prime implicates in first-order logic, extending previous static methods.

Findings

Algorithm correctly updates prime implicates with new clauses.

Proof of correctness for the incremental approach.

Applicable to dynamic knowledge bases in first-order logic.

Abstract

An algorithm to compute the set of prime implicates of a quantifier-free clausal formula X in first order logic had been presented in earlier work. As the knowledge base X is dynamic, new clauses are added to the old knowledge base. In this paper an incremental algorithm is presented to compute the prime implicates of X and a clause C from $\pi(X)\cup C$. The correctness of the algorithm is also proved.