Computing Theory Prime Implicates in Modal Logic

2015/12/28 by Raut, Manoj K.
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1512.08366

Abstract

The algorithm to compute theory prime implicates, a generalization of prime implicates, in propositional logic has been suggested in \citeMarquis. In this paper we have extended that algorithm to compute theory prime implicates of a knowledge base X with respect to another knowledge base \Box Y using \citeBienvenu, where Y is a propositional knowledge base and X\models Y, in modal system T and we have also proved its correctness. We have also proved that it is an equivalence preserving knowledge compilation and the size of theory prime implicates of X with respect to \Box Y is less than the size of the prime implicates of X∪\Box Y.

Related

• An Algorithm for Computing Prime Implicates in Modal Logic Using\n Resolution
• An Incremental Knowledge Compilation in First Order Logic
• Solving Quantified Modal Logic Problems by Translation to Classical Logics
• A Generic Framework for Implicate Generation Modulo Theories
• Base-extension Semantics for Modal Logic