Employing path dissolution to shorten tableaux proofs

摘要

Path dissolution is an inferencing mechanism that generalizes the method of analytic tableaux. The main result presented is that every non-trivial step in any tableau proof can be speeded up with the application of dissolution techniques.