It is a well-known fact that some form of factoring is necessary for completeness of paramodulation-based calculi of general first-order clauses. In this paper we give an overview...
Abstract. leanK is a "lean", i.e., extremely compact, Prolog implementation of a free variable tableau calculus for propositional modal logics. leanK 2.0 includes additio...