Previous  Up  Next

Module Term_logic.Rbc


module Rbc: Constructor
Logical constructors with syntactic simplification based on Reduced Boolean Circuits.

Reduced Boolean Circuits are defined here:

Per Bjesse, Arne Boralv. DAG-Aware Circuit Compression for Formal Verification. ICCAD: 42-49, 2004.

val negation : Term.term -> Term.term
Negation of a term.
val conjunction : Term.term -> Term.term -> Term.term
Conjunction of two terms.
val disjunction : Term.term -> Term.term -> Term.term
Disjunction of two terms.
val equivalence : Term.term -> Term.term -> Term.term
Logical equivalence of two (Boolean) terms.
val difference : Term.term -> Term.term -> Term.term
Logical dis-equivalence of two (Boolean) terms.
val implication : Term.term -> Term.term -> Term.term
Implication of two terms.
val conditional : Term.term -> Term.term -> Term.term -> Term.term
Conditional expression: Boolean condition, and Boolean alternatives.
val equality : Term.term -> Term.term -> Term.term
Equality of two non-Boolean terms.
val ite : Term.term -> Term.term -> Term.term -> Term.term
Conditional expression: Boolean condition, non-Boolean alternatives.
Hosted by the SourceForge.net Logo* web site.
*Other names and brands may be claimed as the property of others.