Resolution games and non-liftable resolution orderings

DOI10.1007/BFB0022263MaRDI QIDQ4474846zbMATH OpenFDO

Authors Hans de Nivelle

Publication date 21 July 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0022263

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
• A unification of ordering refinements of resolution in classical logic
• 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: Resolution games and non-liftable resolution orderings

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