Computing Theory Prime Implicates in Modal Logic

TL;DR

This paper extends an algorithm to compute theory prime implicates in modal logic, specifically in system T, demonstrating correctness and showing that these implicates are smaller than prime implicates of combined knowledge bases.

Contribution

It generalizes existing propositional algorithms to modal logic, providing a correct, size-efficient method for computing theory prime implicates relative to another knowledge base.

Findings

Algorithm extension to modal logic system T

Proof of correctness for the extended algorithm

Theory prime implicates are smaller than prime implicates of combined knowledge bases

Abstract

The algorithm to compute theory prime implicates, a generalization of prime implicates, in propositional logic has been suggested in \cite{Marquis}. 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 \cite{Bienvenu}, where $Y$ is a propositional knowledge base and $X\models Y$, in modal system $\mathcal{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\cup\Box Y$.