Title: An algorithm for computing theory prime implicates in first order logic

Authors: Arindama Singh, Manoj K. Raut

Addresses: Department of Mathematics, Indian Institute of Technology Madras, Chennai-600036, India. ' School of Computing Sciences, Vellore Institute of Technology, Vellore-632014, India

Abstract: An algorithm based on consensus method to compute the set of prime implicates of a quantifier free first order formula X was presented in an earlier work. In this paper the notion of prime implicates is extended to theory prime implicates in the first order case. We provide an algorithm to compute the theory prime implicates of a knowledge base X with respect to another knowledge base Y where both X and Y are assumed to be unquantified first order formulas. The partial correctness of the algorithm is proved.

Keywords: first order logic; resolution; knowledge compilation; theory prime implicates; ICT.

DOI: 10.1504/IJICT.2007.013273

International Journal of Information and Communication Technology, 2007 Vol.1 No.1, pp.4 - 13

Available online: 19 Apr 2007 *

Full-text access for editors Access for subscribers Purchase this article Comment on this article