An Incremental Knowledge Compilation in First Order Logic

2011/10/31 by Raut, Manoj K.
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1110.6738

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 π(X)∪ C. The correctness of the algorithm is also proved.

Related

• Computing Theory Prime Implicates in Modal Logic
• CoAPI: An Efficient Two-Phase Algorithm Using Core-Guided Over-Approximate Cover for Prime Compilation of Non-Clausal Formulae
• A Canonical Partition of the Primes of Logic Functions
• An Optimal Heuristic for Sum of All Prime Numbers Logic for Large Inputs using RAPTOR
• An Algorithm for Computing Prime Implicates in Modal Logic Using\n Resolution