An Incremental Knowledge Compilation in First Order Logic
Logic in Computer Science
2011-11-17 v2
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 . The correctness of the algorithm is also proved.
Keywords
Cite
@article{arxiv.1110.6738,
title = {An Incremental Knowledge Compilation in First Order Logic},
author = {Manoj K. Raut},
journal= {arXiv preprint arXiv:1110.6738},
year = {2011}
}