A classification of non-liftable orders for resolution

DOI10.1007/3-540-63104-6_33zbMath1430.03038OpenAlexW2126000649MaRDI QIDQ5234716

Hans de Nivelle

Publication date: 1 October 2019

Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-63104-6_33

zbMATH Keywords

automated theorem provingresolution ruleempty clauseliftability propertynegative clause

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• On a bound for the complexity of terms in the resolution method
• Resolution methods for the decision problem
• Resolution Strategies as Decision Procedures
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A classification of non-liftable orders for resolution