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. Copyright © 2007 Inderscience Enterprises Ltd.

Arindama Singh

Singh A

Raut M.K.

Formal logic

Knowledge based systems

Optical resolving power

COMPUTING THEORY

CONSENSUS METHODS

First order logic

FIRST-ORDER FORMULAS

Knowledge base

Knowledge compilation

PARTIAL CORRECTNESS

THEORY PRIME IMPLICATES

Algorithms

Fulltext

Vellore Institute of Technology (VIT) is a private university located in&nbsp;Tamil Nadu, India. Founded in 1984, as Vellore Engineering College, the institution offers 20 undergraduate, 34 postgraduate, four integrated and four research programs. It has campuses in Vellore, Amravati, Bhopal and Chennai.

VIT is one of the top ranked private universities in India according to NIRF, THE and QS Rankings.&nbsp;Govt. of India has recognized&nbsp;VIT, Vellore as an&nbsp;Institution of Eminence. This has allowed VIT to take independent quality initiatives and move up in world ranking.

&nbsp;

&nbsp;

VIT University

An algorithm for computing theory prime implicates in first order logic

International Journal of Information and Communication Technology

Strategische Unternehmensplanung mit Hilfe eines Assumption-based-Truth-Maintenance-Systems (ATMS)

Knowledge compilation techniques are usually applied for prepositional knowledge bases. In this article, an extension of the notion of prime implicants of aknowledge base using first order formulas in Skolem conjunctive normal form is suggested. The method of transversal clauses used earlier for computing prime implicants of a propositional formula in conjuctive normal form is adopted to the first order case via substitutions. Partial correctness of the algorithm is proved. The algorithm is adopted heuristically for computing approximate prime implicants.

International Journal of Computer Mathematics

Prime implicants of first order formulas via transversal clauses

Journal of Logic and Computation

Computation of prime implicants using matrix and paths

Principles of Knowledge Representation and Reasoning

Tractable Databases: How to Make Propositional Unit Resolution Complete through Compilation

Journal of Complexity

Polynomial-time algorithms for generation of prime implicants

Journal	International Journal of Information and Communication Technology
Publisher	Inderscience Enterprises Ltd
ISSN	14666642
Open Access	Yes