The Connection Method for Non-Monotonic & Autoepistemic Logic

In this paper, first we present a connection method for non-monotonic logic, together with its soundness and completeness proof. Then, we extend this to a proof procedure for autoepistemic logic. In the last section, we also discuss some improvements on the method through structure sharing techniques.