(*^ ::[paletteColors = 128; automaticGrouping; currentKernel; fontset = title, inactive, noPageBreakBelow, nohscroll, preserveAspect, groupLikeTitle, center, M7, bold, L1, e8, 24, "Times"; ; fontset = subtitle, inactive, noPageBreakBelow, nohscroll, preserveAspect, groupLikeTitle, center, M7, bold, L1, e6, 18, "Times"; ; fontset = subsubtitle, inactive, noPageBreakBelow, nohscroll, preserveAspect, groupLikeTitle, center, M7, italic, L1, e6, 14, "Times"; ; fontset = section, inactive, noPageBreakBelow, nohscroll, preserveAspect, groupLikeSection, grayBox, M22, bold, L1, a20, 18, "Times"; ; fontset = subsection, inactive, noPageBreakBelow, nohscroll, preserveAspect, groupLikeSection, blackBox, M19, bold, L1, a15, 14, "Times"; ; fontset = subsubsection, inactive, noPageBreakBelow, nohscroll, preserveAspect, groupLikeSection, whiteBox, M18, bold, L1, a12, 12, "Times"; ; fontset = text, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12; fontset = smalltext, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 10, "Times"; ; fontset = input, noPageBreakBelow, nowordwrap, preserveAspect, groupLikeInput, M42, N23, bold, L1, 12, "Courier"; ; fontset = output, output, inactive, noPageBreakBelow, nowordwrap, preserveAspect, groupLikeOutput, M42, N23, L-5, 12, "Courier"; ; fontset = message, inactive, noPageBreakBelow, nowordwrap, preserveAspect, groupLikeOutput, M42, N23, L1, 12, "Courier"; ; fontset = print, inactive, noPageBreakBelow, nowordwrap, preserveAspect, groupLikeOutput, M42, N23, L1, 12, "Courier"; ; fontset = info, inactive, noPageBreakBelow, nowordwrap, preserveAspect, groupLikeOutput, M42, N23, L1, 12, "Courier"; ; fontset = postscript, PostScript, formatAsPostScript, output, inactive, noPageBreakBelow, nowordwrap, preserveAspect, groupLikeGraphics, M7, l34, w282, h287, L1, 12, "Courier"; ; fontset = name, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, italic, L1, 10, "Times"; ; fontset = header, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12; fontset = Left Header, nohscroll, cellOutline, 12; fontset = footer, inactive, nohscroll, noKeepOnOnePage, preserveAspect, center, M7, L1, 12; fontset = Left Footer, cellOutline, blackBox, 12; fontset = help, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 10, "Times"; ; fontset = clipboard, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12; fontset = completions, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12, "Courier"; ; fontset = special1, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12; fontset = special2, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12; fontset = special3, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12; fontset = special4, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12; fontset = special5, inactive, nohscroll, noKeepOnOnePage, preserveAspect, M7, L1, 12;] :[font = title; inactive; preserveAspect; startGroup; ] First-Order Theorem Proving :[font = subsubtitle; inactive; preserveAspect; ] Roberto Virga Department of Mathematics, Carnegie Mellon University rvirga+@andrew.cmu.edu :[font = subsubtitle; inactive; preserveAspect; ] Disclaimer: this work is still experimental, and not meant for public distribution. If you use this notebook, please notify the author at the address above. Bug reports and/or suggestions are highly welcome. :[font = text; inactive; preserveAspect; ] This notebook implements a theorem proving technique, complete for first order logic, presented in [4]. It is based on term rewriting techniques, and extends Knuth-Bendix completion [6] to the so-called "boolean ring", i.e. the ring formed by the logical operators and (Times) and exclusive-or (Plus), together with the logical constants true (1) and false (0). ;[s] 17:0,0;265,1;268,2;270,3;275,4;281,5;293,6;295,7;299,8;338,9;342,10;344,11;345,12;351,13;356,14;358,15;359,16;361,-1; 17:1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Courier,1,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Courier,1,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Courier,1,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Courier,1,12,0,0,0;1,11,8,Times,0,12,0,0,0; :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Initialization :[font = text; inactive; preserveAspect; ] Initializes the theorem prover. :[font = input; initialization; preserveAspect; endGroup; ] *) Restart[] := Remove["sc*", "sf*"] (* :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Syntax :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Variables :[font = text; inactive; preserveAspect; ] While Mathematica can represent (uninterpreted) funtion symbols and costants, it doesn't have a builtin notion of (free) variable. This section offers one of many possible implementations of first order variables. ;[s] 3:0,0;6,1;17,2;215,-1; 3:1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0; :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Variables :[font = text; inactive; preserveAspect; ] A variable is, by covention, any symbol beginning with "x", "y", "z", "u", "v", "w". :[font = input; initialization; preserveAspect; endGroup; ] *) VariableQ[t_Symbol] := MemberQ[ {"x", "y", "z", "u", "v", "w"}, First[Characters[ToString[t]]]]; VariableQ[t_] = False; (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Free variables :[font = text; inactive; preserveAspect; ] The list of free variables of a term is obtained by looking at the terminal nodes of a term. :[font = input; initialization; preserveAspect; endGroup; ] *) FreeVariables[expr_] := Select[ Level[{expr}, -1], Function[var, And[ VariableQ[var], FreeQ[expr, all[var, _]], FreeQ[expr, exists[var, _]]]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] VariableQ[x11] :[font = output; output; inactive; preserveAspect; endGroup; ] True ;[o] True :[font = input; preserveAspect; startGroup; ] VariableQ[c1] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; ] False ;[o] False :[font = subsubsection; inactive; preserveAspect; startGroup; ] Remark :[font = text; inactive; preserveAspect; endGroup; endGroup; ] By this definition, any symbol beginnning with an uppercase character is a constant. If you want, for example, consider "X11" a variable, you can do so by extending the previous definition. :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Renaming :[font = text; inactive; preserveAspect; ] Sometime it is useful to rename all the variables of a given term or rewrite rule. We assign variables new names of the form "xm", ..., "xn", where m, n are positive integers, n >= m. Unless specified otherwise, it is assumed m = 1. ;[s] 14:0,0;127,1;128,2;138,3;139,4;148,5;149,6;151,7;152,8;176,9;177,10;182,11;183,12;227,13;234,-1; 14:1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0; :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] New variables :[font = input; initialization; preserveAspect; endGroup; ] *) NewVariable[n_] := ToExpression[StringJoin["x", ToString[n]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Renamimg :[font = text; inactive; preserveAspect; ] Two forms of renaming are needed: renaming of term in in the boolean ring and renaming of closed first order formulas. :[font = input; initialization; preserveAspect; ] *) Rename[expr_, start_Integer:1] := Block[ {n = start}, expr /. Map[ Function[var, var -> NewVariable[n++]], Union[FreeVariables[expr]]]] /; FreeQ[expr, all] && FreeQ[expr, exists] (* :[font = input; initialization; preserveAspect; endGroup; ] *) Rename[expr_, start_Integer:1] := Block[ {n = start}, MapAt[ Function[form, form /. {form[[1]] -> NewVariable[n++]}], expr, Reverse[ Union[ Position[expr, all[_, _]], Position[expr, exists[_, _]]]]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] Rename[f[x1, x, x]] :[font = output; output; inactive; preserveAspect; endGroup; ] f[x2, x1, x1] ;[o] f[x2, x1, x1] :[font = input; preserveAspect; startGroup; ] Rename[f[x1, x, x], 3] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; ] f[x4, x3, x3] ;[o] f[x4, x3, x3] :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Remark :[font = text; inactive; preserveAspect; endGroup; endGroup; endGroup; ] Renaming may not give correct results if applied to open formulas. :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Unification :[font = text; inactive; preserveAspect; ] Mathematica implements matching (of patterns). However we will also need unification. Two terms are said to unify if there is a substitution that makes them equal. In case two terms are unifiable, we will also interested in the most general of these substitutions. ;[s] 2:0,0;11,1;264,-1; 2:1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0; :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] List Unification :[font = input; initialization; preserveAspect; endGroup; ] *) Unify[{}, {}, subst_List:{}] = subst; Unify[list1_List, {}, subst_List:{}] = False; Unify[{}, list2_List, subst_List:{}] = False; Unify[list1_List, list2_List, subst_List:{}] := Block[ {mgu = Unify[First[list1], First[list2]]}, If[mgu =!= False, Unify[ Rest[list1] /. mgu, Rest[list2] /. mgu, Union[mgu, subst /. mgu]], False]] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Term Unification :[font = input; initialization; preserveAspect; endGroup; ] *) Unify[x_, x_, subst_List:{}] = subst; Unify[x_Symbol?VariableQ, y_Symbol?VariableQ, subst_List:{}] := Append[subst, x -> y]; Unify[x_Symbol?VariableQ, y_, subst_List:{}] := If[FreeQ[y, x], Append[subst, x -> y], False]; Unify[x_, y_Symbol?VariableQ, subst_List:{}] := If[FreeQ[x, y], Append[subst, y -> x], False]; Unify[x_Symbol, y_, subst_List:{}] = False; Unify[x_, y_Symbol, subst_List:{}] = False; Unify[x_, y_, subst_List:{}] := If[ SameQ[Head[x], Head[y]], Unify[Apply[List, x], Apply[List, y]], False] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] Unify[p[x, f[a]], p[f[y], f[y]]] :[font = output; output; inactive; preserveAspect; endGroup; ] {x -> f[a], y -> a} ;[o] {x -> f[a], y -> a} :[font = input; preserveAspect; startGroup; ] Unify[p[b, f[a]], p[b, f[a]]] :[font = output; output; inactive; preserveAspect; endGroup; ] {} ;[o] {} :[font = input; preserveAspect; startGroup; ] Unify[p[b, f[a]], p[y, f[y]]] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; ] False ;[o] False :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Orderings :[font = text; inactive; preserveAspect; ] The algorithm requires a well-founded partial order to be defined on terms, to ensure termination. The ordering must also satisfy t > 1 > 0 for every non-numerical tem t. ;[s] 5:0,0;130,1;132,2;168,3;169,4;170,-1; 5:1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0; :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Restricted Quantifiers :[font = text; inactive; preserveAspect; ] The definition of the three term orderings below is significantly simplified if we first introduce functions which compute the truth value of a restricted quantification, i.e. a statement of the form "for all x in L f(x)" or "there exists x in L such that f(x)", where L is a list of terms. :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] ForAll :[font = input; initialization; preserveAspect; endGroup; ] *) ForAll[list_, f_] := Fold[And[#1, f[#2]]& , True, list] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] ForSome :[font = input; initialization; preserveAspect; endGroup; endGroup; ] *) ForSome[list_, f_] := Fold[Or[#1, f[#2]]& , False, list] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Symbols Ordering :[font = text; inactive; preserveAspect; ] All three orderings implemented require that a quasi-order (i.e. a reflexive, transitive relation) greatereq has already been defined over the set of symbols of the language. By default we use a lexicographic ordering on strings, but it is possible, and in some cases advisable, to override this choice. ;[s] 3:0,0;99,1;108,2;304,-1; 3:1,11,8,Times,0,12,0,0,0;1,10,8,Courier,1,12,0,0,0;1,11,8,Times,0,12,0,0,0; :[font = input; initialization; preserveAspect; endGroup; ] *) greatereq[term1_, term2_] := OrderedQ[{term2, term1}] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Ordering Extensions :[font = text; inactive; preserveAspect; ] In defining term orderings, we will need to compare, given two terms with the same head funtion symbol, the arguments of these funtion. From this the need to extend a given ordering between terms to sequences (or multisets) of terms. :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Multiset :[font = input; initialization; preserveAspect; endGroup; ] *) MultisetGE[{___}, {}, _] = True; MultisetGE[{}, {__}, _] = False; MultisetGE[list1_List, list2_List, greater_] := With[ {term1 = First[list1]}, MultisetGE[ Rest[list1], If[MemberQ[list2, term1], Drop[ list2, First[Position[list2, term1, {1}]]], Select[ list2, Not[greater[term1, #]]& ]], greater]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Lexicographic :[font = input; initialization; preserveAspect; endGroup; ] *) LexicographicGE[{___}, {}, _] = True; LexicographicGE[{}, {__}, _] = False; LexicographicGE[list1_List, list2_List, greater_] := If[ SameQ[First[list1], First[list2]], LexicographicGE[Rest[list1], Rest[list2], greater], greater[First[list1], First[list2]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] MultisetGE[{3, 2, 2}, {3, 2, 1, 1, 1, 1}, Greater] :[font = output; output; inactive; preserveAspect; endGroup; ] True ;[o] True :[font = input; preserveAspect; startGroup; ] LexicographicGE[{1, 2, 3}, {1, 2, 2}, Greater] :[font = output; output; inactive; preserveAspect; endGroup; ] True ;[o] True :[font = input; preserveAspect; startGroup; ] LexicographicGE[{1, 2, 3}, {1, 2, 4}, Greater] :[font = output; output; inactive; preserveAspect; endGroup; ] False ;[o] False :[font = input; preserveAspect; startGroup; ] LexicographicGE[{3, 2, 2}, {1, 2, 3, 0}, Greater] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; ] True ;[o] True :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Orderings :[font = text; inactive; preserveAspect; ] Two term orderings are provided with this implementation: Recursive Path and Lexicographic Path; for further details on these orderings, see [2, 3]. These, defined on atomic formulas, are naturally extended to sums of boolean terms by multiset comparison. :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Recursive Path :[font = input; initialization; preserveAspect; endGroup; ] *) RecursivePathGT[term1_, term1_] = False; RecursivePathGT[term1_Integer, term2_Integer] := term1 > term2; RecursivePathGT[term1_Integer, term2_] = False; RecursivePathGT[term1_, term2_Integer] = True; RecursivePathGT[term1_Plus, term2_Plus] := MultisetGE[ Apply[List, term1], Apply[List, term2], RecursivePathGT]; RecursivePathGT[term1_Plus, term2_] := MultisetGE[ Apply[List, term1], {term2}, RecursivePathGT]; RecursivePathGT[term1_, term2_Plus] := MultisetGE[ {term1}, Apply[List, term2], RecursivePathGT]; RecursivePathGT[term1_Times, term2_Times] := MultisetGE[ Apply[List, term1], Apply[List, term2], RecursivePathGT]; RecursivePathGT[term1_Times, term2_] := MultisetGE[ Apply[List, term1], {term2}, RecursivePathGT]; RecursivePathGT[term1_, term2_Times] := MultisetGE[ {term1}, Apply[List, term2], RecursivePathGT]; RecursivePathGT[term1_Symbol?VariableQ, term2_] = False; RecursivePathGT[term1_, term2_Symbol?VariableQ] := Not[FreeQ[term1, term2]]; RecursivePathGT[term1_Symbol, term2_Symbol] := greatereq[term1, term2]; RecursivePathGT[term1_Symbol, term2_] := And[ greatereq[term1, Head[term2]], ForAll[term2, RecursivePathGT[term1, #]& ]]; RecursivePathGT[term1_, term2_Symbol] := Or[ greatereq[Head[term1], term2], ForSome[term1, RecursivePathGT[#, term2]& ]]; RecursivePathGT[term1_, term2_] := With[ {head1 = Head[term1], head2 = Head[term2], args1 = Apply[List, term1], args2 = Apply[List, term2]}, Or[ ForSome[term1, RecursivePathGT[#, term2]& ], And[ greatereq[head1, head2], greatereq[head2, head1], MultisetGE[ args1, args2, RecursivePathGT]], And[ greatereq[head1, head2], Not[greatereq[head2, head1]], ForAll[ term2, RecursivePathGT[term1, #]& ]]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Lexicographic Path :[font = input; initialization; preserveAspect; endGroup; ] *) LexicographicPathGT[term1_, term1_] = False; LexicographicPathGT[term1_Integer, term2_Integer] := term1 > term2; LexicographicPathGT[term1_Integer, term2_] = False; LexicographicPathGT[term1_, term2_Integer] = True; LexicographicPathGT[term1_Plus, term2_Plus] := MultisetGE[ Apply[List, term1], Apply[List, term2], LexicographicPathGT]; LexicographicPathGT[term1_Plus, term2_] := MultisetGE[ Apply[List, term1], {term2}, LexicographicPathGT]; LexicographicPathGT[term1_, term2_Plus] := MultisetGE[ {term1}, Apply[List, term2], LexicographicPathGT]; LexicographicPathGT[term1_Times, term2_Times] := MultisetGE[ Apply[List, term1], Apply[List, term2], LexicographicPathGT]; LexicographicPathGT[term1_Times, term2_] := MultisetGE[ Apply[List, term1], {term2}, LexicographicPathGT]; LexicographicPathGT[term1_, term2_Times] := MultisetGE[ {term1}, Apply[List, term2], LexicographicPathGT]; LexicographicPathGT[term1_Symbol?VariableQ, term2_] = False; LexicographicPathGT[term1_, term2_Symbol?VariableQ] := Not[FreeQ[term1, term2]]; LexicographicPathGT[term1_Symbol, term2_Symbol] := greatereq[term1, term2]; LexicographicPathGT[term1_Symbol, term2_] := And[ greatereq[term1, Head[term2]], ForAll[term2, LexicographicPathGT[term1, #]& ]]; LexicographicPathGT[term1_, term2_Symbol] := Or[ greatereq[Head[term1], term2], ForSome[term1, LexicographicPathGT[#, term2]& ]]; LexicographicPathGT[term1_, term2_] := With[ {head1 = Head[term1], head2 = Head[term2], args1 = Apply[List, term1], args2 = Apply[List, term2]}, Or[ ForSome[term1, LexicographicPathGT[#, term2]& ], And[ greatereq[head1, head2], greatereq[head2, head1], LexicographicGE[ args1, args2, LexicographicPathGT]], And[ greatereq[head1, head2], Not[greatereq[head2, head1]], ForAll[ term2, LexicographicPathGT[term1, #]& ]]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] RecursivePathGT[g[i[x], y], f[y, x]] :[font = output; output; inactive; preserveAspect; endGroup; ] True ;[o] True :[font = input; preserveAspect; startGroup; ] RecursivePathGT[f[f[x, y], z], f[x, f[y, z]]] :[font = output; output; inactive; preserveAspect; endGroup; ] False ;[o] False :[font = input; preserveAspect; startGroup; ] LexicographicPathGT[f[f[x, y], z], f[x, f[y, z]]] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; endGroup; ] True ;[o] True :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Rules :[font = text; inactive; preserveAspect; ] Any polynomial in the system is converted in a rule L -> R, where L is the sum of all the maximal polynomials (according to the partial order used). :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Maximal Monomials :[font = input; initialization; preserveAspect; endGroup; ] *) Maximal[expr_, greater_] := Block[ {list = Sort[Apply[List, expr], greater]}, Select[ list, Not[MatchQ[greater[First[list], #], True]]& ]] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Rule-Pair Transformation :[font = input; initialization; preserveAspect; endGroup; ] *) PairToRule[{x_, y_}] := Apply[Rule, {(x /. {v_Symbol?VariableQ :> Apply[Pattern, {v, Blank[]}]}), y}] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Pair-Rule Transformation :[font = input; initialization; preserveAspect; endGroup; ] *) RuleToPair[rule_Rule] := {rule[[1]] /. {x_Pattern :> First[x]}, rule[[2]]} (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Rule-Polynomial Transformation :[font = input; initialization; preserveAspect; endGroup; ] *) RuleToPoly[rule_Rule] := Apply[Plus, RuleToPair[rule]] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Polynomial-Rule Transformation :[font = input; initialization; preserveAspect; endGroup; ] *) PolyToRule[pol_Plus, greater_] := Block[ {all = Apply[List, pol], max = Maximal[pol, greater]}, PairToRule[ {Apply[Plus, max], Apply[Plus, Complement[all, max]]}]]; PolyToRule[pol_, greater_] := PairToRule[{pol, 0}] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] Maximal[p[x] + p[a] + 1, RecursivePathGT] :[font = output; output; inactive; preserveAspect; endGroup; ] {p[x], p[a]} ;[o] {p[x], p[a]} :[font = input; preserveAspect; startGroup; ] RuleToPoly[p[x_] -> q[x] + 1] :[font = output; output; inactive; preserveAspect; endGroup; ] 1 + p[x] + q[x] ;[o] 1 + p[x] + q[x] :[font = input; preserveAspect; startGroup; ] PolyToRule[p[x] + p[a] + 1, RecursivePathGT] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; ] p[a] + p[x_] -> 1 ;[o] p[a] + p[x_] -> 1 :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Simplification :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] BA Simplification :[font = text; inactive; preserveAspect; ] According to the notation used in [3], BA is the canonical rewrite system for Boolean Algebra. :[font = input; initialization; preserveAspect; endGroup; ] *) BARewrite[expr_] := PolynomialMod[Expand[expr] /. {e_^n_Integer :> e^Sign[n]}, 2] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Simplification :[font = text; inactive; preserveAspect; ] All rules of the form L -> R are used for simplification of other rules or boolean expressions. This powerful scheme of simplification, while being very efficient since it relies on builtin features of Mathematica, it includes subsumption, required in [3]. ;[s] 3:0,0;202,1;213,2;258,-1; 3:1,11,8,Times,0,12,0,0,0;1,10,8,Times,2,12,0,0,0;1,11,8,Times,0,12,0,0,0; :[font = input; initialization; preserveAspect; ] *) Rewrite[{}, simplifiers_, greater_] = {{}, {}}; Rewrite[rules_List, simplifiers_, greater_] := Map[ Apply[Union, #]& , Transpose[Map[Rewrite[#, simplifiers, greater]& , rules]]] (* :[font = input; initialization; preserveAspect; ] *) Rewrite[rule_Rule, simplifiers_, greater_] := Block[ {newrule = PolyToRule[ Rewrite[ RuleToPoly[rule], Complement[simplifiers, {rule}]], greater]}, Switch[newrule[[1]], 0, {{}, {}}, rule[[1]], {{newrule}, {}}, _, {{}, {newrule}}]] (* :[font = input; initialization; preserveAspect; endGroup; endGroup; ] *) Rewrite[expr_, simplifiers_] := FixedPoint[ BARewrite[# /. simplifiers]& , expr] (* :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Critical Pairs :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Superpose :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Overlaps :[font = text; inactive; preserveAspect; ] Overlaps between two boolean term are computed with a variant of the BN unification algorithm presented in [5]. :[font = input; initialization; preserveAspect; endGroup; ] *) Overlap[{}, {}, subst_] = {{{1}, {1}, subst}}; Overlap[{}, terms2_List, subst_] = {{{1}, terms2, subst}}; Overlap[terms1_List, {}, subst_] = {{terms1, {1}, subst}}; Overlap[terms1_List, terms2_List, subst_] := Block[ {mgu}, Prepend[ Apply[Union, Map[ Function[term1, Apply[Union, Map[ Function[term2, mgu = Unify[term1, term2]; If[mgu =!= False, Overlap[ Complement[ terms1 /. mgu, {term1} /. mgu], Complement[ terms2 /. mgu, {term2} /. mgu], Union[ subst /. mgu, mgu]], {}]], terms2]]], terms1]], {terms1, terms2, subst}]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Inference Rule 1 :[font = input; initialization; preserveAspect; ] *) Superpose1[rule1_Rule, rule2_Rule] := Apply[Superpose1, Join[RuleToPair[rule1], RuleToPair[rule2]]] (* :[font = input; initialization; preserveAspect; endGroup; ] *) Superpose1[lhs1_Plus, rhs1_, lhs2_, rhs2_] := Apply[Union, Map[ Superpose1[#, (lhs1 - #) + rhs1, lhs2, rhs2]&, lhs1]]; Superpose1[lhs1_, rhs1_, lhs2_Plus, rhs2_] := Apply[Union, Map[ Superpose1[lhs1, rhs1, #, (lhs2 - #) + rhs2]&, lhs2]]; Superpose1[lhs1_, rhs1_, lhs2_, rhs2_] := With[ {terms1 = If[MatchQ[lhs1, _Times], Apply[List, lhs1], {lhs1}], terms2 = If[MatchQ[lhs2, _Times], Apply[List, lhs2], {lhs2}]}, Map[ (Plus[ Times[Apply[Times, #[[1]]], rhs2], Times[Apply[Times, #[[2]]], rhs1]] /. #[[3]])& , Complement[ Overlap[terms1, terms2, {}], {{terms1, terms2, {}}}]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Inference Rule 2 :[font = input; initialization; preserveAspect; ] *) Superpose2[rule_Rule] := Apply[Superpose2, RuleToPair[rule]] (* :[font = input; initialization; preserveAspect; endGroup; ] *) Superpose2[lhs_Plus, rhs_] := Apply[Union, Map[ Superpose3[#, (lhs - #) + rhs]&, lhs]]; Superpose2[lhs_, rhs_] := With[ {terms = If[MatchQ[lhs, _Times], Apply[List, lhs], {lhs}]}, Map[ (Plus[lhs, rhs] /. #[[3]])& , Select[ Overlap[terms, terms, {}], (#[[3]] =!= {})& ]]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Inference Rule 3 :[font = input; initialization; preserveAspect; ] *) Superpose3[rule_Rule] := Apply[Superpose3, RuleToPair[rule]] (* :[font = input; initialization; preserveAspect; endGroup; ] *) Superpose3[lhs_Plus, rhs_] := Apply[Union, Map[ Superpose4[#, (lhs - #) + rhs]&, lhs]]; Superpose3[lhs_, rhs_] := With[ {terms = If[MatchQ[lhs, _Times], Apply[List, lhs], {lhs}]}, Map[Plus[Times[#, rhs], rhs]&, terms]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Remark :[font = text; inactive; preserveAspect; endGroup; endGroup; ] This implementation fixes what appears to be an error in [4]. By looking at the proof of completeness of the method, it appears that overlaps of a rule with itself have top be considered; under this assumption, then, rule (2) on page 333 becomes redundant. :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Critical Pairs :[font = input; initialization; preserveAspect; endGroup; ] *) CriticalPairs[rule_Rule, rules_List] := With[ {newrule = Rename[ rule, Length[Union[FreeVariables[rules]]] + 1]}, Complement[ Map[ Rename, Rewrite[ Union[ Apply[ Union, Map[Superpose1[newrule, #]&, rules]], Apply[ Union, Map[Superpose1[#, newrule]&, rules]], Superpose2[rule], Superpose3[rule]], rules]], {0}]] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] Superpose1[p[a, x_] q[x_] -> A[x], p[y_, b] r[y_] -> B[y]] :[font = output; output; inactive; preserveAspect; endGroup; ] {B[a]*q[b] + A[b]*r[a]} ;[o] {B[a] q[b] + A[b] r[a]} :[font = input; preserveAspect; startGroup; ] Superpose2[p[x_] p[y_] -> A[x, y]] :[font = output; output; inactive; preserveAspect; endGroup; ] {A[y, y] + p[y]^2, A[x, x] + p[x]^2} ;[o] 2 2 {A[y, y] + p[y] , A[x, x] + p[x] } :[font = input; preserveAspect; startGroup; ] Superpose3[p[x_] -> A[x]] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; ] {A[x] + A[x]*p[x]} ;[o] {A[x] + A[x] p[x]} :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Completion :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Completion Strategies :[font = text; inactive; preserveAspect; ] These strategies are used to select, at each step of the completion process the next rule to consider for superposition. Of these, only the two "F.I.F.O." ones are proved to be fair (for a discussion on fairness of completion strategies, see [1]); however, the others may turn out to be handy in some particular cases. :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Lexicographic F.I.F.O. :[font = input; initialization; preserveAspect; endGroup; ] *) LexicographicFIFO[rules_List] := First[Sort[rules]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Lexicographic L.I.F.O. :[font = input; initialization; preserveAspect; endGroup; ] *) LexicographicLIFO[rules_List] := Last[Sort[rules]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Small Components F.I.F.O. :[font = input; initialization; preserveAspect; endGroup; ] *) SmallFIFO[rules_List] := First[ Sort[rules, LessEqual[ ByteCount[RuleToPoly[#1]], ByteCount[RuleToPoly[#2]]]& ]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Small Components L.I.F.O. :[font = input; initialization; preserveAspect; endGroup; endGroup; ] *) SmallLIFO[rules_List] := Last[ Sort[rules, LessEqual[ ByteCount[RuleToPoly[#1]], ByteCount[RuleToPoly[#2]]]& ]] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Completion :[font = input; initialization; preserveAspect; ] *) Options[Complete] = {Strategy -> SmallFIFO, Ordering -> RecursivePathGT, PrintTrace -> True}; (* :[font = input; initialization; preserveAspect; endGroup; endGroup; ] *) Complete[start_List, options___Rule] := Block[ {choose = Strategy /. {options} /. Options[Complete], greater = Ordering /. {options} /. Options[Complete], trace = PrintTrace /. {options} /. Options[Complete], marked = 1, unmarked = 2, rules = {{}, start}, rule, result1, result2, result}, While[And[rules[[unmarked]] =!= {}, Not[MemberQ[Apply[Union, rules], 1 -> 0]]], If[trace, Complete::trace = ToString[ TableForm[ Join[rules[[marked]], rules[[unmarked]]]]]; Message[Complete::trace]]; result1 = Rewrite[rules[[marked]], Apply[Union, rules], greater]; result2 = Rewrite[rules[[unmarked]], Apply[Union, rules], greater]; rules[[marked]] = Map[Rename, result1[[marked]]]; rules[[unmarked]] = Map[Rename, Union[ result1[[unmarked]], Apply[Union, result2]]]; rule = choose[rules[[unmarked]]]; result = CriticalPairs[rule, Apply[Union, rules]]; rules[[unmarked]] = Union[ rules[[unmarked]], Map[ PolyToRule[#, greater]& , CriticalPairs[ rule, Apply[Union, rules]]]]; AppendTo[rules[[marked]], rule]; rules[[unmarked]] = Complement[rules[[unmarked]], {rule}]]; Return[ If[MemberQ[Apply[Union, rules], 1 -> 0], {1 -> 0}, Apply[Union, rules]]]] (* :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Clause Translation :[font = text; inactive; preserveAspect; ] Closed formulas need to be tranformed in boolean terms to be processed. Skolemization is used wherever is necessary to eliminate quantifiers. :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Skolemization :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Universal Quantification :[font = input; initialization; preserveAspect; ] *) Skolemize[all[x_, form_], 1] := Skolemize[form, 1] (* :[font = input; initialization; preserveAspect; endGroup; ] *) Skolemize[all[x_, form_], -1] := Block[ {vars = Union[FreeVariables[all[x, form]]]}, Skolemize[ If[vars == {}, form /. {x -> Unique["sc"]}, form /. {x -> Apply[Unique["sf"], vars]}], -1]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Existential Quantification :[font = input; initialization; preserveAspect; ] *) Skolemize[exists[x_, form_], -1] := Skolemize[form, -1] (* :[font = input; initialization; preserveAspect; endGroup; ] *) Skolemize[exists[x_, form_], 1] := Block[ {vars = Union[FreeVariables[exists[x, form]]]}, Skolemize[ If[vars == {}, form /. {x -> Unique["sc"]}, form /. {x -> Apply[Unique["sf"], vars]}], 1]] (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Simple Formula :[font = input; initialization; preserveAspect; ] *) Skolemize[form_, 1] := form (* :[font = input; initialization; preserveAspect; endGroup; endGroup; ] *) Skolemize[form_, -1] := form (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Clause Translation :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Subformula :[font = input; initialization; preserveAspect; ] *) Clause[not[form_], sign_Integer] := (1 + Clause[form, -sign]) (* :[font = input; initialization; preserveAspect; ] *) Clause[and[form1_, form2_], sign_Integer] := (Clause[form1, sign] Clause[form2, sign]) (* :[font = input; initialization; preserveAspect; ] *) Clause[or[form1_, form2_], sign_Integer] := With[ {clause1 = Clause[form1, sign], clause2 = Clause[form2, sign]}, (clause1 + clause2 + clause1 clause2)] (* :[font = input; initialization; preserveAspect; ] *) Clause[xor[form1_, form2_], sign_Integer] := Clause[or[and[form1, not[form2]], and[not[form1], form2]], sign] (* :[font = input; initialization; preserveAspect; ] *) Clause[implies[form1_, form2_], sign_Integer] := With[ {clause1 = Clause[form1, sign], clause2 = Clause[form2, sign]}, (clause1 clause2 + (clause1 + 1))] (* :[font = input; initialization; preserveAspect; ] *) Clause[iff[form1_, form2_], sign_Integer] := Clause[or[and[form1, form2], and[not[form1], not[form2]]], sign] (* :[font = input; initialization; preserveAspect; ] *) Clause[all[x_, form_], sign_Integer] := Clause[Skolemize[all[x, form], sign], sign] (* :[font = input; initialization; preserveAspect; ] *) Clause[exists[x_, form_], sign_Integer] := Clause[Skolemize[exists[x, form], sign], sign] (* :[font = input; initialization; preserveAspect; endGroup; ] *) Clause[atom_, sign_Integer] := atom (* :[font = subsubsection; inactive; Cclosed; preserveAspect; startGroup; ] Formula :[font = input; initialization; preserveAspect; ] *) Clause[forms_List, greater_] := Union[Map[Clause[#, greater]& , forms]] (* :[font = input; initialization; preserveAspect; endGroup; endGroup; ] *) Clause[form_, greater_] := PolyToRule[Rename[BARewrite[Expand[Clause[form, 1] + 1]]], greater] (* :[font = subsection; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; preserveAspect; startGroup; ] Clause[ implies[ and[ all[x, s[x] ~implies~ q[x]], exists[y, q[y]]], exists[z, s[z]]], RecursivePathGT] :[font = output; output; inactive; preserveAspect; endGroup; ] q[sc2]*q[x1_]*s[sc3]*s[x1_] -> q[sc2] + q[sc2]*s[sc3] + q[sc2]*s[x1] + q[sc2]*q[x1]*s[x1] + q[sc2]*s[sc3]*s[x1] ;[o] q[sc2] q[x1_] s[sc3] s[x1_] -> q[sc2] + q[sc2] s[sc3] + q[sc2] s[x1] + q[sc2] q[x1] s[x1] + q[sc2] s[sc3] s[x1] :[font = input; preserveAspect; startGroup; ] Clause[all[x, exists[y, father[y, x]]], RecursivePathGT] :[font = output; output; inactive; preserveAspect; endGroup; ] father[sf2[x1_], x1_] -> 1 ;[o] father[sf2[x1_], x1_] -> 1 :[font = input; preserveAspect; startGroup; ] Clause[ iff[ (not @ (p[] ~and~ q[])), (not @ p[]) ~or~ (not @ q[])], RecursivePathGT] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; endGroup; ] 0 -> 0 ;[o] 0 -> 0 :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Theorem Proving :[font = input; initialization; preserveAspect; ] *) Options[Prover] = Options[Complete]; (* :[font = input; initialization; preserveAspect; ] *) Prover[theorem_, options___Rule] := Prover[{}, theorem, options] (* :[font = input; initialization; preserveAspect; endGroup; ] *) Prover[axioms_List, theorem_, options___Rule] := Block[ {greater = Ordering /. {options} /. Options[Prover]}, Restart[]; Complete[ Clause[ Map[Rename, Append[axioms, not[theorem]]], greater], options]] (* :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] Examples :[font = input; Cclosed; preserveAspect; startGroup; ] Prover[ {all[x, exists[y, father[y, x]]], all[x, all[y, all[z, (father[x, y] ~and~ father[y, z]) ~implies~ grandfather[x, z]]]]}, all[x, exists[y, grandfather[y, x]]]] :[font = message; inactive; preserveAspect; ] Complete::trace: father[sf1[x1_], x1_] -> 1 grandfather[x1_, sc1] -> 0 father[x2_, x1_] father[x3_, x2_] grandfather[x3_, x1_] -> father[x2, x1] father[x3, x2] :[font = message; inactive; preserveAspect; ] Complete::trace: grandfather[x1_, sc1] -> 0 father[x1_, sc1] father[x2_, x1_] -> 0 father[sf1[x1_], x1_] -> 1 father[x2_, x1_] father[x3_, x2_] grandfather[x3_, x1_] -> father[x2, x1] father[x3, x2] :[font = message; inactive; preserveAspect; ] Complete::trace: grandfather[x1_, sc1] -> 0 father[x1_, sc1] father[x2_, x1_] -> 0 father[sc1, sc1] -> 0 father[x1_, sc1] -> 0 father[x1_, sf1[sc1]] -> 0 father[sf1[x1_], x1_] -> 1 father[x2_, x1_] father[x3_, x2_] grandfather[x3_, x1_] -> father[x2, x1] father[x3, x2] :[font = output; output; inactive; preserveAspect; endGroup; endGroup; ] {1 -> 0} ;[o] {1 -> 0} :[font = section; inactive; Cclosed; preserveAspect; startGroup; ] References :[font = text; inactive; preserveAspect; ] [1]Bachmair, L., Dershowitz, N., "Critical pair criteria for completion", Journal of Symbolic Computation, Vol 6, No. 1, pp. 1-18 :[font = text; inactive; preserveAspect; ] [2]Bachmair, L., Dershowitz, N., Hsiang, J., "Orderings for equational proofs", Proceedings of the 1st Annual IEEE Symposium on Logic in Computer Science, Cambridge, MA, 1986, pp. 346-357 :[font = text; inactive; preserveAspect; ] [3]Bachmair, L., Dershowitz, N., "Inference rules for rewrite-based first-order theorem proving", Proceedings of the 2nd Annual IEEE Symposium on Logic in Computer Science, Ithaca, NY, 1987, pp. 331-337 :[font = text; inactive; preserveAspect; ] [4] Dershowitz, N., "Orderings for term rewriting systems", Theoretical Computer Science, Vol 17, No. 3, 1982, pp. 279-301 :[font = text; inactive; preserveAspect; ] [5] Hsiang, H., "Refutational theorem proving using term-rewriting systems", Artificial Intelligence, Vol 25, 1985, pp. 255-300 :[font = text; inactive; preserveAspect; endGroup; ] [6] Knuth, D.E., Bendix, P.B., "Simple word problems in universal algebras", Computational Problems in Abstract Algebra, J. Leech, Pergamon Press, Oxford, U.K., 1970, pp. 263-297 :[font = subsubtitle; inactive; preserveAspect; endGroup; ] Last updated: 14/4/96 ^*)