BTab2DNF computes for a B-ternary function table a propositional logic formula in DNF according to [Muka72]. The result is returned as a set of set of literals.

compute all functions xNew & f1(x) | !xNew & f0(x)) for f0,f1 of the given set

compute all DC2-functions over the given set

compute all DC3-functions over the given set

compute all DC4-functions over the given set

compute all functions ParITE(xNew,f1(x),f0(x)) for f0,f1 of the given set

compute all functions SeqITE(xNew,f1(x),f0(x)) for f0,f1 of the given set

DNF2Str converts a DNF given as set of sets of literals to a string.

compute the DC4 decomposition of a monotone function

evaluate a ternary logic formula with a variable assignment rho

compute a firing tree of a ternary function

compute the cofactors of a given function

compute all hazards of a given ternary function; the hazards are returned as a set of pairs (b,x) such that the function has a logic 1-hazard at x if b is TRUE, the function has a logic 0-hazard at x if b is FALSE, and f has a function hazard at x if b is BOT.

MTab2DNF computes for a monotone ternary function table a propositional logic formula in DNF. The result is returned as a set of set of literals.

MTab2MukaDNF computes for a monotone ternary function table a propositional logic formula of the form Φ1 ∨ ⊥∧¬Φ0 where Φ1 and Φ0 are in DNF. Hence, the function returns a pair (Φ1,Φ0) where both Φ1 and Φ0 are sets of sets of literals.

given disjoint primes prime0 and prime1 as generated by function MkStablePrimes, this function generates a stable function with the same boolean core

generate the maximal hazard-free function for a given function

This function modifies the prime implicants prime0 and prime1 of a ternary function so that the primes represent a stable function with the same boolean core.

compute all total monotonic extensions of a partial ternary function

This function parses a string to a ternary logic formula

compute the spectrum of the given monotone function, i.e., the set of minimal input vectors where f(x)=0 or f(x)=1 holds, and the set of maximal input vectors where f(x)=⊥ holds.

print a firing table in html format

print a function table in html format

print a function table in LaTeX format

print a function table in ASCII format

TTab2DNF computes for a ternary function table a propositional logic formula in DNF. The result is returned as a set of set of literals.

convert a ternary logic expression to an explicit map

check equivalence of two ternary logic expressions

teaching tool function

check validity of two ternary logic expressions (only makes sense for formulas with equality)

compute the set of variables that occur in a ternary logic expression

compare all ternary functions of a given set an draw a Hasse diagram in graphviz format where the function printTable is used to print each one

infimum of two values

compute infimum and supremum of a set of values

infimum on the components of two vectors

check whether a given function is B-ternary

check commutativity of a ternary function with two arguments

check whether a given function is has a DC1 decomposition by x[n-1]

check whether a given function is has a DC2 decomposition by x[n-1]

check whether a given function is has a DC3 decomposition by x[n-1]

check whether a given ternary function has no logic hazards

check monotonicity of a (totally defined) ternary function

check whether a given function is sequential; if so, it returns a sequential decomposition

check whether a given function is stable

check whether two vectors are joinable, i.e., have an upper bound

this function defines the order of the semi-lattice

extending the order to vectors of the same length