## PropLogic Module

This module implements functions for dealing with propositional logic like computing truth tables, evaluating formulas by truth assignments, computing canonical CNF and DNF and the sequent calculus.

### Types

 Type Description BddCallExpr is used by function MkBDDCallTable and abbreviates calls of a BDD function. There are three kinds of BddCallExpr: BddArg(bddAdr) is simply an address of a Bdd as argument BddCallApply(fName,cL,y) is a call of BDD algorithm fName with arguments cL and result y BddCallNode(x,c1,c0,y) represents two calls c1 and c0 embedded in a BDD node with root x which yields then BDD node y. type for sequent calculus proof trees; each node has either one, two or no successor nodes and consists of two sets of formulas. Moreover, each node is uniquely identified by an index. Leaf nodes are further separated into valid ones (NodeTrue) and invalid ones (NodeFalse).

### Functions and values

 Function or value Description  BDDAlgorithmsTool qscoll  Full Usage: BDDAlgorithmsTool qscoll Parameters: qscoll : NameValueCollection This cgi-function provides various BDD algorithms. qscoll : NameValueCollection  BDDReorderingTool qscoll  Full Usage: BDDReorderingTool qscoll Parameters: qscoll : NameValueCollection This cgi-function is used to first construct the BDD of a formula with a specified variable ordering and the converts it to the BDD of another specified variable ordering by a sequence of swap operations. Afterwards, it applies sifting to optimize the second ordering. qscoll : NameValueCollection  CanonicalCNFofBDD bddAdr  Full Usage: CanonicalCNFofBDD bddAdr Parameters: bddAdr : BddAdr Returns: Set> This function derives a formula in conjunctive normal form from a BDD. The CNF is given as a set of sets of literals with an obvious meaning. bddAdr : BddAdr Returns: Set>  CanonicalCNFofTruthTable atomL phi  Full Usage: CanonicalCNFofTruthTable atomL phi Parameters: atomL : BoolExpr list phi : BoolExpr Returns: Set> Compute canonical CNF by truth table, where the maxterms are ordered as given by atomL. atomL : BoolExpr list phi : BoolExpr Returns: Set>  CanonicalDNFofBDD bddAdr  Full Usage: CanonicalDNFofBDD bddAdr Parameters: bddAdr : BddAdr Returns: Set> This function derives a formula in disjunctive normal form from a BDD. The DNF is given as a set of sets of literals with an obvious meaning. bddAdr : BddAdr Returns: Set>  CanonicalDNFofTruthTable atomL phi  Full Usage: CanonicalDNFofTruthTable atomL phi Parameters: atomL : BoolExpr list phi : BoolExpr Returns: Set> Compute canonical DNF by truth table, where the minterms are ordered as given by atomL. atomL : BoolExpr list phi : BoolExpr Returns: Set>  CanonicalRMNF phi  Full Usage: CanonicalRMNF phi Parameters: phi : BoolExpr Returns: Set> Compute Reed-Muller normal form directly from a formula, where the RMNF is encoded as sets of sets of variables where false is {}, true is {{}}, x is {{x}}, and !x is {{},{x}}. We define a n-ary XOR as XOR{} := false; XOR{m} := m; and otherwise the xor of the elements. Similarly, we have AND{} := true, AND{x} := x, etc. phi : BoolExpr Returns: Set>  CanonicalSNFofBDD bddAdr  Full Usage: CanonicalSNFofBDD bddAdr Parameters: bddAdr : BddAdr Returns: BoolExpr This function derives a formula in Shannon normal form from a BDD. Of course, the formula can have an exponential size also for a small BDD. bddAdr : BddAdr Returns: BoolExpr  ComputeAllAssignments atomL  Full Usage: ComputeAllAssignments atomL Parameters: atomL : BoolExpr list Returns: Map list Enumerate all assignments for the given list of atoms; an assignment is thereby a map that maps an atom of the given boolean expression to a boolean value. atomL : BoolExpr list Returns: Map list  ComputeFDDs atomL rmfL  Full Usage: ComputeFDDs atomL rmfL Parameters: atomL : BoolExpr list rmfL : Set> list Returns: int list * Map<(BoolExpr * int * int), int> ComputeFDDs computes the functional decision diagrams of Reed-Muller normal forms as computed by CanonicalRMNF following the variable order given by argument atomL (as always for decision diagrams, the leftmost atom in atomL is closest to the leaf nodes). The FDDs are stored in a map that maps a node address i to a triple (x,i1,i0) where x is the variable of the node, and i1,i0 are the addresses of the positive and negative subFDDs. The result is a pair (iL,m) where iL is the list of addresses of the FDDs and m is the map described before. atomL : BoolExpr list rmfL : Set> list Returns: int list * Map<(BoolExpr * int * int), int>  ComputeZDDs atomL bddL  Full Usage: ComputeZDDs atomL bddL Parameters: atomL : BoolExpr list bddL : BddAdr list Returns: int list * Map<(BoolExpr * int * int), int> ComputeZDDs computes for a given list of BDDs the corresponding ZDDs where the variable ordering atomL is followed (should be the one used by the BDDs, i.e., as always for decision diagrams, the leftmost atom in atomL is closest to the leaf nodes). Analogously to the FDDs, the ZDDs are stored in a map that maps a node address i to a triple (x,i1,i0) where x is the variable of the node, and i1,i0 are the addresses of the positive and negative subZDDs. The result is a pair (iL,m) where iL is the list of addresses of the ZDDs and m is the map described before. atomL : BoolExpr list bddL : BddAdr list Returns: int list * Map<(BoolExpr * int * int), int>  DualRails inputSet posName negName phi  Full Usage: DualRails inputSet posName negName phi Parameters: inputSet : Set posName : string -> string negName : string -> string phi : BoolExpr Returns: BoolExpr * BoolExpr Dual-rail encoding of a formula: If a variable x belongs to inputSet, it will be encoded as (x,!x) instead of (x+,x-). inputSet : Set posName : string -> string negName : string -> string phi : BoolExpr Returns: BoolExpr * BoolExpr  EvalBoolExpr rho e  Full Usage: EvalBoolExpr rho e Parameters: rho : Map e : BoolExpr Returns: bool Evaluate a formula with respect to a given assignment of the atoms. It is expected that the given assignment is complete, i.e., that every atom of the given boolean expression is mapped to either true or false. rho : Map e : BoolExpr Returns: bool  FDD2Dot outStr writeLF (iL, fddMap)  Full Usage: FDD2Dot outStr writeLF (iL, fddMap) Parameters: outStr : TextWriter writeLF : bool iL : int list fddMap : Map<(BoolExpr * int * int), int> Write a FDD as generated by function ComputeFDD to a DotFile. outStr : TextWriter writeLF : bool iL : int list fddMap : Map<(BoolExpr * int * int), int>  KarnaughVeitch atomL  Full Usage: KarnaughVeitch atomL Parameters: atomL : BoolExpr list Returns: Map[] * Map[] Computes a KV diagram for a given list of atoms. The KV diagram is given as two arrays (col,row) where col and row denote the column and row vectors, respectively, i.e., col[i] and row[j] denote the assignments to the variables in entry (i,j) of the KV diagram, and their union is therefore the assignment to be evaluated there. atomL : BoolExpr list Returns: Map[] * Map[]  LinearClauseForm phi  Full Usage: LinearClauseForm phi Parameters: phi : BoolExpr Returns: BoolExpr * ((BoolExpr * BoolExpr) * Set>) list Generate linear clause forms for a given formula phi. The result is a pair (v,l) where v is the variable that finally abbreviates phi, and l is a list of pairs ((v,t),cl) where (v,t) represents an abbreviation v=t and cl is its corresponding clause set. phi : BoolExpr Returns: BoolExpr * ((BoolExpr * BoolExpr) * Set>) list  LogicMinimizationTool qscoll  Full Usage: LogicMinimizationTool qscoll Parameters: qscoll : NameValueCollection This cgi-function is used for logic minimization using KV diagrams, the Quine/McCluskey table, or symbolic logic minimization. qscoll : NameValueCollection  MkBDDCallTable vComp call  Full Usage: MkBDDCallTable vComp call Parameters: vComp : AtomIndex option call : BddCallExpr Returns: Map This function explains the recursive calls of a BDD function like Apply. The function expects a call to such a BDD function as explained with type BddCallExpr. In case of Compose, the optional argument vComp must contain the BDD index of the variable that should be replaced in the BDD. The result is a table that maps a BddCallExpr to a list of such that explains the computations. vComp : AtomIndex option call : BddCallExpr Returns: Map  MkCanonicalCNF atomL cnf  Full Usage: MkCanonicalCNF atomL cnf Parameters: atomL : BoolExpr list cnf : Set> Returns: BoolExpr Construct a CNF formula of a set of sets representation (clause set), where the literals in the cubes are ordered as given by atomL. atomL : BoolExpr list cnf : Set> Returns: BoolExpr  MkCanonicalDNF atomL dnf  Full Usage: MkCanonicalDNF atomL dnf Parameters: atomL : BoolExpr list dnf : Set> Returns: BoolExpr Construct a DNF formula of a set of sets representation, where the literals in the maxterms are ordered as given by atomL. atomL : BoolExpr list dnf : Set> Returns: BoolExpr  MkPrimImplicantBDD phi  Full Usage: MkPrimImplicantBDD phi Parameters: phi : BoolExpr Returns: BoolExpr list list * BddAdr * BddAdr phi : BoolExpr Returns: BoolExpr list list * BddAdr * BddAdr  PartialEval rho e  Full Usage: PartialEval rho e Parameters: rho : Map e : BoolExpr Returns: BoolExpr Partial evaluation of a formula wrt. a partial variable assignment: Since the given assignment rho may not map every atom of the boolean expression to a boolean value, the result is just another boolean formula where the mapped atoms are replaced by constants and where simplifications were applied to propagate these constants. rho : Map e : BoolExpr Returns: BoolExpr  PrintKarnaughVeitch atomL (col, row) care phi  Full Usage: PrintKarnaughVeitch atomL (col, row) care phi Parameters: atomL : BoolExpr list col : seq> row : seq> care : BoolExpr phi : BoolExpr Print a KV diagram as constructed by KarnaughVeitch as a html table. atomL : BoolExpr list col : seq> row : seq> care : BoolExpr phi : BoolExpr  PrintTruthTable atomL formulaL  Full Usage: PrintTruthTable atomL formulaL Parameters: atomL : BoolExpr list formulaL : seq Print the truth tables for the given functions as a html table. atomL : BoolExpr list formulaL : seq  PropLogicTool qscoll  Full Usage: PropLogicTool qscoll Parameters: qscoll : NameValueCollection PropLogicTool is the function to be called from the web page qscoll : NameValueCollection  QuineCube2BitvecStr atomL (idx, arg3)  Full Usage: QuineCube2BitvecStr atomL (idx, arg3) Parameters: atomL : BoolExpr list idx : Set<'a> arg2 : Set * Set Returns: string Convert a cube (idx,(pos,neg)) as used in the Quine table to a string. The index set idx is written as a set of integers {i1,...,iN} and the cube (pos,neg) itself is written as a bitvector with * whenever there is a don't care. atomL : BoolExpr list idx : Set<'a> arg2 : Set * Set Returns: string  QuineCube2Minterm atomL (idx, arg3)  Full Usage: QuineCube2Minterm atomL (idx, arg3) Parameters: atomL : BoolExpr list idx : 'a arg2 : Set * Set Returns: BoolExpr Convert a cube (idx,(pos,neg)) as used in the Quine table to a boolean expression where the literals occur as specified by the variable order atomL. atomL : BoolExpr list idx : 'a arg2 : Set * Set Returns: BoolExpr  QuineMcCluskeyMinimalDNF atomL care phi  Full Usage: QuineMcCluskeyMinimalDNF atomL care phi Parameters: atomL : BoolExpr list care : BoolExpr phi : BoolExpr Returns: (Set * (Set * Set)) list list list * (BoolExpr * (Set * (Set * Set))) list * BoolExpr * Set> * Set The following function computes minimal DNFs for a given formula phi with a care set care, where the ordering of atoms atomL is respected. The function applies first the Quine method QuineTable to compute all cubes (implicants) of care->phi, and extracts then the prime cubes with function QuineTablePrimeImplicants where each prime cube is associated with a new boolean variable PI[i]. After this, it generates a formula coverPhi in CNF over the variables PI[i] such that coverPhi has a disjunct for each model of care&phi and that contains all PI[i] that cover that model. The formula coverPhi is then converted to DNF (in sets of sets representation) so that minimal DNFs for phi wrt. care can be derived. The function finally returns a tuple (qt,primeCubes,coverPhi,dnfCover,minDNFs) with: qt is the Quine table as generated by function QuineTable. primeCubes is a list of pairs (PI[i],pc[i]) where pi is a variable associated with prime cube pc[i]. coverPhi is the cover formula using variables PI[i] in CNF. dnfCover is the set of set representation of coverPhi. minDNFs is the list of minimal DNFs of phi wrt. care set care. atomL : BoolExpr list care : BoolExpr phi : BoolExpr Returns: (Set * (Set * Set)) list list list * (BoolExpr * (Set * (Set * Set))) list * BoolExpr * Set> * Set  QuineTable atomL phi  Full Usage: QuineTable atomL phi Parameters: atomL : BoolExpr list phi : BoolExpr Returns: (Set * (Set * Set)) list list list Compute the Quine table: The function expects a formula phi and its variable order order atomL. It computes the Quine table that contains all implicants of phi as a list of list of lists [I0;...;In] where each Ik is the list of list of implicants of order k, i.e., where k variables are don't cares, hence, I0 are all full models of phi. Each Ik=[Lk0;...;Lkj] is partitioned into levels Lki according to the number of atoms made true (zero in Lk0 up to j in Lkj]. Each Lki is finally a list of cubes, where a cube (idx,(pos,neg)) is given by the sets of atoms (pos,neg) made true and false by the cube, respectively. The index idx is a set of integers that uniquely represents the cube; it is the union of binary numbers that an be derived when all don't cares are replaced by either true and false (following the order atomL). atomL : BoolExpr list phi : BoolExpr Returns: (Set * (Set * Set)) list list list  QuineTable2Html atomL qt  Full Usage: QuineTable2Html atomL qt Parameters: atomL : BoolExpr list qt : (Set * (Set * Set)) list list list Print a Quine table as a html table atomL : BoolExpr list qt : (Set * (Set * Set)) list list list  QuineTablePrimeImplicants qt  Full Usage: QuineTablePrimeImplicants qt Parameters: qt : (Set * (Set * Set)) list list list Returns: (BoolExpr * (Set * (Set * Set))) list Get the prime implicants of a formula phi from its Quine table: We check whether the index set of a cube is contained in one of the other cube's index set of the next level. If so, it is not a prime implicant, since it has been used to construct that higher cube. The function returns a list of tuples (piv,(idx,(pos,neg))) where piv is a boolean variable generated for the prime implicant (idx,(pos,neg)). qt : (Set * (Set * Set)) list list list Returns: (BoolExpr * (Set * (Set * Set))) list  RMNF2Str rmf  Full Usage: RMNF2Str rmf Parameters: rmf : Set> Returns: string This function converts a Reed-Muller form given in set representation to a string where xor is printed as ⊕. rmf : Set> Returns: string  SequentCalculusProof i (leftSet, rightSet)  Full Usage: SequentCalculusProof i (leftSet, rightSet) Parameters: i : int leftSet : Set rightSet : Set Returns: int * SequentProofTree Construct a proof tree for the validity of a given formula; the function expects an index i for the root node and the goal of the root node. i : int leftSet : Set rightSet : Set Returns: int * SequentProofTree  SequentProofTree2Dot ostr p  Full Usage: SequentProofTree2Dot ostr p Parameters: ostr : TextWriter p : SequentProofTree write proof tree to a dot file ostr : TextWriter p : SequentProofTree  SolveBoolExprByBDDs e  Full Usage: SolveBoolExprByBDDs e Parameters: e : BoolExpr Returns: Map option Solves a propositional logic formula phi by means of the BDD package. If there is no model, the result is None, otherwise, a model is returned as a mapping of BoolExpr to boolean truth values. e : BoolExpr Returns: Map option  SolveBoolExprBySatSolver e  Full Usage: SolveBoolExprBySatSolver e Parameters: e : BoolExpr Returns: Map option Solves a propositional logic formula phi by means of the SAT solver. If there is no model, the result is None, otherwise, a model is returned as a mapping of BoolExpr to boolean truth values. e : BoolExpr Returns: Map option  ZDD2Dot outStr writeLF (iL, zddMap)  Full Usage: ZDD2Dot outStr writeLF (iL, zddMap) Parameters: outStr : TextWriter writeLF : bool iL : int list zddMap : Map<(BoolExpr * int * int), int> Write a ZDD as generated by function ComputeZDD to a DotFile. outStr : TextWriter writeLF : bool iL : int list zddMap : Map<(BoolExpr * int * int), int>  getRMNF uniqueTable i  Full Usage: getRMNF uniqueTable i Parameters: uniqueTable : Map<(BoolExpr * int * int), int> i : int Returns: Set> Extract a Reed-Muller form set representation from a graph (FDD) given in a unique table as returned by functions ComputeFDDs and ComputeZDDs. uniqueTable : Map<(BoolExpr * int * int), int> i : int Returns: Set>  getSNFofZDD uniqueTable atomL i  Full Usage: getSNFofZDD uniqueTable atomL i Parameters: uniqueTable : Map<(BoolExpr * int * int), int> atomL : BoolExpr list i : int Returns: BoolExpr Extract a Shannon normal representation from a decision diagram (read as ZDD) given in a unique table as returned by functions ComputeFDDs and ComputeZDDs. The ordering given in atomL should be consistent with the one used in the ZDDs, i.e., leftmost atom in atomL should be closest to the leaf nodes. uniqueTable : Map<(BoolExpr * int * int), int> atomL : BoolExpr list i : int Returns: BoolExpr  printSNF indent phi  Full Usage: printSNF indent phi Parameters: indent : string phi : BoolExpr This function prints a formula in Shannon normal form such that the cofactors are printed in different lines with suitable indentation. indent : string phi : BoolExpr