2Laurent Catach. TABLEAUX: A general theorem prover for modal logics[J] 1991,Journal of Automated Reasoning(4):489~510
3David A. Plaisted. A decision procedure for combinations of propositional temporal logic and other specialized theories[J] 1986,Journal of Automated Reasoning(2):171~190