Publication:4474846
From MaRDI portal
zbMath1044.03506MaRDI QIDQ4474846
Publication date: 21 July 2004
03B35: Mechanization of proofs and logical operations
Related Items
An algorithm for the retrieval of unifiers from discrimination trees, A classification of non-liftable orders for resolution, Resolution is cut-free, Completeness of hyper-resolution via the semantics of disjunctive logic programs, Deciding the \(E^+\)-class by an a posteriori, liftable order, Deciding the guarded fragments by resolution