## 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  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>  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>  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>  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>  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  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  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  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