Zero, successor and equality in BDDs

DOI10.1016/j.apal.2004.10.005zbMath1064.03009WikidataQ62047502 ScholiaQ62047502MaRDI QIDQ1772774

Jaco van de Pol, Bahareh Badban

Publication date: 21 April 2005

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://ir.cwi.nl/pub/10606

zbMATH Keywords

satisfiability; binary decision diagrams; fragment of first-order logic; quantifier-free logic with zero, successor and equality

Mathematics Subject Classification ID

03B25: Decidability of theories and sets of sentences

03B35: Mechanization of proofs and logical operations

68Q42: Grammars and rewriting systems

03B20: Subsystems of classical logic (including intuitionistic logic)

Related Items

A Term Rewriting Technique for Decision Graphs, Generalizing DPLL and satisfiability for equalities, An efficient relational deductive system for propositional non-classical logics

Uses Software

• PVS
• Uppaal
• mCRL

Cites Work

• Termination of rewriting
• A rewriting approach to binary decision diagrams
• Solvable cases of the decision problem
• Fast Decision Procedures Based on Congruence Closure
• An algorithm for reasoning about equality
• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item