Matrix Proof Methods for Modal Logics

Abstract

We preoent mt.trlx proof oyotama for both conott.nt- o.nd varying-domo.in verolono of the llrot-order modallogieo K, K4, D, D4, T, S4 and 86 baHd on modal veroiono of Herbrand'o Theorem opecillcally formulated to oupport efficient automated proof aearch. The oyotema treat the full modal language (no normal-forming) and admit otralghtforward otructure oharln1 lmplementationo. A key feature of our approach Ia the uoe of a opeclalioed unillcatlon algorithm to rellect the condltlono on the acceoolbillty relation for a 1lven lope. The matrix oyotem for one logic dilfero from the matrix oyotem for another only ln the nature of thla unlllcatlon al&orithm. In addition, proof aearch may be interpreted u conotructlng generallaed proof treM in an appropriate tableau- or Hquent-bued proof oyotem. Thil facilitateo the uoe of the matrix oyotema within Interactive environmento.