(* logexpr.sml Logical expression manipulation program. It generates theorems of the propositional calculus. S. Tanimoto, 3 Nov 2002. Ver. 1.01. For the Standard ML of N.J. version of ML. To run this program, put it in the startup directory for ML, start a session and type use "logexpr.sml" ; Then type demo(); or type demo2(); *) datatype propsym = P | Q | R ; datatype unaryOp = neg ; datatype binaryOp = binand | binor | binxor | implies | iff ; datatype formula = Prop of propsym | Neg of unaryOp * formula | Bin of formula * binaryOp * formula ; fun binaryopToString(binand) = " & " | binaryopToString(binor) = " v " | binaryopToString(binxor) = " xor " | binaryopToString(implies) = " -> " | binaryopToString(iff) = " <-> " ; fun formulaToString (Prop(P)) = "P" | formulaToString (Prop(Q)) = "Q" | formulaToString (Prop(R)) = "R" | formulaToString (Neg(neg,f)) = "(not " ^ formulaToString(f) ^ ")" | formulaToString (Bin(f1,binop,f2)) = "(" ^ formulaToString(f1) ^ binaryopToString(binop) ^ formulaToString(f2) ^ ")"; fun member (elt, []) = false | member (elt, a::rest) = elt = a orelse member (elt, rest) ; (* The next function evaluates a formula, using a set (actually a list) of propositional formulas that should be considered true. For example, eval(Neg(neg, Prop P), [Prop Q]) returns true, because P is not in the trueset, and so its negation is true. *) fun eval (Prop p, trueset) = member(p, trueset) | eval (Neg(neg,p), trueset) = if (eval(p, trueset)) then false else true | eval (Bin(f1,binand,f2),trueset) = eval(f1,trueset) andalso eval(f2,trueset) | eval (Bin(f1,binor,f2),trueset) = eval(f1,trueset) orelse eval(f2,trueset) | eval (Bin(f1,binxor,f2),trueset) = if eval(f1,trueset) then if eval(f2,trueset) then false else true else if eval(f2,trueset) then true else false | eval (Bin(f1,implies,f2),trueset) = if eval(f1,trueset) then eval(f2,trueset) else true | eval (Bin(f1,iff,f2),trueset) = (eval(f1,trueset) = eval(f2,trueset)); (* Ask the interpreter (and compiler) to avoid ellipses in most cases *) Compiler.Control.Print.printDepth := 1000; Compiler.Control.Print.printLength := 1000000; Compiler.Control.Print.stringDepth := 1000000; (* Some sample formulas *) val f1 = Prop(P); val f1q = Prop(Q); val f2 = Neg(neg,f1); val f3 = Bin(f1,binand,f1q); val f4 = Bin(f1,binor,f1q); val f5 = Bin(f1,binxor,f1q); val f6 = Bin(f1,implies,f1q); val f7 = Bin(f1,iff,f1q); (* substitute formula f1 for proposition p in formula f2...*) (* fun substitute (f1, p, f2) *) fun substitute (f1, p, Prop(q)) = if p = q then f1 else Prop(q) | substitute (f1, p, Neg(neg,q)) = Neg(neg,substitute(f1,p,q)) | substitute (f1, p, Bin(f3,binop,f4)) = Bin(substitute(f1,p,f3),binop,substitute(f1,p,f4)) ; fun appendLists ([a]) = a | appendLists(a::b) = a@appendLists(b) ; (* The function allOrderedPairs takes one list of values and returns a list of lists. Each of the lists has two elements and so represents one of the ordered pairs. *) fun allOrderedPairs ([]) = [] | allOrderedPairs ([a]) = [[a,a]] | allOrderedPairs (lst) = appendLists(map (fn x => map (fn y => [x,y]) lst) lst) ; (* The next function takes two lists, call them SET1 and SET2. It returns a list of ordered pairs representing the concatenation of SET1 X SET2 with SET2 X SET1, where X represents the cartesian product. *) fun allOrderedPairsFromTwoSets (set1, []) = [] | allOrderedPairsFromTwoSets ([], set2) = [] | allOrderedPairsFromTwoSets (set1, set2) = appendLists(map (fn x => map (fn y => [x,y]) set1) set2) @ appendLists(map (fn x => map (fn y => [x,y]) set2) set1) ; (* The function generateNegations takes a list of formulas and returns a new list of the same length in which each original formula appears negated. *) fun generateNegations(formulas) = map (fn x => Neg(neg,x)) formulas ; (* The functions makeOr and makeImplies each construct a new formula given two existing formulas. One uses the binary OR operator, and the other uses the Implies operator. *) fun makeOr ([x,y]) = Bin(x,binor,y); fun makeImplies ([x,y]) = Bin(x,implies,y); (* The function generateBinaries creates all formulas of depth d whose top level operator is a binary operator (either OR or IMPLIES). In order to have a formula of depth d, either the left subformula or the right subformula or both must be of depth d-1. However, the smaller subformula, if there is one, can be of any smaller depth. When d=3 (or more) the number of possibilities is very large, even with the number of ELEMENTS as small as 2. *) fun generateBinaries(d, oneShorters, elements) = let val twoOrMoreShorters = genFormulasToDepth(d-2, elements); val orderedPairsOfOneShorters = allOrderedPairs(oneShorters); val orderedPairsOfMixedDepths = allOrderedPairsFromTwoSets(oneShorters,twoOrMoreShorters); val allPairs = orderedPairsOfOneShorters @ orderedPairsOfMixedDepths; in map makeOr allPairs @ map makeImplies allPairs end and (* needed because these are mutually recursive functions *) (* Generate all formulas of depth d using the given elements. *) genFormulasAtDepth (0, elements) = elements | genFormulasAtDepth (d, []) = [] | genFormulasAtDepth (d, elements) = let val oneShorters = genFormulasAtDepth(d-1,elements) in generateNegations (oneShorters) @ generateBinaries (d, oneShorters, elements) end and (* Generate all formulas of depth d or smaller using the given elements. *) genFormulasToDepth (0, elements) = elements | genFormulasToDepth (~1, elements) = [] | genFormulasToDepth (d, elements) = genFormulasToDepth(d-1,elements) @ genFormulasAtDepth(d,elements) ; (* The next function assumes that its two arguments are lists having the same type of elements. It returns a new list containing all the elements of the two lists, except that any element occurring in the first list that also occurs in the second list is not repeated. Note that if either list contains repeated elements by itself, there may still be repeated elements in the result. *) fun union (list1,[]) = list1 | union ([],list2) = list2 | union (a::rest, list2) = if member(a,list2) then union(rest,list2) else a::union(rest,list2); (* The function getProps takes a formula and returns a list representing the set of the proposition symbols that it contains. *) fun getProps (Prop p) = [p] | getProps (Neg(neg,f)) = getProps(f) | getProps (Bin(f1,binop,f2)) = union(getProps(f1),getProps(f2)) ; (* The powerSet function takes a list that represents some set. It returns a list of lists that represents the set of all subsets of the input set. *) fun powerSet ([]) = [[]] | powerSet (a::rest) = let val restPower = powerSet(rest) in restPower @ map (fn x => a::x) restPower end ; (* The function evalAllCases takes a formula as its argument. It determines the set of proposition symbols in it. Then it generates all subsets of this set. The subsets represent the possible assignments of true or false to the proposition symbols, since the presence of a proposition symbol in a subset means it's to be considered true, while absence means false. The formula is evaluated once for each assignment, producing a list of truth values. If there were k distinct proposition symbols in the formula then there will be 2^k boolean values in the resulting list. *) fun evalAllCases(f) = map (fn vars => eval(f, vars)) (powerSet(getProps(f))); (* The function classifyBools with help from cbHelper takes a list of boolean values and returns one of three possible strings: "always true", "it depends", or "always false". *) fun cbHelper ([true]) = 1 | cbHelper ([false]) = 3 | cbHelper (true::rest) = if cbHelper(rest) = 1 then 1 else 2 | cbHelper (false::rest) = if cbHelper(rest) = 3 then 3 else 2 ; fun classifyBools(boolVector) = let val result = cbHelper(boolVector) in if result = 1 then "always true" else if result = 2 then "it depends" else "always false" end ; (* The function formulaType takes a formula, tries all possible assignments of truth values to its proposition symbols, and returns one of the three descriptive strings, indicating whether the formula is always true, variable, or always false. *) fun formulaType (f) = classifyBools(evalAllCases(f)); (* The isTheorem function takes a formula and returns true if it is always true. *) fun isTheorem (f) = (formulaType(f) = "always true") ; (* extractTheorems takes a list of formulas and returns a list of those which are theorems. *) fun extractTheorems([]) = [] | extractTheorems(f::rest) = if isTheorem(f) then f::extractTheorems(rest) else extractTheorems(rest); (* The function formulasToString takes a list of formulas and creates one big string with their more understandable descriptions. Note that this string will be too large for practical use if the depth of formulas is more than 2. Then it would be better to simply print out one string for each formula rather than trying to do all the appending, which quickly consumes memory and can take hours to complete. *) fun formulasToString([]) = "" | formulasToString(f1::rest) = formulaToString(f1) ^ ", " ^ formulasToString(rest); (* Notes about running this program... The program can, in principle, generate complex formulas. However, the combinatorial explosion of number of formulas with depth is enormous. You can run it as follows: val theorems = extractTheorems(genFormulasToDepth(2, [Prop P])); val ans = formulasToString(theorems); I ran extractTheorems(genFormulasToDepth(3, [Prop P, Prop Q])), and this took 20 minutes on a state of the art laptop. Trying to convert the resulting set of theorems to a single string may take several hours, due to the size of the string and the number of garbage collection invocations needed by ML. To keep times reasonable, restrict the depth to 2 or restrict the number of proposition symbols to 1. *) (* demonstration... *) fun demo() = formulasToString(extractTheorems(genFormulasToDepth(2, [Prop P]))); fun demo2() = formulasToString(extractTheorems(genFormulasToDepth(2, [Prop P, Prop Q])));