Sorry, I don't have a good reference for it.
There exists a clausal tableau system for KD4 that has space requriements on the order of N log N. [Nguyen, 1999]
System KD4 is the system K4 plus the axiom D [Lp>Mp]
© Copyright 2000, by John Halleck, All Rights Reserved.
This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/kd4.html
This page was last modified on October 2nd, 2005