Proceedings chapter
Open access

Sigma Decision Diagrams

Publication date2009

Encoding and rewriting of large set of terms is very useful in a number of domains, such as model checking and theorem proving. The challenge of encoding and normalizing several billions of terms requires efficient ways of representing and manipulating them. Term Graph Rewriting is a well-known technique to share common sub-terms and thus to save both memory and processing time. However, this does not always fit well to the operational framework since it destroys the original structure and replaces it by a new one. This paper introduces a new kind of Decision Diagrams (DD), especially designed to handle set of terms in an efficient way. Based on the Set Decision Diagrams(SDD), an evolution of the well-known Binary Decision Diagrams(BDD), we propose the Sigma Decision Diagrams (ΣDD), a new approach to perform Term Rewriting on a set of terms in order to compute the image of that set efficiently.

  • Term Rewriting
  • Set Decision Diagrams
  • Σ Decision Diagrams
  • Set of terms
Citation (ISO format)
BUCHS, Didier, HOSTETTLER, Steve Patrick. Sigma Decision Diagrams. In: TERMGRAPH 2009 : Preliminary proceedings of the 5th International Workshop on Computing with Terms and Graphs. [s.l.] : [s.n.], 2009.
Main files (1)
Proceedings chapter
  • PID : unige:12331

Technical informations

Creation11/05/2010 1:55:00 PM
First validation11/05/2010 1:55:00 PM
Update time03/14/2023 4:08:22 PM
Status update03/14/2023 4:08:22 PM
Last indexation02/12/2024 7:27:33 PM
All rights reserved by Archive ouverte UNIGE and the University of GenevaunigeBlack