ON THE RELATIVE MERITS OF PATH DISSOLUTION AND THE METHOD OF ANALYTICTABLEAUX

Path dissolution is an inferencing mechanism that generalizes the meth od of analytic tableaux. We present several results demonstrating that tableau deductions can be substantially speeded up with applications of dissolution technology. We also consider the class of formulas on w hich the method of analytic tableaux was first shown to be intractable and prove that, with the application of the ordinary distributive law , standard tableau methods admit linear time proofs for this class.