KK: a theorem prover for K

摘要

Nonclassical propositional logics play an increasing role in computer science. They are used in model checking, verification, and knowledge representation. Traditional decision procedures for these logics are based on semantic tableaux [6,7,1], SAT-based methods [4], or translation into classical logic [10]. In this system abstract we overview the system KK that implements the tableau method and the less traditional inverse method for propositional modal logic K.