Lines Matching defs:terms
90 higher order logic (HOL) terms to binary decision diagrams (BDDs).
112 using a dynamically extendable global table mapping \HOL{} terms to
150 judgements $(a,\rho,t,b)$, where $a$ is a set of boolean terms
225 way of using these to create BDDs from logical terms. Voss enables
230 applied to terms to optimise them for BDD purposes (e.g.~disjunctive
1190 assumptions containing terms $t_1, \ldots ,t_n$ is denoted by
1460 corresponding to the \Buddy{} BDD operation $bddop$ to terms $t_1$ and $t_2$
1494 Raises \t{BddForallError} if any of the terms in the term list argument
1528 Raises \t{BddExistsError} if any of the terms in the term list argument
1570 if any of the terms in the term list argument
1613 if any of the terms in the term list argument
1693 or if any of the terms $v_1,\ldots,v_i$ are repeated or are not variables
1739 or if any of the terms $v_1,\ldots,v_i$ are repeated or are not variables,
1783 or if any of the terms $v_1,\ldots,v_i$ are repeated or are not variables,
1784 or if any of the terms $v_1',\ldots,v_i'$ are repeated or are not variables
2066 \subsection{Conversion to terms}