Analysis of a new reduction calculus for the satisfiability problem

MaRDI QIDQ3434492zbMATH OpenFDO

Authors S. Noureddine

Publication date 2 May 2007

zbMATH Keywords

algorithm for hybrid reduction/resolutionreduction calculus for propositional formulassatisfiability

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• A satisfiability tester for non-clausal propositional calculus
• On O(Tlog T) reduction from RAM computations to satisfiability
• An efficient and flexible approach to resolution proof reduction
• scientific article; zbMATH DE number 1098495
• scientific article; zbMATH DE number 956865

Cited in

(3)

• Algorithm for PP-reduction a PC formula to the clause form
• Experiments with reduction finding
• Reversed resolution in reducing general satisfiability problem

This page was built for publication: Analysis of a new reduction calculus for the satisfiability problem

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