Zero, successor and equality in BDDs
type: Item
instance of: scholarly article
title: Zero, successor and equality in BDDs
zbMATH Open document ID: 1064.03009
author: Bahareh Badban
author: Jaco van de Pol
published in: Annals of Pure and Applied Logic
publication date: 2005-04-21T00:00:00Z
full work available at URL: https://ir.cwi.nl/pub/10606
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 2160243
zbMATH Keywords: binary decision diagrams
zbMATH Keywords: fragment of first-order logic
zbMATH Keywords: quantifier-free logic with zero, successor and equality
zbMATH Keywords: satisfiability
describes a project that uses: Uppaal
describes a project that uses: PVS
describes a project that uses: mCRL
MaRDI profile type: Publication
OpenAlex ID: W2039160606
Wikidata QID: Q62047502
cites work: Solvable cases of the decision problem
cites work: Q4818802
cites work: Q4551157
cites work: Q4806211
cites work: Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
cites work: Termination of rewriting
cites work: Q4809070
cites work: Q2767014
cites work: Q4945220
cites work: Fast Decision Procedures Based on Congruence Closure
cites work: Q4818813
cites work: Q4804887
cites work: Q4808733
cites work: An algorithm for reasoning about equality
cites work: Q4427902
cites work: Q4804898
cites work: Q4847000
cites work: A rewriting approach to binary decision diagrams
DOI: 10.1016/J.APAL.2004.10.005
description: scientific article; zbMATH DE number 2160243