Zero, successor and equality in BDDs

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

Bahareh Badban, Jaco van de Pol

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

satisfiabilitybinary decision diagramsfragment of first-order logicquantifier-free logic with zero, successor and equality

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (3)

Generalizing DPLL and satisfiability for equalities ⋮ A Term Rewriting Technique for Decision Graphs ⋮ 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

This page was built for publication: Zero, successor and equality in BDDs