scientific article; zbMATH DE number 834569

MaRDI QIDQ4860656zbMATH OpenFDO

Authors Jean Goubault-Larrecq

Publication date 12 January 1998

zbMATH Keywords

automated theorem-provingbinary decision diagramsfalse dependencefirst-order logicskolemization

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

Recommendations

• BDDs -- design, analysis, complexity, and applications.
• Experimental and Efficient Algorithms
• Solving BDD by enumeration: an update
• BDD-based symbolic model checking
• scientific article; zbMATH DE number 1980926
• scientific article; zbMATH DE number 1487864
• Programming Combinations of Deduction and BDD-based Symbolic Calculation
• scientific article; zbMATH DE number 139820

Cited in

(2)

• LCF-Style Propositional Simplification with BDDs and SAT Solvers
• Proving with BDDs and control of information

Describes a project that uses

Uses Software

• ETPS
• REDUCE

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 Q4860656)