scientific article; zbMATH DE number 2079034

MaRDI QIDQ4474846zbMATH OpenFDO

Authors Hans de Nivelle

Publication date 21 July 2004

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 910745
• A classification of non-liftable orders for resolution
• scientific article; zbMATH DE number 1761419
• Completeness of resolution revisited
• A-ordered tableaux

Cited in

(7)

• 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
• scientific article; zbMATH DE number 910745 (Why is no real title available?)
• A classification of non-liftable orders for resolution
• An algorithm for the retrieval of unifiers from discrimination trees
• Resolution is cut-free

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4474846)