(* Content-type: application/vnd.wolfram.mathematica *)
(*** Wolfram Notebook File ***)
(* http://www.wolfram.com/nb *)
(* CreatedBy='Mathematica 8.0' *)
(*CacheID: 234*)
(* Internal cache information:
NotebookFileLineBreakTest
NotebookFileLineBreakTest
NotebookDataPosition[ 157, 7]
NotebookDataLength[ 141434, 3536]
NotebookOptionsPosition[ 135348, 3346]
NotebookOutlinePosition[ 136972, 3396]
CellTagsIndexPosition[ 136636, 3384]
WindowFrame->Normal*)
(* Beginning of Notebook Content *)
Notebook[{
Cell[CellGroupData[{
Cell["The Completeness Theorem of Equivalential Calculus", "DemoTitle",
CellChangeTimes->{{3.56405973078125*^9, 3.5640597655625*^9}, {
3.5642299823125*^9, 3.564229984234375*^9}}],
Cell[CellGroupData[{
Cell["", "InitializationSection"],
Cell[BoxData[
RowBox[{
RowBox[{"rulesG", "=",
RowBox[{"{",
RowBox[{
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",",
RowBox[{"{",
RowBox[{"x_", ",", "y_"}], "}"}]}], "}"}], "\[RuleDelayed]", "y"}],
",",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",", "y_"}], "}"}], ",", "z_"}], "}"}], ":>",
RowBox[{"{",
RowBox[{"x", ",",
RowBox[{"{",
RowBox[{"y", ",", "z"}], "}"}]}], "}"}]}], ",",
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"y_", ",", "z_"}], "}"}], ",", "w_"}], "}"}]}], "}"}], ":>",
RowBox[{"{",
RowBox[{"x", ",",
RowBox[{"{",
RowBox[{"y", ",",
RowBox[{"{",
RowBox[{"z", ",", "w"}], "}"}]}], "}"}]}], "}"}]}], ",",
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",",
RowBox[{"{",
RowBox[{"y_", ",", "z_"}], "}"}]}], "}"}], ":>",
RowBox[{"{",
RowBox[{"x", ",",
RowBox[{"{",
RowBox[{"z", ",", "y"}], "}"}]}], "}"}]}], ",",
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"y_", ",", "z_"}], "}"}], ",", "w_"}], "}"}]}], "}"}], ":>",
RowBox[{"{",
RowBox[{"x", ",",
RowBox[{"{",
RowBox[{"z", ",",
RowBox[{"{",
RowBox[{"y", ",", "w"}], "}"}]}], "}"}]}], "}"}]}]}], "}"}]}],
";"}]], "Input",
InitializationCell->True,
CellChangeTimes->{{3.456979887421875*^9, 3.456980048953125*^9}, {
3.45698008959375*^9, 3.45698014028125*^9}, {3.456980196625*^9,
3.45698030271875*^9}, 3.564032908921875*^9, {3.564032941859375*^9,
3.564033001625*^9}},
CellID->8114744],
Cell[BoxData[
RowBox[{
RowBox[{"pletters", "=",
RowBox[{"CharacterRange", "[",
RowBox[{"\"\
\"", ",", "\"\\""}], "]"}]}], ";"}]], "Input",
InitializationCell->True,
CellChangeTimes->{{3.56403304409375*^9, 3.56403315296875*^9}, {
3.564033211234375*^9, 3.564033211875*^9}, {3.56403454696875*^9,
3.564034549109375*^9}, 3.56405429628125*^9},
CellID->132417912],
Cell[BoxData[
RowBox[{
RowBox[{"formulaexample", "=",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"x", ",", "y"}], "}"}], ",", "z"}], "}"}], ",", "w"}],
"}"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"x", ",", "y"}], "}"}], ",", "z"}], "}"}], ",", "w"}],
"}"}], ",", "v"}], "}"}], ",", "a"}], "}"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"x", ",", "y"}], "}"}], ",", "z"}], "}"}], ",",
"w"}], "}"}], ",", "v"}], "}"}], ",", "a"}], "}"}], ",", "b"}],
"}"}], ",", "c"}], "}"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"x", ",", "y"}], "}"}], ",", "z"}], "}"}], ",",
"w"}], "}"}], ",", "v"}], "}"}], ",", "a"}], "}"}], ",",
"b"}], "}"}], ",", "c"}], "}"}], ",", "d"}], "}"}], ",", "e"}],
"}"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"x", ",", "y"}], "}"}], ",", "z"}], "}"}], ",",
"w"}], "}"}], ",", "v"}], "}"}], ",", "a"}], "}"}], ",",
"b"}], "}"}], ",", "c"}], "}"}], ",", "d"}], "}"}], ",",
"e"}], "}"}], ",", "f"}], "}"}], ",", "g"}], "}"}]}], "}"}]}],
";"}]], "Input",
InitializationCell->True,
CellChangeTimes->{{3.56403316921875*^9, 3.56403319540625*^9}, {
3.564033252140625*^9, 3.564033438625*^9}, {3.564033596734375*^9,
3.56403361978125*^9}, {3.564033653578125*^9, 3.56403370365625*^9}, {
3.564033862890625*^9, 3.56403392025*^9}, 3.564033993703125*^9, {
3.564034036390625*^9, 3.5640340375625*^9}, 3.564034822515625*^9, {
3.564034853875*^9, 3.564034914609375*^9}, 3.56403884696875*^9},
CellID->45531902],
Cell[BoxData[{
RowBox[{
RowBox[{
RowBox[{"RandomKsublist", "[",
RowBox[{"set_", ",", "k_"}], "]"}], ":=",
RowBox[{"Module", "[",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"sub", "=",
RowBox[{"{", "}"}]}], ",",
RowBox[{"rest", "=", "set"}], ",", "new"}], "}"}], ",",
"\[IndentingNewLine]",
RowBox[{
RowBox[{"Do", "[",
RowBox[{
RowBox[{
RowBox[{"new", "=",
RowBox[{"rest", "[",
RowBox[{"[",
RowBox[{"RandomInteger", "[",
RowBox[{"{",
RowBox[{"1", ",",
RowBox[{"Length", "[", "rest", "]"}]}], "}"}], "]"}], "]"}],
"]"}]}], ";",
RowBox[{"sub", "=",
RowBox[{"AppendTo", "[",
RowBox[{"sub", ",", "new"}], "]"}]}], ";",
RowBox[{"rest", "=",
RowBox[{"Complement", "[",
RowBox[{"rest", ",",
RowBox[{"{", "new", "}"}]}], "]"}]}]}], ",",
RowBox[{"{", "k", "}"}]}], "]"}], ";", "sub"}]}], "]"}]}],
";"}], "\n",
RowBox[{
RowBox[{
RowBox[{"Randompermut", "[", "k_", "]"}], ":=",
RowBox[{"RandomKsublist", "[",
RowBox[{
RowBox[{"Range", "[", "k", "]"}], ",", "k"}], "]"}]}], ";"}], "\n",
RowBox[{
RowBox[{
RowBox[{"set2", "[", "n_", "]"}], ":=",
RowBox[{"Flatten", "[",
RowBox[{
RowBox[{"Table", "[",
RowBox[{
RowBox[{"{",
RowBox[{"i", ",", "j"}], "}"}], ",",
RowBox[{"{",
RowBox[{"i", ",",
RowBox[{
RowBox[{"-", "n"}], "+", "1"}], ",",
RowBox[{"n", "-", "1"}]}], "}"}], ",",
RowBox[{"{",
RowBox[{"j", ",",
RowBox[{
RowBox[{"-", "n"}], "+", "1"}], ",",
RowBox[{"n", "-", "1"}]}], "}"}]}], "]"}], ",", "1"}], "]"}]}],
";"}]}], "Input",
InitializationCell->True,
CellID->750369280],
Cell[BoxData[
RowBox[{
RowBox[{"taut", "=", " ",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"{",
RowBox[{"2", ",", "2"}], "}"}], "}"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"2", ",", "2", ",", "2"}], "}"}], ",",
RowBox[{"{",
RowBox[{"4", ",", "2"}], "}"}]}], "}"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"2", ",", "2", ",", "2", ",", "2"}], "}"}], ",",
RowBox[{"{",
RowBox[{"4", ",", "2", ",", "2"}], "}"}], ",",
RowBox[{"{",
RowBox[{"4", ",", "4"}], "}"}]}], "}"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"2", ",", "2", ",", "2", ",", "2", ",", "2"}], "}"}], ",",
RowBox[{"{",
RowBox[{"4", ",", "2", ",", "2", ",", "2"}], "}"}], ",",
RowBox[{"{",
RowBox[{"4", ",", "4", ",", "2"}], "}"}]}], "}"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"2", ",", "2", ",", "2", ",", "2", ",", "2", ",", "2"}],
"}"}], ",",
RowBox[{"{",
RowBox[{"4", ",", "2", ",", "2", ",", "2", ",", "2"}], "}"}], ",",
RowBox[{"{",
RowBox[{"4", ",", "4", ",", "2", ",", "2"}], "}"}], ",",
RowBox[{"{",
RowBox[{"4", ",", "4", ",", "4"}], "}"}]}], "}"}]}], "}"}]}],
";"}]], "Input",
InitializationCell->True,
CellChangeTimes->{{3.564034780421875*^9, 3.56403478390625*^9}, {
3.564034939125*^9, 3.564035152140625*^9}, 3.564054331*^9},
CellID->168982622],
Cell[BoxData[
RowBox[{
RowBox[{
RowBox[{"set", "[", "k_", "]"}], ":=",
RowBox[{"Module", "[",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"kom", "=",
RowBox[{"Random", "[",
RowBox[{"Integer", ",",
RowBox[{"{",
RowBox[{"1", ",",
RowBox[{"Length", "[",
RowBox[{"taut", "[",
RowBox[{"[", "k", "]"}], "]"}], "]"}]}], "}"}]}], "]"}]}], ",",
"komb"}], "}"}], ",",
RowBox[{
RowBox[{"komb", "=",
RowBox[{"taut", "[",
RowBox[{"[",
RowBox[{"k", ",", "kom"}], "]"}], "]"}]}], ";",
RowBox[{
RowBox[{"Flatten", "[",
RowBox[{"Table", "[",
RowBox[{
RowBox[{"Table", "[",
RowBox[{
RowBox[{"pletters", "[",
RowBox[{"[", "i", "]"}], "]"}], ",",
RowBox[{"{",
RowBox[{"komb", "[",
RowBox[{"[", "i", "]"}], "]"}], "}"}]}], "]"}], ",",
RowBox[{"{",
RowBox[{"i", ",", "1", ",",
RowBox[{"Length", "[", "komb", "]"}]}], "}"}]}], "]"}], "]"}],
"[",
RowBox[{"[",
RowBox[{"Randompermut", "[",
RowBox[{
RowBox[{"2", "k"}], "+", "2"}], "]"}], "]"}], "]"}]}]}], "]"}]}],
";"}]], "Input",
InitializationCell->True,
CellChangeTimes->{{3.564035218859375*^9, 3.5640352623125*^9}, {
3.564035334234375*^9, 3.56403533446875*^9}, {3.564035397640625*^9,
3.564035452015625*^9}, {3.564035540265625*^9, 3.56403557971875*^9}, {
3.564035627546875*^9, 3.5640356445625*^9}, {3.5640356865625*^9,
3.5640356945*^9}, {3.564035888453125*^9, 3.564036081328125*^9}, {
3.56403611825*^9, 3.564036137859375*^9}, {3.56403643146875*^9,
3.564036475828125*^9}, {3.5640367485625*^9, 3.56403677290625*^9}, {
3.564036815125*^9, 3.564036816140625*^9}, 3.564054341140625*^9},
CellID->155615391],
Cell[BoxData[
RowBox[{
RowBox[{"rulesLetter1", "=",
RowBox[{"{",
RowBox[{
"x", ",", "y", ",", "z", ",", "w", ",", "v", ",", "a", ",", "b", ",", "c",
",", "d", ",", "e", ",", "f", ",", "g"}], "}"}]}], ";"}]], "Input",
InitializationCell->True,
CellChangeTimes->{{3.564037592984375*^9, 3.564037615234375*^9}, {
3.564037822078125*^9, 3.56403783740625*^9}},
CellID->17641989],
Cell[BoxData[
RowBox[{
RowBox[{"randformulaT", "[", "k_", "]"}], ":=",
RowBox[{"Module", "[",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"formula", "=",
RowBox[{"formulaexample", "[",
RowBox[{"[", "k", "]"}], "]"}]}], ",",
RowBox[{"kk", "=",
RowBox[{"Random", "[",
RowBox[{"Integer", ",",
RowBox[{"{",
RowBox[{"1", ",", "k"}], "}"}]}], "]"}]}], ",", "set1", ",",
"rul"}], "}"}], ",",
RowBox[{
RowBox[{"Do", "[",
RowBox[{
RowBox[{"formula", "=",
RowBox[{"formula", "/.", "rulesG"}]}], ",",
RowBox[{"{",
RowBox[{"i", ",", "1", ",", "kk"}], "}"}]}], " ", "]"}], ";",
RowBox[{"set1", "=",
RowBox[{"set", "[", "k", "]"}]}], ";",
RowBox[{"rul", "=",
RowBox[{"Table", "[",
RowBox[{
RowBox[{
RowBox[{"rulesLetter1", "[",
RowBox[{"[", "i", "]"}], "]"}], "\[Rule]",
RowBox[{"set1", "[",
RowBox[{"[", "i", "]"}], "]"}]}], ",",
RowBox[{"{",
RowBox[{"i", ",", "1", ",",
RowBox[{
RowBox[{"2", "k"}], "+", "2"}]}], "}"}]}], "]"}]}], ";",
RowBox[{"formula", "/.", "rul"}]}]}], "]"}]}]], "Input",
InitializationCell->True,
CellChangeTimes->{{3.564035868421875*^9, 3.56403588178125*^9}, {
3.564036889203125*^9, 3.56403690409375*^9}, {3.564037023203125*^9,
3.564037336609375*^9}, {3.564037530640625*^9, 3.56403756809375*^9}, {
3.564037642984375*^9, 3.56403775465625*^9}, 3.564037842109375*^9,
3.5640379419375*^9, {3.564052782640625*^9, 3.564052787265625*^9}},
CellID->521444088],
Cell[BoxData[
RowBox[{
RowBox[{"setpl", "=",
RowBox[{
RowBox[{"Join", "[",
RowBox[{
RowBox[{"Take", "[",
RowBox[{"pletters", ",", "3"}], "]"}], ",",
RowBox[{"Take", "[",
RowBox[{"pletters", ",", "3"}], "]"}], ",",
RowBox[{"Take", "[",
RowBox[{"pletters", ",", "3"}], "]"}], ",",
RowBox[{"Take", "[",
RowBox[{"pletters", ",", "3"}], "]"}]}], "]"}], "[",
RowBox[{"[",
RowBox[{"Randompermut", "[", "12", "]"}], "]"}], "]"}]}], ";"}]], "Input",
InitializationCell->True,
CellChangeTimes->{{3.564038105609375*^9, 3.564038126734375*^9}, {
3.56403818159375*^9, 3.56403821171875*^9}, {3.564038248671875*^9,
3.564038362296875*^9}, 3.56405436240625*^9},
CellID->479318433],
Cell[BoxData[{
RowBox[{
RowBox[{
RowBox[{"randformula", "[", "k_", "]"}], ":=",
RowBox[{"Module", "[",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"formula", "=",
RowBox[{"formulaexample", "[",
RowBox[{"[", "k", "]"}], "]"}]}], ",",
RowBox[{"kk", "=",
RowBox[{"Random", "[",
RowBox[{"Integer", ",",
RowBox[{"{",
RowBox[{"1", ",", "k"}], "}"}]}], "]"}]}], ",", "rul"}], "}"}],
",",
RowBox[{
RowBox[{"Do", "[",
RowBox[{
RowBox[{"formula", "=",
RowBox[{"formula", "/.", "rulesG"}]}], ",",
RowBox[{"{",
RowBox[{"i", ",", "1", ",", "k"}], "}"}]}], " ", "]"}], ";",
RowBox[{"rul", "=",
RowBox[{"Table", "[",
RowBox[{
RowBox[{
RowBox[{"rulesLetter1", "[",
RowBox[{"[", "i", "]"}], "]"}], "\[Rule]",
RowBox[{"setpl", "[",
RowBox[{"[", "i", "]"}], "]"}]}], ",",
RowBox[{"{",
RowBox[{"i", ",", "1", ",",
RowBox[{
RowBox[{"2", "k"}], "+", "2"}]}], "}"}]}], "]"}]}], ";",
RowBox[{"formula", "/.", "rul"}]}]}], "]"}]}],
";"}], "\[IndentingNewLine]",
RowBox[{
RowBox[{
RowBox[{"Convert", "[", "p_", "]"}], ":=",
RowBox[{"(",
RowBox[{"p", "/;",
RowBox[{"AtomQ", "[", "p", "]"}]}], ")"}]}],
";"}], "\[IndentingNewLine]",
RowBox[{
RowBox[{
RowBox[{"Convert", "[",
RowBox[{"{",
RowBox[{"p_", ",", "q_"}], "}"}], "]"}], ":=",
RowBox[{"StringJoin", "[",
RowBox[{"\"\\"", ",",
RowBox[{"Convert", "[", "p", "]"}], ",",
RowBox[{"Convert", "[", "q", "]"}]}], "]"}]}], ";"}]}], "Input",
InitializationCell->True,
CellChangeTimes->{{3.564035868421875*^9, 3.56403588178125*^9}, {
3.564036889203125*^9, 3.56403690409375*^9}, {3.564037023203125*^9,
3.564037336609375*^9}, {3.564037530640625*^9, 3.56403756809375*^9}, {
3.564037642984375*^9, 3.56403775465625*^9}, 3.564037842109375*^9,
3.5640379419375*^9, 3.564037995640625*^9, {3.564038416375*^9,
3.5640384178125*^9}, {3.564038517515625*^9, 3.564038525765625*^9}, {
3.5640386483125*^9, 3.564038649703125*^9}, {3.5640525795625*^9,
3.5640525906875*^9}, {3.564052723171875*^9, 3.56405274584375*^9}, {
3.56405291509375*^9, 3.564052950515625*^9}, {3.564053504578125*^9,
3.564053508890625*^9}, 3.564053616421875*^9, 3.5640543828125*^9, {
3.5640598555625*^9, 3.564059856578125*^9}},
CellID->542360971],
Cell[BoxData[
RowBox[{
RowBox[{"rules", "=",
RowBox[{"{",
RowBox[{
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",",
RowBox[{"{",
RowBox[{"x_", ",", "y_"}], "}"}]}], "}"}], "\[RuleDelayed]",
RowBox[{"y", "/;",
RowBox[{"AtomQ", "[", "x", "]"}]}]}], ",",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",", "y_"}], "}"}], ",", "z_"}], "}"}], ":>",
RowBox[{"{",
RowBox[{"x", ",",
RowBox[{"{",
RowBox[{"y", ",", "z"}], "}"}]}], "}"}]}], ",",
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"y_", ",", "z_"}], "}"}], ",", "w_"}], "}"}]}], "}"}], ":>",
RowBox[{
RowBox[{"{",
RowBox[{"x", ",",
RowBox[{"{",
RowBox[{"y", ",",
RowBox[{"{",
RowBox[{"z", ",", "w"}], "}"}]}], "}"}]}], "}"}], "/;",
RowBox[{
RowBox[{"AtomQ", "[", "x", "]"}], "&&",
RowBox[{"OccursQ", "[",
RowBox[{"x", ",", "y"}], "]"}]}]}]}], ",",
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",",
RowBox[{"{",
RowBox[{"y_", ",", "z_"}], "}"}]}], "}"}], ":>",
RowBox[{
RowBox[{"{",
RowBox[{"x", ",",
RowBox[{"{",
RowBox[{"z", ",", "y"}], "}"}]}], "}"}], "/;",
RowBox[{
RowBox[{"AtomQ", "[", "x", "]"}], "&&",
RowBox[{"OccursQ", "[",
RowBox[{"x", ",", "z"}], "]"}], "&&",
RowBox[{"!",
RowBox[{"OccursQ", "[",
RowBox[{"x", ",", "y"}], "]"}]}]}]}]}], ",",
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"y_", ",", "z_"}], "}"}], ",", "w_"}], "}"}]}], "}"}], ":>",
RowBox[{
RowBox[{"{",
RowBox[{"x", ",",
RowBox[{"{",
RowBox[{"z", ",",
RowBox[{"{",
RowBox[{"y", ",", "w"}], "}"}]}], "}"}]}], "}"}], "/;",
RowBox[{
RowBox[{"AtomQ", "[", "x", "]"}], "&&",
RowBox[{"OccursQ", "[",
RowBox[{"x", ",", "z"}], "]"}], "&&",
RowBox[{"!",
RowBox[{"OccursQ", "[",
RowBox[{"x", ",", "y"}], "]"}]}]}]}]}]}], "}"}]}], ";"}]], "Input",
InitializationCell->True,
CellChangeTimes->{{3.456979887421875*^9, 3.456980048953125*^9}, {
3.45698008959375*^9, 3.45698014028125*^9}, {3.456980196625*^9,
3.45698030271875*^9}, 3.564032908921875*^9, 3.5640632855625*^9, {
3.565125880703556*^9, 3.565125880970668*^9}},
CellID->474890314],
Cell[BoxData[
RowBox[{
RowBox[{"rulesE", "=",
RowBox[{"{",
RowBox[{
"\"\<1. ExExy~y\>\"", ",", "\"\<2. EExyz~ExEyz\>\"", ",",
"\"\<3. ExEEyzw~ExEyEzw\>\"", ",", "\"\<4. ExEyz~ExEzy\>\"", ",",
"\"\<5. ExEEyzw~ExEzEyw\>\""}], "}"}]}], ";"}]], "Input",
InitializationCell->True,
CellChangeTimes->{{3.5640749918125*^9, 3.564075460578125*^9}, {
3.564075496578125*^9, 3.5640755260625*^9}},
CellID->115710270],
Cell[BoxData[
RowBox[{
RowBox[{"rules1", "=",
RowBox[{"{",
RowBox[{
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",",
RowBox[{"{",
RowBox[{"x_", ",", "y_"}], "}"}]}], "}"}], "/;",
RowBox[{"AtomQ", "[", "x", "]"}]}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",", "y_"}], "}"}], ",", "z_"}], "}"}], ",",
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"y_", ",", "z_"}], "}"}], ",", "w_"}], "}"}]}], "}"}], "/;",
RowBox[{
RowBox[{"AtomQ", "[", "x", "]"}], "&&",
RowBox[{"OccursQ", "[",
RowBox[{"x", ",", "y"}], "]"}]}]}], ",",
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",",
RowBox[{"{",
RowBox[{"y_", ",", "z_"}], "}"}]}], "}"}], "/;",
RowBox[{
RowBox[{"AtomQ", "[", "x", "]"}], "&&",
RowBox[{"OccursQ", "[",
RowBox[{"x", ",", "z"}], "]"}], "&&",
RowBox[{"!",
RowBox[{"OccursQ", "[",
RowBox[{"x", ",", "y"}], "]"}]}]}]}], ",",
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"y_", ",", "z_"}], "}"}], ",", "w_"}], "}"}]}], "}"}], "/;",
RowBox[{
RowBox[{"AtomQ", "[", "x", "]"}], "&&",
RowBox[{"OccursQ", "[",
RowBox[{"x", ",", "z"}], "]"}], "&&",
RowBox[{"!",
RowBox[{"OccursQ", "[",
RowBox[{"x", ",", "y"}], "]"}]}]}]}]}], "}"}]}], ";"}]], "Input",
InitializationCell->True,
CellChangeTimes->{{3.563981837265625*^9, 3.56398187725*^9},
3.563981923203125*^9, {3.5639914225625*^9, 3.56399142375*^9},
3.564061465421875*^9, {3.565125881070465*^9, 3.5651258813429832`*^9}},
CellID->98096639],
Cell[BoxData[
RowBox[{
RowBox[{"theq", "[", "formula_", "]"}], ":=",
RowBox[{"Module", "[",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"expr", "=", "formula"}], ",",
RowBox[{"theorem", "=", "True"}], ",", "mapmatch", ",", "pos", ",",
"subs", ",", "formule"}], "}"}], ",",
RowBox[{
RowBox[{"formule", "=",
RowBox[{"{",
RowBox[{"Convert", "[", "expr", "]"}], "}"}]}], ";", "\n",
RowBox[{"While", "[",
RowBox[{
RowBox[{"theorem", " ", "&&", " ",
RowBox[{"!",
RowBox[{"MatchQ", "[",
RowBox[{"expr", ",",
RowBox[{
RowBox[{"{",
RowBox[{"x_", ",", "x_"}], "}"}], "/;",
RowBox[{"AtomQ", "[", "x", "]"}]}]}], "]"}]}]}], ",",
RowBox[{
RowBox[{"mapmatch", "=",
RowBox[{"Map", "[",
RowBox[{
RowBox[{
RowBox[{"MatchQ", "[",
RowBox[{"expr", ",", "#"}], "]"}], "&"}], ",", "rules1"}],
"]"}]}], ";",
RowBox[{"pos", "=",
RowBox[{"Position", "[",
RowBox[{"mapmatch", ",", "True"}], "]"}]}], ";",
RowBox[{"If", "[",
RowBox[{
RowBox[{"!",
RowBox[{"MemberQ", "[",
RowBox[{"mapmatch", ",", "True"}], "]"}]}], ",",
RowBox[{"theorem", "=", "False"}], ",",
RowBox[{
RowBox[{"subs", "=",
RowBox[{"Sub", "[",
RowBox[{"expr", ",",
RowBox[{"pos", "[",
RowBox[{"[",
RowBox[{"1", ",", "1"}], "]"}], "]"}]}], "]"}]}], ";",
RowBox[{"expr", "=",
RowBox[{"(",
RowBox[{"expr", "/.",
RowBox[{"rules", "[",
RowBox[{"[",
RowBox[{"pos", "[",
RowBox[{"[",
RowBox[{"1", ",", "1"}], "]"}], "]"}], "]"}], "]"}]}],
")"}]}], ";",
RowBox[{"formule", "=",
RowBox[{"Append", "[",
RowBox[{"formule", ",",
RowBox[{"Row", "[",
RowBox[{"{",
RowBox[{
RowBox[{"Convert", "[", "expr", "]"}], ",", "\"\<, \>\"",
",",
RowBox[{"pos", "[",
RowBox[{"[",
RowBox[{"1", ",", "1"}], "]"}], "]"}], ",",
RowBox[{"MapAt", "[",
RowBox[{"Convert", ",", "subs", ",",
RowBox[{"Table", "[",
RowBox[{
RowBox[{"{",
RowBox[{"i", ",", "2"}], "}"}], ",",
RowBox[{"{",
RowBox[{"i", ",", "1", ",",
RowBox[{"Length", "[", "subs", "]"}]}], "}"}]}], "]"}]}],
"]"}]}], "}"}], "]"}]}], "]"}]}]}]}], "]"}]}]}], "]"}], ";",
RowBox[{"Column", "[",
RowBox[{"{",
RowBox[{
RowBox[{"Style", "[",
RowBox[{
RowBox[{"Column", "[", "formule", "]"}], ",", "\"\\""}], "]"}],
",", "\"\<\>\"", ",",
RowBox[{"Text", "@",
RowBox[{"If", "[",
RowBox[{
"theorem", ",", "\"\\"", ",",
"\"\\""}], "]"}]}]}], "}"}],
"]"}]}]}], "]"}]}]], "Input",
InitializationCell->True,
CellChangeTimes->{{3.563982431015625*^9, 3.563982469671875*^9},
3.56398249996875*^9, {3.563982548015625*^9, 3.563982640546875*^9}, {
3.5639826985625*^9, 3.563982723875*^9}, {3.5639827630625*^9,
3.563982807890625*^9}, {3.56398287603125*^9, 3.563983269203125*^9}, {
3.56398330434375*^9, 3.56398332028125*^9}, {3.563983520296875*^9,
3.56398352678125*^9}, {3.563983580265625*^9, 3.563983592109375*^9},
3.5639836805*^9, {3.563984172265625*^9, 3.563984174984375*^9}, {
3.56398424403125*^9, 3.563984270328125*^9}, {3.5639844089375*^9,
3.563984414515625*^9}, {3.563984453765625*^9, 3.56398446534375*^9}, {
3.56398470865625*^9, 3.563984713125*^9}, {3.56398481278125*^9,
3.563984813765625*^9}, {3.563984957375*^9, 3.56398496784375*^9}, {
3.56398604853125*^9, 3.563986124171875*^9}, {3.56398690121875*^9,
3.563986912046875*^9}, {3.563986951421875*^9, 3.56398695903125*^9}, {
3.563987543234375*^9, 3.563987564078125*^9}, {3.563987614140625*^9,
3.563987622171875*^9}, {3.56398765559375*^9, 3.563987675328125*^9}, {
3.563987755015625*^9, 3.563987774390625*^9}, {3.563988156171875*^9,
3.56398819490625*^9}, {3.563988233484375*^9, 3.563988339921875*^9}, {
3.5639915976875*^9, 3.56399159921875*^9}, {3.563991659234375*^9,
3.56399167028125*^9}, {3.563991792203125*^9, 3.563991879484375*^9}, {
3.564060040140625*^9, 3.564060183921875*^9}, {3.5640602263125*^9,
3.564060238125*^9}, {3.56406049559375*^9, 3.564060500265625*^9}, {
3.564060602015625*^9, 3.56406064053125*^9}, {3.564062486171875*^9,
3.56406255115625*^9}, 3.5640627058125*^9, {3.564062842484375*^9,
3.564062847265625*^9}, 3.564062971046875*^9, {3.564065720625*^9,
3.56406572525*^9}, {3.564065817015625*^9, 3.56406588528125*^9}, {
3.5640659696875*^9, 3.564065977078125*^9}, {3.5640665648125*^9,
3.564066599875*^9}, {3.564066630578125*^9, 3.56406677040625*^9}, {
3.564067247328125*^9, 3.564067248296875*^9}, {3.564074898453125*^9,
3.564074910109375*^9}, {3.565127077881109*^9, 3.56512709516064*^9}},
CellID->259145725],
Cell[BoxData[{
RowBox[{
RowBox[{
RowBox[{"OccursQ", "[",
RowBox[{"x_", ",", "y_"}], "]"}], ":=",
RowBox[{"If", "[",
RowBox[{
RowBox[{"AtomQ", "[", "y", "]"}], ",",
RowBox[{"x", "===", "y"}], " ", ",",
RowBox[{"MemberQ", "[",
RowBox[{
RowBox[{"Flatten", "[", "y", "]"}], ",", "x"}], "]"}]}], "]"}]}],
";"}], "\[IndentingNewLine]",
RowBox[{
RowBox[{
RowBox[{"Sub", "[",
RowBox[{"expr_", ",", "1"}], "]"}], ":=",
RowBox[{"{",
RowBox[{
RowBox[{"x", "\[Rule]",
RowBox[{"expr", "[",
RowBox[{"[", "1", "]"}], "]"}]}], ",",
RowBox[{"y", "->",
RowBox[{"expr", "[",
RowBox[{"[",
RowBox[{"2", ",", "2"}], "]"}], "]"}]}]}], " ", "}"}]}],
";"}], "\[IndentingNewLine]",
RowBox[{
RowBox[{
RowBox[{"Sub", "[",
RowBox[{"expr_", ",", "2"}], "]"}], ":=",
RowBox[{"{",
RowBox[{
RowBox[{"x", "\[Rule]",
RowBox[{"expr", "[",
RowBox[{"[",
RowBox[{"1", ",", "1"}], "]"}], "]"}]}], ",",
RowBox[{"y", "->",
RowBox[{"expr", "[",
RowBox[{"[",
RowBox[{"1", ",", "2"}], "]"}], "]"}]}], ",",
RowBox[{"z", "->", " ",
RowBox[{"expr", "[",
RowBox[{"[", "2", "]"}], "]"}]}]}], "}"}]}],
";"}], "\[IndentingNewLine]",
RowBox[{
RowBox[{
RowBox[{"Sub", "[",
RowBox[{"expr_", ",", "3"}], "]"}], ":=",
RowBox[{"{",
RowBox[{
RowBox[{"x", "\[Rule]",
RowBox[{"expr", "[",
RowBox[{"[", "1", "]"}], "]"}]}], ",",
RowBox[{"y", "->",
RowBox[{"expr", "[",
RowBox[{"[",
RowBox[{"2", ",", "1", ",", "1"}], "]"}], "]"}]}], ",",
RowBox[{"z", "->", " ",
RowBox[{"expr", "[",
RowBox[{"[",
RowBox[{"2", ",", "1", ",", "2"}], "]"}], "]"}]}], ",",
RowBox[{"w", "->",
RowBox[{"expr", "[",
RowBox[{"[",
RowBox[{"2", ",", "2"}], "]"}], "]"}]}]}], "}"}]}],
";"}], "\[IndentingNewLine]",
RowBox[{
RowBox[{
RowBox[{"Sub", "[",
RowBox[{"expr_", ",", "4"}], "]"}], ":=",
RowBox[{"{",
RowBox[{
RowBox[{"x", "\[Rule]",
RowBox[{"expr", "[",
RowBox[{"[", "1", "]"}], "]"}]}], ",",
RowBox[{"y", "->",
RowBox[{"expr", "[",
RowBox[{"[",
RowBox[{"2", ",", "1"}], "]"}], "]"}]}], ",",
RowBox[{"z", "->", " ",
RowBox[{"expr", "[",
RowBox[{"[",
RowBox[{"2", ",", "2"}], "]"}], "]"}]}]}], "}"}]}],
";"}], "\[IndentingNewLine]",
RowBox[{
RowBox[{
RowBox[{"Sub", "[",
RowBox[{"expr_", ",", "5"}], "]"}], ":=",
RowBox[{"{",
RowBox[{
RowBox[{"x", "\[Rule]",
RowBox[{"expr", "[",
RowBox[{"[", "1", "]"}], "]"}]}], ",",
RowBox[{"y", "->",
RowBox[{"expr", "[",
RowBox[{"[",
RowBox[{"2", ",", "1", ",", "1"}], "]"}], "]"}]}], ",",
RowBox[{"z", "->", " ",
RowBox[{"expr", "[",
RowBox[{"[",
RowBox[{"2", ",", "1", ",", "2"}], "]"}], "]"}]}], ",",
RowBox[{"w", "->",
RowBox[{"expr", "[",
RowBox[{"[",
RowBox[{"2", ",", "2"}], "]"}], "]"}]}]}], "}"}]}], ";"}]}], "Input",
InitializationCell->True,
CellChangeTimes->{{3.456932359296875*^9, 3.45693241525*^9}, {
3.45693244659375*^9, 3.45693246159375*^9}, {3.456933620078125*^9,
3.456933633171875*^9}, {3.456933700171875*^9, 3.456933744859375*^9}, {
3.45693380625*^9, 3.4569338159375*^9}, {3.45693567415625*^9,
3.456935679015625*^9}, {3.5640634685*^9, 3.564063469890625*^9},
3.565125880622382*^9},
CellID->101636556]
}, Open ]],
Cell[CellGroupData[{
Cell["", "ManipulateSection"],
Cell[CellGroupData[{
Cell[BoxData[
RowBox[{"Manipulate", "[",
RowBox[{
RowBox[{
RowBox[{"SeedRandom", "[", "ranint", "]"}], ";",
RowBox[{"With", "[",
RowBox[{
RowBox[{"{",
RowBox[{"len", "=",
RowBox[{"Random", "[",
RowBox[{"Integer", ",",
RowBox[{"{",
RowBox[{"1", ",", "5"}], "}"}]}], "]"}]}], "}"}], ",",
RowBox[{"With", "[",
RowBox[{
RowBox[{"{",
RowBox[{"formula", "=",
RowBox[{
RowBox[{"{",
RowBox[{
RowBox[{"randformulaT", "[", "len", "]"}], ",",
RowBox[{"randformula", "[", "len", "]"}]}], "}"}], "[",
RowBox[{"[",
RowBox[{"Random", "[",
RowBox[{"Integer", ",",
RowBox[{"{",
RowBox[{"1", ",", "2"}], "}"}]}], "]"}], "]"}], "]"}]}], "}"}],
",",
RowBox[{"Style", "[",
RowBox[{
RowBox[{"Column", "[",
RowBox[{"{",
RowBox[{
RowBox[{
"Text", "@",
"\"\\""}], ",",
RowBox[{"Style", "[",
RowBox[{
RowBox[{"Convert", "[", "formula", "]"}], ",", "\"\\""}],
"]"}], ",", "\"\< \>\"", ",", "\[IndentingNewLine]",
RowBox[{"If", "[", "\[IndentingNewLine]",
RowBox[{"show", ",", "\[IndentingNewLine]",
RowBox[{"Column", "[",
RowBox[{"{",
RowBox[{
RowBox[{"Text", "@", "\"\\""}], ",",
RowBox[{"theq", "[", "formula", "]"}]}], "}"}], "]"}], ",",
"\[IndentingNewLine]",
RowBox[{"Column", "[",
RowBox[{"{", "\[IndentingNewLine]",
RowBox[{
RowBox[{"Text", "@", "\"\\""}], ",",
"\[IndentingNewLine]",
RowBox[{"Style", "[",
RowBox[{
RowBox[{"Column", "[", "rulesE", "]"}], ",",
"\"\\""}], "]"}], ",", "\[IndentingNewLine]",
RowBox[{"Text", "@",
RowBox[{"Row", "[",
RowBox[{"{",
RowBox[{"\"\<\\n\>\"", ",",
RowBox[{"Style", "[",
RowBox[{"\"\\"", ",", "Italic"}], "]"}],
",", "\"\< implementation:\\n\>\""}], "}"}], "]"}]}], ",",
"\[IndentingNewLine]",
RowBox[{"Style", "[",
RowBox[{
RowBox[{"Column", "[", "rules", "]"}], ",",
"\"\\""}], "]"}]}], "\[IndentingNewLine]", "}"}],
"]"}]}], "\[IndentingNewLine]", "]"}]}],
"\[IndentingNewLine]", "}"}], "]"}], ",", "14"}], "]"}]}],
"\[IndentingNewLine]", "]"}]}], "\[IndentingNewLine]", "]"}]}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"ranint", ",",
RowBox[{"RandomInteger", "[", "1233455", "]"}]}], "}"}], ",",
RowBox[{"ControlType", "\[Rule]", "None"}]}], "}"}], ",",
RowBox[{"Button", "[",
RowBox[{"\"\\"", ",",
RowBox[{"(*",
RowBox[{
RowBox[{"an", "=", "0"}], ";"}], "*)"}],
RowBox[{
RowBox[{"show", "=", "False"}], ";",
RowBox[{"ranint", "=",
RowBox[{"RandomInteger", "[",
RowBox[{"{",
RowBox[{"1", ",", "23423"}], "}"}], "]"}]}]}]}], "]"}], ",",
RowBox[{"{",
RowBox[{
RowBox[{"{",
RowBox[{"show", ",", "False", ",", "\"\\""}], "}"}],
",",
RowBox[{"{",
RowBox[{"True", ",", "False"}], "}"}]}], "}"}], ",",
RowBox[{"SaveDefinitions", "\[Rule]", "True"}], ",",
RowBox[{"ContentSize", "\[Rule]",
RowBox[{"{",
RowBox[{"540", ",", "450"}], "}"}]}]}], "]"}]], "Input",
CellChangeTimes->{{3.564059825265625*^9, 3.5640598293125*^9}, {
3.564062253375*^9, 3.564062324671875*^9}, {3.564062903078125*^9,
3.564062911703125*^9}, {3.564063008671875*^9, 3.56406302703125*^9}, {
3.564063075015625*^9, 3.56406311559375*^9}, {3.5640654618125*^9,
3.564065471625*^9}, {3.564065510890625*^9, 3.56406554821875*^9}, {
3.564065581515625*^9, 3.56406558484375*^9}, {3.564066014953125*^9,
3.564066018171875*^9}, {3.56406610946875*^9, 3.5640661655*^9}, {
3.564067074375*^9, 3.56406710153125*^9}, {3.5640676396875*^9,
3.564067655625*^9}, 3.564067726921875*^9, {3.5640678373125*^9,
3.56406784765625*^9}, {3.5640679285*^9, 3.564067975265625*^9}, {
3.564075595609375*^9, 3.564075637828125*^9}, {3.564149259828125*^9,
3.564149263671875*^9}, {3.565125935425517*^9, 3.565126172923163*^9}, {
3.565126328922085*^9, 3.56512647292227*^9}, {3.5651265814974613`*^9,
3.5651266958152857`*^9}, {3.565126731164814*^9, 3.565126782283996*^9}, {
3.565126861274035*^9, 3.565126926175741*^9}, {3.5651269584993773`*^9,
3.565126962108329*^9}, {3.565127108560452*^9, 3.565127110723645*^9}}],
Cell[BoxData[
TagBox[
StyleBox[
DynamicModuleBox[{$CellContext`ranint$$ = 1145408, $CellContext`show$$ =
True, Typeset`show$$ = True, Typeset`bookmarkList$$ = {},
Typeset`bookmarkMode$$ = "Menu", Typeset`animator$$, Typeset`animvar$$ =
1, Typeset`name$$ = "\"untitled\"", Typeset`specs$$ = {{{
Hold[$CellContext`ranint$$], 1145408}}, {
Hold[
Button[
"new equivalential formula", $CellContext`show$$ =
False; $CellContext`ranint$$ = RandomInteger[{1, 23423}]]],
Manipulate`Dump`ThisIsNotAControl}, {{
Hold[$CellContext`show$$], False, "show proof/rules"}, {True, False}}},
Typeset`size$$ = {335., {184.5, 189.5}}, Typeset`update$$ = 0,
Typeset`initDone$$, Typeset`skipInitDone$$ =
False, $CellContext`show$310710$$ = False},
DynamicBox[Manipulate`ManipulateBoxes[
1, StandardForm,
"Variables" :> {$CellContext`ranint$$ = 1145408, $CellContext`show$$ =
False}, "ControllerVariables" :> {
Hold[$CellContext`show$$, $CellContext`show$310710$$, False]},
"OtherVariables" :> {
Typeset`show$$, Typeset`bookmarkList$$, Typeset`bookmarkMode$$,
Typeset`animator$$, Typeset`animvar$$, Typeset`name$$,
Typeset`specs$$, Typeset`size$$, Typeset`update$$, Typeset`initDone$$,
Typeset`skipInitDone$$},
"Body" :> (SeedRandom[$CellContext`ranint$$];
With[{$CellContext`len$ = Random[Integer, {1, 5}]},
With[{$CellContext`formula$ = Part[{
$CellContext`randformulaT[$CellContext`len$],
$CellContext`randformula[$CellContext`len$]},
Random[Integer, {1, 2}]]},
Style[
Column[{
Text["Is the following formula a tautology?\n"],
Style[
$CellContext`Convert[$CellContext`formula$], "MR"], " ",
If[$CellContext`show$$,
Column[{
Text["Proof:\n"],
$CellContext`theq[$CellContext`formula$]}],
Column[{
Text["Rules:\n"],
Style[
Column[$CellContext`rulesE], "MR"],
Text[
Row[{"\n",
Style["Mathematica", Italic], " implementation:\n"}]],
Style[
Column[$CellContext`rules], "MR"]}]]}], 14]]]),
"Specifications" :> {{{$CellContext`ranint$$, 1145408}, ControlType ->
None},
Button[
"new equivalential formula", $CellContext`show$$ =
False; $CellContext`ranint$$ =
RandomInteger[{1, 23423}]], {{$CellContext`show$$, False,
"show proof/rules"}, {True, False}}},
"Options" :> {ContentSize -> {540, 450}},
"DefaultOptions" :> {ControllerLinking -> True}],
ImageSizeCache->{558., {265., 270.}},
SingleEvaluation->True],
Deinitialization:>None,
DynamicModuleValues:>{},
Initialization:>({$CellContext`randformulaT[
Pattern[$CellContext`k,
Blank[]]] :=
Module[{$CellContext`formula =
Part[$CellContext`formulaexample, $CellContext`k], $CellContext`kk =
Random[Integer, {
1, $CellContext`k}], $CellContext`set1, $CellContext`rul},
Do[$CellContext`formula =
ReplaceAll[$CellContext`formula, $CellContext`rulesG], \
{$CellContext`i,
1, $CellContext`kk}]; $CellContext`set1 = \
$CellContext`set[$CellContext`k]; $CellContext`rul =
Table[Part[$CellContext`rulesLetter1, $CellContext`i] ->
Part[$CellContext`set1, $CellContext`i], {$CellContext`i, 1,
2 $CellContext`k + 2}];
ReplaceAll[$CellContext`formula, $CellContext`rul]], \
$CellContext`formulaexample = {{{{$CellContext`x, $CellContext`y}, \
$CellContext`z}, $CellContext`w}, {{{{{$CellContext`x, $CellContext`y}, \
$CellContext`z}, $CellContext`w}, $CellContext`v}, $CellContext`a}, \
{{{{{{{$CellContext`x, $CellContext`y}, $CellContext`z}, $CellContext`w}, \
$CellContext`v}, $CellContext`a}, $CellContext`b}, $CellContext`c}, \
{{{{{{{{{$CellContext`x, $CellContext`y}, $CellContext`z}, $CellContext`w}, \
$CellContext`v}, $CellContext`a}, $CellContext`b}, $CellContext`c}, \
$CellContext`d}, $CellContext`e}, {{{{{{{{{{{$CellContext`x, $CellContext`y}, \
$CellContext`z}, $CellContext`w}, $CellContext`v}, $CellContext`a}, \
$CellContext`b}, $CellContext`c}, $CellContext`d}, $CellContext`e}, \
$CellContext`f}, $CellContext`g}}, $CellContext`rulesG = {{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]}} :> $CellContext`y, {{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]},
Pattern[$CellContext`z,
Blank[]]} :> {$CellContext`x, {$CellContext`y, $CellContext`z}}, {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :> {$CellContext`x, {$CellContext`y, {$CellContext`z, \
$CellContext`w}}}, {
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]}} :> {$CellContext`x, {$CellContext`z, \
$CellContext`y}}, {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :> {$CellContext`x, {$CellContext`z, {$CellContext`y, \
$CellContext`w}}}}, $CellContext`set[
Pattern[$CellContext`k,
Blank[]]] := Module[{$CellContext`kom = Random[Integer, {1,
Length[
Part[$CellContext`taut, $CellContext`k]]}], $CellContext`komb}, \
$CellContext`komb = Part[$CellContext`taut, $CellContext`k, $CellContext`kom];
Part[
Flatten[
Table[
Table[
Part[$CellContext`pletters, $CellContext`i], {
Part[$CellContext`komb, $CellContext`i]}], {$CellContext`i, 1,
Length[$CellContext`komb]}]],
$CellContext`Randompermut[
2 $CellContext`k + 2]]], $CellContext`taut = {{{2,
2}}, {{2, 2, 2}, {4, 2}}, {{2, 2, 2, 2}, {4, 2, 2}, {4, 4}}, {{2, 2,
2, 2, 2}, {4, 2, 2, 2}, {4, 4, 2}}, {{2, 2, 2, 2, 2, 2}, {4, 2, 2,
2, 2}, {4, 4, 2, 2}, {4, 4, 4}}}, $CellContext`pletters = {
"p", "q", "r", "s", "t", "u", "v"}, $CellContext`Randompermut[
Pattern[$CellContext`k,
Blank[]]] := $CellContext`RandomKsublist[
Range[$CellContext`k], $CellContext`k], $CellContext`RandomKsublist[
Pattern[$CellContext`set,
Blank[]],
Pattern[$CellContext`k,
Blank[]]] :=
Module[{$CellContext`sub = {}, $CellContext`rest = $CellContext`set, \
$CellContext`new}, Do[$CellContext`new = Part[$CellContext`rest,
RandomInteger[{1,
Length[$CellContext`rest]}]]; $CellContext`sub =
AppendTo[$CellContext`sub, $CellContext`new]; $CellContext`rest =
Complement[$CellContext`rest, {$CellContext`new}], \
{$CellContext`k}]; $CellContext`sub], $CellContext`rulesLetter1 = \
{$CellContext`x, $CellContext`y, $CellContext`z, $CellContext`w, \
$CellContext`v, $CellContext`a, $CellContext`b, $CellContext`c, \
$CellContext`d, $CellContext`e, $CellContext`f, $CellContext`g}, \
$CellContext`randformula[
Pattern[$CellContext`k,
Blank[]]] :=
Module[{$CellContext`formula =
Part[$CellContext`formulaexample, $CellContext`k], $CellContext`kk =
Random[Integer, {1, $CellContext`k}], $CellContext`rul},
Do[$CellContext`formula =
ReplaceAll[$CellContext`formula, $CellContext`rulesG], \
{$CellContext`i, 1, $CellContext`k}]; $CellContext`rul =
Table[Part[$CellContext`rulesLetter1, $CellContext`i] ->
Part[$CellContext`setpl, $CellContext`i], {$CellContext`i, 1,
2 $CellContext`k + 2}];
ReplaceAll[$CellContext`formula, $CellContext`rul]], \
$CellContext`setpl = {
"p", "p", "q", "p", "q", "r", "r", "q", "q", "p", "r",
"r"}, $CellContext`Convert[
Pattern[$CellContext`p,
Blank[]]] := Condition[$CellContext`p,
AtomQ[$CellContext`p]], $CellContext`Convert[{
Pattern[$CellContext`p,
Blank[]],
Pattern[$CellContext`q,
Blank[]]}] := StringJoin["E",
$CellContext`Convert[$CellContext`p],
$CellContext`Convert[$CellContext`q]], $CellContext`theq[
Pattern[$CellContext`formula,
Blank[]]] :=
Module[{$CellContext`expr = $CellContext`formula, $CellContext`theorem =
True, $CellContext`mapmatch, $CellContext`pos, $CellContext`subs, \
$CellContext`formule}, $CellContext`formule = {
$CellContext`Convert[$CellContext`expr]}; While[
And[$CellContext`theorem,
Not[
MatchQ[$CellContext`expr,
Condition[{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`x,
Blank[]]},
AtomQ[$CellContext`x]]]]], $CellContext`mapmatch =
Map[MatchQ[$CellContext`expr, #]& , $CellContext`rules1]; \
$CellContext`pos = Position[$CellContext`mapmatch, True]; If[
Not[
MemberQ[$CellContext`mapmatch, True]], $CellContext`theorem =
False, $CellContext`subs = $CellContext`Sub[$CellContext`expr,
Part[$CellContext`pos, 1, 1]]; $CellContext`expr =
ReplaceAll[$CellContext`expr,
Part[$CellContext`rules,
Part[$CellContext`pos, 1, 1]]]; $CellContext`formule =
Append[$CellContext`formule,
Row[{
$CellContext`Convert[$CellContext`expr], ", ",
Part[$CellContext`pos, 1, 1],
MapAt[$CellContext`Convert, $CellContext`subs,
Table[{$CellContext`i, 2}, {$CellContext`i, 1,
Length[$CellContext`subs]}]]}]]]]; Column[{
Style[
Column[$CellContext`formule], "MR"], "",
Text[
If[$CellContext`theorem, "The formula is a tautology.",
"The formula is not a tautology."]]}]], $CellContext`rules1 = {
Condition[{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]}},
AtomQ[$CellContext`x]], {{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]},
Pattern[$CellContext`z,
Blank[]]},
Condition[{
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]],
Condition[{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]],
Condition[{
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]]}, \
$CellContext`OccursQ[
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]] := If[
AtomQ[$CellContext`y], $CellContext`x === $CellContext`y,
MemberQ[
Flatten[$CellContext`y], $CellContext`x]], $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 1] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 2] := {$CellContext`x ->
Part[$CellContext`expr, 1, 1], $CellContext`y ->
Part[$CellContext`expr, 1, 2], $CellContext`z ->
Part[$CellContext`expr, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 3] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 1, 1], $CellContext`z ->
Part[$CellContext`expr, 2, 1, 2], $CellContext`w ->
Part[$CellContext`expr, 2, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 4] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 1], $CellContext`z ->
Part[$CellContext`expr, 2, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 5] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 1, 1], $CellContext`z ->
Part[$CellContext`expr, 2, 1, 2], $CellContext`w ->
Part[$CellContext`expr, 2, 2]}, $CellContext`rules = {{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]}} :> Condition[$CellContext`y,
AtomQ[$CellContext`x]], {{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]},
Pattern[$CellContext`z,
Blank[]]} :> {$CellContext`x, {$CellContext`y, $CellContext`z}}, {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :>
Condition[{$CellContext`x, {$CellContext`y, {$CellContext`z, \
$CellContext`w}}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]], {
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]}} :>
Condition[{$CellContext`x, {$CellContext`z, $CellContext`y}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]], {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :>
Condition[{$CellContext`x, {$CellContext`z, {$CellContext`y, \
$CellContext`w}}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]]}, \
$CellContext`rulesE = {
"1. ExExy~y", "2. EExyz~ExEyz", "3. ExEEyzw~ExEyEzw",
"4. ExEyz~ExEzy", "5. ExEEyzw~ExEzEyw"}}; Typeset`initDone$$ = True),
SynchronousInitialization->True,
UnsavedVariables:>{Typeset`initDone$$},
UntrackedVariables:>{Typeset`size$$}], "Manipulate",
Deployed->True,
StripOnInput->False],
Manipulate`InterpretManipulate[1]]], "Output",
CellChangeTimes->{{3.5661444389103823`*^9, 3.5661444677540073`*^9}},
CellID->1958622864]
}, Open ]]
}, Open ]],
Cell[CellGroupData[{
Cell["", "ManipulateCaptionSection"],
Cell[TextData[{
"This Demonstration shows \[CapitalLSlash]ukasiewicz's completeness theorem \
for the equivalential calculus. A formula is a theorem if it is deductively \
equivalent to a formula ",
StyleBox["Exx", "MR"],
", where ",
StyleBox["x", "MR"],
" is a propositional variable (propositional letter). Two adjacent lines in \
a proof such as"
}], "ManipulateCaption",
CellChangeTimes->{{3.564076415046875*^9, 3.56407672075*^9}, {
3.564078931640625*^9, 3.564078937765625*^9}, {3.56415007909375*^9,
3.56415016725*^9}, {3.56415019821875*^9, 3.564150421984375*^9},
3.5641504581875*^9, {3.564150524796875*^9, 3.564150568703125*^9},
3.56423027675*^9, {3.564230491296875*^9, 3.564230513859375*^9}, {
3.565125047954103*^9, 3.5651250488080072`*^9}, 3.5651273361072483`*^9,
3.565127560839048*^9, {3.56614312212855*^9, 3.566143135122162*^9}, {
3.5661432091950607`*^9, 3.566143227327949*^9}, {3.56621712059375*^9,
3.566217160203125*^9}, {3.566217567515625*^9, 3.5662175753125*^9}}],
Cell["\<\
EpEpEqErErq, 5{x->p, y->q, z->p, w->ErErq}\
\>", "ManipulateCaption",
CellChangeTimes->{{3.56621727884375*^9, 3.56621748434375*^9}},
CellID->284197905],
Cell["EqErErq, 1{x->p, y->EqErErq}", "ManipulateCaption",
CellChangeTimes->{{3.56621748728125*^9, 3.5662175526875*^9}, {
3.566218152015625*^9, 3.566218167265625*^9}, 3.56621878296875*^9},
CellID->49185482],
Cell["\<\
mean that the formula in the second line is obtained from the formula in the \
first line, and the rule 1 on which the substitution {x->p, y->ErErq} is \
applied. In this case the rule 1 has the form\
\>", "ManipulateCaption",
CellChangeTimes->{{3.564076415046875*^9, 3.56407672075*^9}, {
3.564078931640625*^9, 3.564078937765625*^9}, {3.56415007909375*^9,
3.56415016725*^9}, {3.56415019821875*^9, 3.564150421984375*^9},
3.5641504581875*^9, {3.564150524796875*^9, 3.564150568703125*^9},
3.56423027675*^9, {3.564230491296875*^9, 3.564230513859375*^9}, {
3.565125047954103*^9, 3.5651250488080072`*^9}, 3.5651273361072483`*^9,
3.565127560839048*^9, {3.56614312212855*^9, 3.566143135122162*^9}, {
3.5661432091950607`*^9, 3.566143227327949*^9}, {3.56621712059375*^9,
3.56621713140625*^9}, 3.5662176068125*^9, {3.5662176911875*^9,
3.566217810078125*^9}, 3.5662192220625*^9, 3.566378352171875*^9},
CellID->629924060],
Cell["EpEpEqErErq~EqErErq", "ManipulateCaption",
CellChangeTimes->{{3.56621783978125*^9, 3.56621796021875*^9}, {
3.566218027*^9, 3.566218041765625*^9}, {3.566218801453125*^9,
3.566218802328125*^9}, {3.566218834296875*^9, 3.566218863609375*^9}, {
3.566218929390625*^9, 3.566218929390625*^9}},
CellID->109221385],
Cell["\<\
showing equivalence of the formulas.\
\>", "ManipulateCaption",
CellChangeTimes->{{3.56621894434375*^9, 3.56621897003125*^9}, {
3.56621909284375*^9, 3.566219093640625*^9}},
CellID->26379133]
}, Open ]],
Cell[CellGroupData[{
Cell["", "ThumbnailSection"],
Cell[BoxData[
TagBox[
StyleBox[
DynamicModuleBox[{$CellContext`ranint$$ = 342714, $CellContext`show$$ =
False, Typeset`show$$ = True, Typeset`bookmarkList$$ = {},
Typeset`bookmarkMode$$ = "Menu", Typeset`animator$$, Typeset`animvar$$ =
1, Typeset`name$$ = "\"untitled\"", Typeset`specs$$ = {{{
Hold[$CellContext`ranint$$], 342714}}, {
Hold[
Button[
"new equivalential formula", $CellContext`show$$ =
False; $CellContext`ranint$$ = RandomInteger[{1, 23423}]]],
Manipulate`Dump`ThisIsNotAControl}, {{
Hold[$CellContext`show$$], True, "show proof/rules"}, {True, False}}},
Typeset`size$$ = {500., {206.5, 211.5}}, Typeset`update$$ = 0,
Typeset`initDone$$, Typeset`skipInitDone$$ =
False, $CellContext`show$285028$$ = False},
DynamicBox[Manipulate`ManipulateBoxes[
1, StandardForm,
"Variables" :> {$CellContext`ranint$$ = 342714, $CellContext`show$$ =
True}, "ControllerVariables" :> {
Hold[$CellContext`show$$, $CellContext`show$285028$$, False]},
"OtherVariables" :> {
Typeset`show$$, Typeset`bookmarkList$$, Typeset`bookmarkMode$$,
Typeset`animator$$, Typeset`animvar$$, Typeset`name$$,
Typeset`specs$$, Typeset`size$$, Typeset`update$$, Typeset`initDone$$,
Typeset`skipInitDone$$},
"Body" :> (SeedRandom[$CellContext`ranint$$];
With[{$CellContext`len$ = Random[Integer, {1, 5}]},
With[{$CellContext`formula$ = Part[{
$CellContext`randformulaT[$CellContext`len$],
$CellContext`randformula[$CellContext`len$]},
Random[Integer, {1, 2}]]},
Style[
Column[{
Text["Is the following formula a tautology?\n"],
Style[
$CellContext`Convert[$CellContext`formula$], "MR"], " ",
If[$CellContext`show$$,
Column[{
Text["Proof:\n"],
$CellContext`theq[$CellContext`formula$]}],
Column[{
Text["Rules:\n"],
Style[
Column[$CellContext`rulesE], "MR"],
Text[
Row[{"\n",
Style["Mathematica", Italic], " implementation:\n"}]],
Style[
Column[$CellContext`rules], "MR"]}]]}], 14]]]),
"Specifications" :> {{{$CellContext`ranint$$, 342714}, ControlType ->
None},
Button[
"new equivalential formula", $CellContext`show$$ =
False; $CellContext`ranint$$ =
RandomInteger[{1, 23423}]], {{$CellContext`show$$, True,
"show proof/rules"}, {True, False}}},
"Options" :> {ContentSize -> {540, 450}},
"DefaultOptions" :> {ControllerLinking -> True}],
ImageSizeCache->{558., {265., 270.}},
SingleEvaluation->True],
Deinitialization:>None,
DynamicModuleValues:>{},
Initialization:>({$CellContext`randformulaT[
Pattern[$CellContext`k,
Blank[]]] :=
Module[{$CellContext`formula =
Part[$CellContext`formulaexample, $CellContext`k], $CellContext`kk =
Random[Integer, {
1, $CellContext`k}], $CellContext`set1, $CellContext`rul},
Do[$CellContext`formula =
ReplaceAll[$CellContext`formula, $CellContext`rulesG], \
{$CellContext`i,
1, $CellContext`kk}]; $CellContext`set1 = \
$CellContext`set[$CellContext`k]; $CellContext`rul =
Table[Part[$CellContext`rulesLetter1, $CellContext`i] ->
Part[$CellContext`set1, $CellContext`i], {$CellContext`i, 1,
2 $CellContext`k + 2}];
ReplaceAll[$CellContext`formula, $CellContext`rul]], \
$CellContext`formulaexample = {{{{$CellContext`x, $CellContext`y}, \
$CellContext`z}, $CellContext`w}, {{{{{$CellContext`x, $CellContext`y}, \
$CellContext`z}, $CellContext`w}, $CellContext`v}, $CellContext`a}, \
{{{{{{{$CellContext`x, $CellContext`y}, $CellContext`z}, $CellContext`w}, \
$CellContext`v}, $CellContext`a}, $CellContext`b}, $CellContext`c}, \
{{{{{{{{{$CellContext`x, $CellContext`y}, $CellContext`z}, $CellContext`w}, \
$CellContext`v}, $CellContext`a}, $CellContext`b}, $CellContext`c}, \
$CellContext`d}, $CellContext`e}, {{{{{{{{{{{$CellContext`x, $CellContext`y}, \
$CellContext`z}, $CellContext`w}, $CellContext`v}, $CellContext`a}, \
$CellContext`b}, $CellContext`c}, $CellContext`d}, $CellContext`e}, \
$CellContext`f}, $CellContext`g}}, $CellContext`rulesG = {{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]}} :> $CellContext`y, {{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]},
Pattern[$CellContext`z,
Blank[]]} :> {$CellContext`x, {$CellContext`y, $CellContext`z}}, {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :> {$CellContext`x, {$CellContext`y, {$CellContext`z, \
$CellContext`w}}}, {
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]}} :> {$CellContext`x, {$CellContext`z, \
$CellContext`y}}, {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :> {$CellContext`x, {$CellContext`z, {$CellContext`y, \
$CellContext`w}}}}, $CellContext`set[
Pattern[$CellContext`k,
Blank[]]] := Module[{$CellContext`kom = Random[Integer, {1,
Length[
Part[$CellContext`taut, $CellContext`k]]}], $CellContext`komb}, \
$CellContext`komb = Part[$CellContext`taut, $CellContext`k, $CellContext`kom];
Part[
Flatten[
Table[
Table[
Part[$CellContext`pletters, $CellContext`i], {
Part[$CellContext`komb, $CellContext`i]}], {$CellContext`i, 1,
Length[$CellContext`komb]}]],
$CellContext`Randompermut[
2 $CellContext`k + 2]]], $CellContext`taut = {{{2,
2}}, {{2, 2, 2}, {4, 2}}, {{2, 2, 2, 2}, {4, 2, 2}, {4, 4}}, {{2, 2,
2, 2, 2}, {4, 2, 2, 2}, {4, 4, 2}}, {{2, 2, 2, 2, 2, 2}, {4, 2, 2,
2, 2}, {4, 4, 2, 2}, {4, 4, 4}}}, $CellContext`pletters = {
"p", "q", "r", "s", "t", "u", "v"}, $CellContext`Randompermut[
Pattern[$CellContext`k,
Blank[]]] := $CellContext`RandomKsublist[
Range[$CellContext`k], $CellContext`k], $CellContext`RandomKsublist[
Pattern[$CellContext`set,
Blank[]],
Pattern[$CellContext`k,
Blank[]]] :=
Module[{$CellContext`sub = {}, $CellContext`rest = $CellContext`set, \
$CellContext`new}, Do[$CellContext`new = Part[$CellContext`rest,
RandomInteger[{1,
Length[$CellContext`rest]}]]; $CellContext`sub =
AppendTo[$CellContext`sub, $CellContext`new]; $CellContext`rest =
Complement[$CellContext`rest, {$CellContext`new}], \
{$CellContext`k}]; $CellContext`sub], $CellContext`rulesLetter1 = \
{$CellContext`x, $CellContext`y, $CellContext`z, $CellContext`w, \
$CellContext`v, $CellContext`a, $CellContext`b, $CellContext`c, \
$CellContext`d, $CellContext`e, $CellContext`f, $CellContext`g}, \
$CellContext`randformula[
Pattern[$CellContext`k,
Blank[]]] :=
Module[{$CellContext`formula =
Part[$CellContext`formulaexample, $CellContext`k], $CellContext`kk =
Random[Integer, {1, $CellContext`k}], $CellContext`rul},
Do[$CellContext`formula =
ReplaceAll[$CellContext`formula, $CellContext`rulesG], \
{$CellContext`i, 1, $CellContext`k}]; $CellContext`rul =
Table[Part[$CellContext`rulesLetter1, $CellContext`i] ->
Part[$CellContext`setpl, $CellContext`i], {$CellContext`i, 1,
2 $CellContext`k + 2}];
ReplaceAll[$CellContext`formula, $CellContext`rul]], \
$CellContext`setpl = {
"p", "q", "r", "r", "p", "p", "q", "r", "r", "q", "q",
"p"}, $CellContext`Convert[
Pattern[$CellContext`p,
Blank[]]] := Condition[$CellContext`p,
AtomQ[$CellContext`p]], $CellContext`Convert[{
Pattern[$CellContext`p,
Blank[]],
Pattern[$CellContext`q,
Blank[]]}] := StringJoin["E",
$CellContext`Convert[$CellContext`p],
$CellContext`Convert[$CellContext`q]], $CellContext`theq[
Pattern[$CellContext`formula,
Blank[]]] :=
Module[{$CellContext`expr = $CellContext`formula, $CellContext`theorem =
True, $CellContext`mapmatch, $CellContext`pos, $CellContext`subs, \
$CellContext`formule}, $CellContext`formule = {
$CellContext`Convert[$CellContext`expr]}; While[
And[$CellContext`theorem,
Not[
MatchQ[$CellContext`expr,
Condition[{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`x,
Blank[]]},
AtomQ[$CellContext`x]]]]], $CellContext`mapmatch =
Map[MatchQ[$CellContext`expr, #]& , $CellContext`rules1]; \
$CellContext`pos = Position[$CellContext`mapmatch, True]; If[
Not[
MemberQ[$CellContext`mapmatch, True]], $CellContext`theorem =
False, $CellContext`subs = $CellContext`Sub[$CellContext`expr,
Part[$CellContext`pos, 1, 1]]; $CellContext`expr =
ReplaceAll[$CellContext`expr,
Part[$CellContext`rules,
Part[$CellContext`pos, 1, 1]]]; $CellContext`formule =
Append[$CellContext`formule,
Row[{
$CellContext`Convert[$CellContext`expr], ", ",
Part[$CellContext`pos, 1, 1],
MapAt[$CellContext`Convert, $CellContext`subs,
Table[{$CellContext`i, 2}, {$CellContext`i, 1,
Length[$CellContext`subs]}]]}]]]]; Column[{
Style[
Column[$CellContext`formule], "MR"], "",
Text[
If[$CellContext`theorem, "The formula is a tautology.",
"The formula is not a tautology."]]}]], $CellContext`rules1 = {
Condition[{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]}},
AtomQ[$CellContext`x]], {{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]},
Pattern[$CellContext`z,
Blank[]]},
Condition[{
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]],
Condition[{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]],
Condition[{
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]]}, \
$CellContext`OccursQ[
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]] := If[
AtomQ[$CellContext`y], $CellContext`x === $CellContext`y,
MemberQ[
Flatten[$CellContext`y], $CellContext`x]], $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 1] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 2] := {$CellContext`x ->
Part[$CellContext`expr, 1, 1], $CellContext`y ->
Part[$CellContext`expr, 1, 2], $CellContext`z ->
Part[$CellContext`expr, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 3] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 1, 1], $CellContext`z ->
Part[$CellContext`expr, 2, 1, 2], $CellContext`w ->
Part[$CellContext`expr, 2, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 4] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 1], $CellContext`z ->
Part[$CellContext`expr, 2, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 5] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 1, 1], $CellContext`z ->
Part[$CellContext`expr, 2, 1, 2], $CellContext`w ->
Part[$CellContext`expr, 2, 2]}, $CellContext`rules = {{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]}} :> Condition[$CellContext`y,
AtomQ[$CellContext`x]], {{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]},
Pattern[$CellContext`z,
Blank[]]} :> {$CellContext`x, {$CellContext`y, $CellContext`z}}, {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :>
Condition[{$CellContext`x, {$CellContext`y, {$CellContext`z, \
$CellContext`w}}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]], {
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]}} :>
Condition[{$CellContext`x, {$CellContext`z, $CellContext`y}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]], {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :>
Condition[{$CellContext`x, {$CellContext`z, {$CellContext`y, \
$CellContext`w}}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]]}, \
$CellContext`rulesE = {
"1. ExExy~y", "2. EExyz~ExEyz", "3. ExEEyzw~ExEyEzw",
"4. ExEyz~ExEzy", "5. ExEEyzw~ExEzEyw"}}; Typeset`initDone$$ = True),
SynchronousInitialization->True,
UnsavedVariables:>{Typeset`initDone$$},
UntrackedVariables:>{Typeset`size$$}], "Manipulate",
Deployed->True,
StripOnInput->False],
Manipulate`InterpretManipulate[1]]], "Output",
CellID->138927251]
}, Open ]],
Cell[CellGroupData[{
Cell["", "SnapshotsSection"],
Cell[BoxData[
TagBox[
StyleBox[
DynamicModuleBox[{$CellContext`ranint$$ = 13806, $CellContext`show$$ =
False, Typeset`show$$ = True, Typeset`bookmarkList$$ = {},
Typeset`bookmarkMode$$ = "Menu", Typeset`animator$$, Typeset`animvar$$ =
1, Typeset`name$$ = "\"untitled\"", Typeset`specs$$ = {{{
Hold[$CellContext`ranint$$], 13806}}, {
Hold[
Button[
"new equivalential formula", $CellContext`show$$ =
False; $CellContext`ranint$$ = RandomInteger[{1, 23423}]]],
Manipulate`Dump`ThisIsNotAControl}, {{
Hold[$CellContext`show$$], False, "show proof/rules"}, {True, False}}},
Typeset`size$$ = {500., {206.5, 211.5}}, Typeset`update$$ = 0,
Typeset`initDone$$, Typeset`skipInitDone$$ =
False, $CellContext`show$285080$$ = False},
DynamicBox[Manipulate`ManipulateBoxes[
1, StandardForm,
"Variables" :> {$CellContext`ranint$$ = 13806, $CellContext`show$$ =
False}, "ControllerVariables" :> {
Hold[$CellContext`show$$, $CellContext`show$285080$$, False]},
"OtherVariables" :> {
Typeset`show$$, Typeset`bookmarkList$$, Typeset`bookmarkMode$$,
Typeset`animator$$, Typeset`animvar$$, Typeset`name$$,
Typeset`specs$$, Typeset`size$$, Typeset`update$$, Typeset`initDone$$,
Typeset`skipInitDone$$},
"Body" :> (SeedRandom[$CellContext`ranint$$];
With[{$CellContext`len$ = Random[Integer, {1, 5}]},
With[{$CellContext`formula$ = Part[{
$CellContext`randformulaT[$CellContext`len$],
$CellContext`randformula[$CellContext`len$]},
Random[Integer, {1, 2}]]},
Style[
Column[{
Text["Is the following formula a tautology?\n"],
Style[
$CellContext`Convert[$CellContext`formula$], "MR"], " ",
If[$CellContext`show$$,
Column[{
Text["Proof:\n"],
$CellContext`theq[$CellContext`formula$]}],
Column[{
Text["Rules:\n"],
Style[
Column[$CellContext`rulesE], "MR"],
Text[
Row[{"\n",
Style["Mathematica", Italic], " implementation:\n"}]],
Style[
Column[$CellContext`rules], "MR"]}]]}], 14]]]),
"Specifications" :> {{{$CellContext`ranint$$, 13806}, ControlType ->
None},
Button[
"new equivalential formula", $CellContext`show$$ =
False; $CellContext`ranint$$ =
RandomInteger[{1, 23423}]], {{$CellContext`show$$, False,
"show proof/rules"}, {True, False}}},
"Options" :> {ContentSize -> {540, 450}},
"DefaultOptions" :> {ControllerLinking -> True}],
ImageSizeCache->{558., {265., 270.}},
SingleEvaluation->True],
Deinitialization:>None,
DynamicModuleValues:>{},
Initialization:>({$CellContext`randformulaT[
Pattern[$CellContext`k,
Blank[]]] :=
Module[{$CellContext`formula =
Part[$CellContext`formulaexample, $CellContext`k], $CellContext`kk =
Random[Integer, {
1, $CellContext`k}], $CellContext`set1, $CellContext`rul},
Do[$CellContext`formula =
ReplaceAll[$CellContext`formula, $CellContext`rulesG], \
{$CellContext`i,
1, $CellContext`kk}]; $CellContext`set1 = \
$CellContext`set[$CellContext`k]; $CellContext`rul =
Table[Part[$CellContext`rulesLetter1, $CellContext`i] ->
Part[$CellContext`set1, $CellContext`i], {$CellContext`i, 1,
2 $CellContext`k + 2}];
ReplaceAll[$CellContext`formula, $CellContext`rul]], \
$CellContext`formulaexample = {{{{$CellContext`x, $CellContext`y}, \
$CellContext`z}, $CellContext`w}, {{{{{$CellContext`x, $CellContext`y}, \
$CellContext`z}, $CellContext`w}, $CellContext`v}, $CellContext`a}, \
{{{{{{{$CellContext`x, $CellContext`y}, $CellContext`z}, $CellContext`w}, \
$CellContext`v}, $CellContext`a}, $CellContext`b}, $CellContext`c}, \
{{{{{{{{{$CellContext`x, $CellContext`y}, $CellContext`z}, $CellContext`w}, \
$CellContext`v}, $CellContext`a}, $CellContext`b}, $CellContext`c}, \
$CellContext`d}, $CellContext`e}, {{{{{{{{{{{$CellContext`x, $CellContext`y}, \
$CellContext`z}, $CellContext`w}, $CellContext`v}, $CellContext`a}, \
$CellContext`b}, $CellContext`c}, $CellContext`d}, $CellContext`e}, \
$CellContext`f}, $CellContext`g}}, $CellContext`rulesG = {{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]}} :> $CellContext`y, {{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]},
Pattern[$CellContext`z,
Blank[]]} :> {$CellContext`x, {$CellContext`y, $CellContext`z}}, {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :> {$CellContext`x, {$CellContext`y, {$CellContext`z, \
$CellContext`w}}}, {
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]}} :> {$CellContext`x, {$CellContext`z, \
$CellContext`y}}, {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :> {$CellContext`x, {$CellContext`z, {$CellContext`y, \
$CellContext`w}}}}, $CellContext`set[
Pattern[$CellContext`k,
Blank[]]] := Module[{$CellContext`kom = Random[Integer, {1,
Length[
Part[$CellContext`taut, $CellContext`k]]}], $CellContext`komb}, \
$CellContext`komb = Part[$CellContext`taut, $CellContext`k, $CellContext`kom];
Part[
Flatten[
Table[
Table[
Part[$CellContext`pletters, $CellContext`i], {
Part[$CellContext`komb, $CellContext`i]}], {$CellContext`i, 1,
Length[$CellContext`komb]}]],
$CellContext`Randompermut[
2 $CellContext`k + 2]]], $CellContext`taut = {{{2,
2}}, {{2, 2, 2}, {4, 2}}, {{2, 2, 2, 2}, {4, 2, 2}, {4, 4}}, {{2, 2,
2, 2, 2}, {4, 2, 2, 2}, {4, 4, 2}}, {{2, 2, 2, 2, 2, 2}, {4, 2, 2,
2, 2}, {4, 4, 2, 2}, {4, 4, 4}}}, $CellContext`pletters = {
"p", "q", "r", "s", "t", "u", "v"}, $CellContext`Randompermut[
Pattern[$CellContext`k,
Blank[]]] := $CellContext`RandomKsublist[
Range[$CellContext`k], $CellContext`k], $CellContext`RandomKsublist[
Pattern[$CellContext`set,
Blank[]],
Pattern[$CellContext`k,
Blank[]]] :=
Module[{$CellContext`sub = {}, $CellContext`rest = $CellContext`set, \
$CellContext`new}, Do[$CellContext`new = Part[$CellContext`rest,
RandomInteger[{1,
Length[$CellContext`rest]}]]; $CellContext`sub =
AppendTo[$CellContext`sub, $CellContext`new]; $CellContext`rest =
Complement[$CellContext`rest, {$CellContext`new}], \
{$CellContext`k}]; $CellContext`sub], $CellContext`rulesLetter1 = \
{$CellContext`x, $CellContext`y, $CellContext`z, $CellContext`w, \
$CellContext`v, $CellContext`a, $CellContext`b, $CellContext`c, \
$CellContext`d, $CellContext`e, $CellContext`f, $CellContext`g}, \
$CellContext`randformula[
Pattern[$CellContext`k,
Blank[]]] :=
Module[{$CellContext`formula =
Part[$CellContext`formulaexample, $CellContext`k], $CellContext`kk =
Random[Integer, {1, $CellContext`k}], $CellContext`rul},
Do[$CellContext`formula =
ReplaceAll[$CellContext`formula, $CellContext`rulesG], \
{$CellContext`i, 1, $CellContext`k}]; $CellContext`rul =
Table[Part[$CellContext`rulesLetter1, $CellContext`i] ->
Part[$CellContext`setpl, $CellContext`i], {$CellContext`i, 1,
2 $CellContext`k + 2}];
ReplaceAll[$CellContext`formula, $CellContext`rul]], \
$CellContext`setpl = {
"p", "q", "r", "r", "p", "p", "q", "r", "r", "q", "q",
"p"}, $CellContext`Convert[
Pattern[$CellContext`p,
Blank[]]] := Condition[$CellContext`p,
AtomQ[$CellContext`p]], $CellContext`Convert[{
Pattern[$CellContext`p,
Blank[]],
Pattern[$CellContext`q,
Blank[]]}] := StringJoin["E",
$CellContext`Convert[$CellContext`p],
$CellContext`Convert[$CellContext`q]], $CellContext`theq[
Pattern[$CellContext`formula,
Blank[]]] :=
Module[{$CellContext`expr = $CellContext`formula, $CellContext`theorem =
True, $CellContext`mapmatch, $CellContext`pos, $CellContext`subs, \
$CellContext`formule}, $CellContext`formule = {
$CellContext`Convert[$CellContext`expr]}; While[
And[$CellContext`theorem,
Not[
MatchQ[$CellContext`expr,
Condition[{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`x,
Blank[]]},
AtomQ[$CellContext`x]]]]], $CellContext`mapmatch =
Map[MatchQ[$CellContext`expr, #]& , $CellContext`rules1]; \
$CellContext`pos = Position[$CellContext`mapmatch, True]; If[
Not[
MemberQ[$CellContext`mapmatch, True]], $CellContext`theorem =
False, $CellContext`subs = $CellContext`Sub[$CellContext`expr,
Part[$CellContext`pos, 1, 1]]; $CellContext`expr =
ReplaceAll[$CellContext`expr,
Part[$CellContext`rules,
Part[$CellContext`pos, 1, 1]]]; $CellContext`formule =
Append[$CellContext`formule,
Row[{
$CellContext`Convert[$CellContext`expr], ", ",
Part[$CellContext`pos, 1, 1],
MapAt[$CellContext`Convert, $CellContext`subs,
Table[{$CellContext`i, 2}, {$CellContext`i, 1,
Length[$CellContext`subs]}]]}]]]]; Column[{
Style[
Column[$CellContext`formule], "MR"], "",
Text[
If[$CellContext`theorem, "The formula is a tautology.",
"The formula is not a tautology."]]}]], $CellContext`rules1 = {
Condition[{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]}},
AtomQ[$CellContext`x]], {{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]},
Pattern[$CellContext`z,
Blank[]]},
Condition[{
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]],
Condition[{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]],
Condition[{
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]]}, \
$CellContext`OccursQ[
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]] := If[
AtomQ[$CellContext`y], $CellContext`x === $CellContext`y,
MemberQ[
Flatten[$CellContext`y], $CellContext`x]], $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 1] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 2] := {$CellContext`x ->
Part[$CellContext`expr, 1, 1], $CellContext`y ->
Part[$CellContext`expr, 1, 2], $CellContext`z ->
Part[$CellContext`expr, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 3] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 1, 1], $CellContext`z ->
Part[$CellContext`expr, 2, 1, 2], $CellContext`w ->
Part[$CellContext`expr, 2, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 4] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 1], $CellContext`z ->
Part[$CellContext`expr, 2, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 5] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 1, 1], $CellContext`z ->
Part[$CellContext`expr, 2, 1, 2], $CellContext`w ->
Part[$CellContext`expr, 2, 2]}, $CellContext`rules = {{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]}} :> Condition[$CellContext`y,
AtomQ[$CellContext`x]], {{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]},
Pattern[$CellContext`z,
Blank[]]} :> {$CellContext`x, {$CellContext`y, $CellContext`z}}, {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :>
Condition[{$CellContext`x, {$CellContext`y, {$CellContext`z, \
$CellContext`w}}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]], {
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]}} :>
Condition[{$CellContext`x, {$CellContext`z, $CellContext`y}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]], {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :>
Condition[{$CellContext`x, {$CellContext`z, {$CellContext`y, \
$CellContext`w}}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]]}, \
$CellContext`rulesE = {
"1. ExExy~y", "2. EExyz~ExEyz", "3. ExEEyzw~ExEyEzw",
"4. ExEyz~ExEzy", "5. ExEEyzw~ExEzEyw"}}; Typeset`initDone$$ = True),
SynchronousInitialization->True,
UnsavedVariables:>{Typeset`initDone$$},
UntrackedVariables:>{Typeset`size$$}], "Manipulate",
Deployed->True,
StripOnInput->False],
Manipulate`InterpretManipulate[1]]], "Output",
CellID->635583268],
Cell[BoxData[
TagBox[
StyleBox[
DynamicModuleBox[{$CellContext`ranint$$ = 13806, $CellContext`show$$ =
True, Typeset`show$$ = True, Typeset`bookmarkList$$ = {},
Typeset`bookmarkMode$$ = "Menu", Typeset`animator$$, Typeset`animvar$$ =
1, Typeset`name$$ = "\"untitled\"", Typeset`specs$$ = {{{
Hold[$CellContext`ranint$$], 13806}}, {
Hold[
Button[
"new equivalential formula", $CellContext`show$$ =
False; $CellContext`ranint$$ = RandomInteger[{1, 23423}]]],
Manipulate`Dump`ThisIsNotAControl}, {{
Hold[$CellContext`show$$], True, "show proof/rules"}, {True, False}}},
Typeset`size$$ = {368., {175.5, 180.5}}, Typeset`update$$ = 0,
Typeset`initDone$$, Typeset`skipInitDone$$ =
False, $CellContext`show$285132$$ = False},
DynamicBox[Manipulate`ManipulateBoxes[
1, StandardForm,
"Variables" :> {$CellContext`ranint$$ = 13806, $CellContext`show$$ =
True}, "ControllerVariables" :> {
Hold[$CellContext`show$$, $CellContext`show$285132$$, False]},
"OtherVariables" :> {
Typeset`show$$, Typeset`bookmarkList$$, Typeset`bookmarkMode$$,
Typeset`animator$$, Typeset`animvar$$, Typeset`name$$,
Typeset`specs$$, Typeset`size$$, Typeset`update$$, Typeset`initDone$$,
Typeset`skipInitDone$$},
"Body" :> (SeedRandom[$CellContext`ranint$$];
With[{$CellContext`len$ = Random[Integer, {1, 5}]},
With[{$CellContext`formula$ = Part[{
$CellContext`randformulaT[$CellContext`len$],
$CellContext`randformula[$CellContext`len$]},
Random[Integer, {1, 2}]]},
Style[
Column[{
Text["Is the following formula a tautology?\n"],
Style[
$CellContext`Convert[$CellContext`formula$], "MR"], " ",
If[$CellContext`show$$,
Column[{
Text["Proof:\n"],
$CellContext`theq[$CellContext`formula$]}],
Column[{
Text["Rules:\n"],
Style[
Column[$CellContext`rulesE], "MR"],
Text[
Row[{"\n",
Style["Mathematica", Italic], " implementation:\n"}]],
Style[
Column[$CellContext`rules], "MR"]}]]}], 14]]]),
"Specifications" :> {{{$CellContext`ranint$$, 13806}, ControlType ->
None},
Button[
"new equivalential formula", $CellContext`show$$ =
False; $CellContext`ranint$$ =
RandomInteger[{1, 23423}]], {{$CellContext`show$$, True,
"show proof/rules"}, {True, False}}},
"Options" :> {ContentSize -> {540, 450}},
"DefaultOptions" :> {ControllerLinking -> True}],
ImageSizeCache->{558., {265., 270.}},
SingleEvaluation->True],
Deinitialization:>None,
DynamicModuleValues:>{},
Initialization:>({$CellContext`randformulaT[
Pattern[$CellContext`k,
Blank[]]] :=
Module[{$CellContext`formula =
Part[$CellContext`formulaexample, $CellContext`k], $CellContext`kk =
Random[Integer, {
1, $CellContext`k}], $CellContext`set1, $CellContext`rul},
Do[$CellContext`formula =
ReplaceAll[$CellContext`formula, $CellContext`rulesG], \
{$CellContext`i,
1, $CellContext`kk}]; $CellContext`set1 = \
$CellContext`set[$CellContext`k]; $CellContext`rul =
Table[Part[$CellContext`rulesLetter1, $CellContext`i] ->
Part[$CellContext`set1, $CellContext`i], {$CellContext`i, 1,
2 $CellContext`k + 2}];
ReplaceAll[$CellContext`formula, $CellContext`rul]], \
$CellContext`formulaexample = {{{{$CellContext`x, $CellContext`y}, \
$CellContext`z}, $CellContext`w}, {{{{{$CellContext`x, $CellContext`y}, \
$CellContext`z}, $CellContext`w}, $CellContext`v}, $CellContext`a}, \
{{{{{{{$CellContext`x, $CellContext`y}, $CellContext`z}, $CellContext`w}, \
$CellContext`v}, $CellContext`a}, $CellContext`b}, $CellContext`c}, \
{{{{{{{{{$CellContext`x, $CellContext`y}, $CellContext`z}, $CellContext`w}, \
$CellContext`v}, $CellContext`a}, $CellContext`b}, $CellContext`c}, \
$CellContext`d}, $CellContext`e}, {{{{{{{{{{{$CellContext`x, $CellContext`y}, \
$CellContext`z}, $CellContext`w}, $CellContext`v}, $CellContext`a}, \
$CellContext`b}, $CellContext`c}, $CellContext`d}, $CellContext`e}, \
$CellContext`f}, $CellContext`g}}, $CellContext`rulesG = {{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]}} :> $CellContext`y, {{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]},
Pattern[$CellContext`z,
Blank[]]} :> {$CellContext`x, {$CellContext`y, $CellContext`z}}, {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :> {$CellContext`x, {$CellContext`y, {$CellContext`z, \
$CellContext`w}}}, {
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]}} :> {$CellContext`x, {$CellContext`z, \
$CellContext`y}}, {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :> {$CellContext`x, {$CellContext`z, {$CellContext`y, \
$CellContext`w}}}}, $CellContext`set[
Pattern[$CellContext`k,
Blank[]]] := Module[{$CellContext`kom = Random[Integer, {1,
Length[
Part[$CellContext`taut, $CellContext`k]]}], $CellContext`komb}, \
$CellContext`komb = Part[$CellContext`taut, $CellContext`k, $CellContext`kom];
Part[
Flatten[
Table[
Table[
Part[$CellContext`pletters, $CellContext`i], {
Part[$CellContext`komb, $CellContext`i]}], {$CellContext`i, 1,
Length[$CellContext`komb]}]],
$CellContext`Randompermut[
2 $CellContext`k + 2]]], $CellContext`taut = {{{2,
2}}, {{2, 2, 2}, {4, 2}}, {{2, 2, 2, 2}, {4, 2, 2}, {4, 4}}, {{2, 2,
2, 2, 2}, {4, 2, 2, 2}, {4, 4, 2}}, {{2, 2, 2, 2, 2, 2}, {4, 2, 2,
2, 2}, {4, 4, 2, 2}, {4, 4, 4}}}, $CellContext`pletters = {
"p", "q", "r", "s", "t", "u", "v"}, $CellContext`Randompermut[
Pattern[$CellContext`k,
Blank[]]] := $CellContext`RandomKsublist[
Range[$CellContext`k], $CellContext`k], $CellContext`RandomKsublist[
Pattern[$CellContext`set,
Blank[]],
Pattern[$CellContext`k,
Blank[]]] :=
Module[{$CellContext`sub = {}, $CellContext`rest = $CellContext`set, \
$CellContext`new}, Do[$CellContext`new = Part[$CellContext`rest,
RandomInteger[{1,
Length[$CellContext`rest]}]]; $CellContext`sub =
AppendTo[$CellContext`sub, $CellContext`new]; $CellContext`rest =
Complement[$CellContext`rest, {$CellContext`new}], \
{$CellContext`k}]; $CellContext`sub], $CellContext`rulesLetter1 = \
{$CellContext`x, $CellContext`y, $CellContext`z, $CellContext`w, \
$CellContext`v, $CellContext`a, $CellContext`b, $CellContext`c, \
$CellContext`d, $CellContext`e, $CellContext`f, $CellContext`g}, \
$CellContext`randformula[
Pattern[$CellContext`k,
Blank[]]] :=
Module[{$CellContext`formula =
Part[$CellContext`formulaexample, $CellContext`k], $CellContext`kk =
Random[Integer, {1, $CellContext`k}], $CellContext`rul},
Do[$CellContext`formula =
ReplaceAll[$CellContext`formula, $CellContext`rulesG], \
{$CellContext`i, 1, $CellContext`k}]; $CellContext`rul =
Table[Part[$CellContext`rulesLetter1, $CellContext`i] ->
Part[$CellContext`setpl, $CellContext`i], {$CellContext`i, 1,
2 $CellContext`k + 2}];
ReplaceAll[$CellContext`formula, $CellContext`rul]], \
$CellContext`setpl = {
"p", "q", "r", "r", "p", "p", "q", "r", "r", "q", "q",
"p"}, $CellContext`Convert[
Pattern[$CellContext`p,
Blank[]]] := Condition[$CellContext`p,
AtomQ[$CellContext`p]], $CellContext`Convert[{
Pattern[$CellContext`p,
Blank[]],
Pattern[$CellContext`q,
Blank[]]}] := StringJoin["E",
$CellContext`Convert[$CellContext`p],
$CellContext`Convert[$CellContext`q]], $CellContext`theq[
Pattern[$CellContext`formula,
Blank[]]] :=
Module[{$CellContext`expr = $CellContext`formula, $CellContext`theorem =
True, $CellContext`mapmatch, $CellContext`pos, $CellContext`subs, \
$CellContext`formule}, $CellContext`formule = {
$CellContext`Convert[$CellContext`expr]}; While[
And[$CellContext`theorem,
Not[
MatchQ[$CellContext`expr,
Condition[{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`x,
Blank[]]},
AtomQ[$CellContext`x]]]]], $CellContext`mapmatch =
Map[MatchQ[$CellContext`expr, #]& , $CellContext`rules1]; \
$CellContext`pos = Position[$CellContext`mapmatch, True]; If[
Not[
MemberQ[$CellContext`mapmatch, True]], $CellContext`theorem =
False, $CellContext`subs = $CellContext`Sub[$CellContext`expr,
Part[$CellContext`pos, 1, 1]]; $CellContext`expr =
ReplaceAll[$CellContext`expr,
Part[$CellContext`rules,
Part[$CellContext`pos, 1, 1]]]; $CellContext`formule =
Append[$CellContext`formule,
Row[{
$CellContext`Convert[$CellContext`expr], ", ",
Part[$CellContext`pos, 1, 1],
MapAt[$CellContext`Convert, $CellContext`subs,
Table[{$CellContext`i, 2}, {$CellContext`i, 1,
Length[$CellContext`subs]}]]}]]]]; Column[{
Style[
Column[$CellContext`formule], "MR"], "",
Text[
If[$CellContext`theorem, "The formula is a tautology.",
"The formula is not a tautology."]]}]], $CellContext`rules1 = {
Condition[{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]}},
AtomQ[$CellContext`x]], {{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]},
Pattern[$CellContext`z,
Blank[]]},
Condition[{
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]],
Condition[{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]],
Condition[{
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]]}, \
$CellContext`OccursQ[
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]] := If[
AtomQ[$CellContext`y], $CellContext`x === $CellContext`y,
MemberQ[
Flatten[$CellContext`y], $CellContext`x]], $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 1] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 2] := {$CellContext`x ->
Part[$CellContext`expr, 1, 1], $CellContext`y ->
Part[$CellContext`expr, 1, 2], $CellContext`z ->
Part[$CellContext`expr, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 3] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 1, 1], $CellContext`z ->
Part[$CellContext`expr, 2, 1, 2], $CellContext`w ->
Part[$CellContext`expr, 2, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 4] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 1], $CellContext`z ->
Part[$CellContext`expr, 2, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 5] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 1, 1], $CellContext`z ->
Part[$CellContext`expr, 2, 1, 2], $CellContext`w ->
Part[$CellContext`expr, 2, 2]}, $CellContext`rules = {{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]}} :> Condition[$CellContext`y,
AtomQ[$CellContext`x]], {{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]},
Pattern[$CellContext`z,
Blank[]]} :> {$CellContext`x, {$CellContext`y, $CellContext`z}}, {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :>
Condition[{$CellContext`x, {$CellContext`y, {$CellContext`z, \
$CellContext`w}}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]], {
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]}} :>
Condition[{$CellContext`x, {$CellContext`z, $CellContext`y}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]], {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :>
Condition[{$CellContext`x, {$CellContext`z, {$CellContext`y, \
$CellContext`w}}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]]}, \
$CellContext`rulesE = {
"1. ExExy~y", "2. EExyz~ExEyz", "3. ExEEyzw~ExEyEzw",
"4. ExEyz~ExEzy", "5. ExEEyzw~ExEzEyw"}}; Typeset`initDone$$ = True),
SynchronousInitialization->True,
UnsavedVariables:>{Typeset`initDone$$},
UntrackedVariables:>{Typeset`size$$}], "Manipulate",
Deployed->True,
StripOnInput->False],
Manipulate`InterpretManipulate[1]]], "Output",
CellID->664325098],
Cell[BoxData[
TagBox[
StyleBox[
DynamicModuleBox[{$CellContext`ranint$$ = 4463, $CellContext`show$$ = True,
Typeset`show$$ = True, Typeset`bookmarkList$$ = {},
Typeset`bookmarkMode$$ = "Menu", Typeset`animator$$, Typeset`animvar$$ =
1, Typeset`name$$ = "\"untitled\"", Typeset`specs$$ = {{{
Hold[$CellContext`ranint$$], 4463}}, {
Hold[
Button[
"new equivalential formula", $CellContext`show$$ =
False; $CellContext`ranint$$ = RandomInteger[{1, 23423}]]],
Manipulate`Dump`ThisIsNotAControl}, {{
Hold[$CellContext`show$$], True, "show proof/rules"}, {True, False}}},
Typeset`size$$ = {399., {166.5, 171.5}}, Typeset`update$$ = 0,
Typeset`initDone$$, Typeset`skipInitDone$$ =
False, $CellContext`show$285184$$ = False},
DynamicBox[Manipulate`ManipulateBoxes[
1, StandardForm,
"Variables" :> {$CellContext`ranint$$ = 4463, $CellContext`show$$ =
True}, "ControllerVariables" :> {
Hold[$CellContext`show$$, $CellContext`show$285184$$, False]},
"OtherVariables" :> {
Typeset`show$$, Typeset`bookmarkList$$, Typeset`bookmarkMode$$,
Typeset`animator$$, Typeset`animvar$$, Typeset`name$$,
Typeset`specs$$, Typeset`size$$, Typeset`update$$, Typeset`initDone$$,
Typeset`skipInitDone$$},
"Body" :> (SeedRandom[$CellContext`ranint$$];
With[{$CellContext`len$ = Random[Integer, {1, 5}]},
With[{$CellContext`formula$ = Part[{
$CellContext`randformulaT[$CellContext`len$],
$CellContext`randformula[$CellContext`len$]},
Random[Integer, {1, 2}]]},
Style[
Column[{
Text["Is the following formula a tautology?\n"],
Style[
$CellContext`Convert[$CellContext`formula$], "MR"], " ",
If[$CellContext`show$$,
Column[{
Text["Proof:\n"],
$CellContext`theq[$CellContext`formula$]}],
Column[{
Text["Rules:\n"],
Style[
Column[$CellContext`rulesE], "MR"],
Text[
Row[{"\n",
Style["Mathematica", Italic], " implementation:\n"}]],
Style[
Column[$CellContext`rules], "MR"]}]]}], 14]]]),
"Specifications" :> {{{$CellContext`ranint$$, 4463}, ControlType ->
None},
Button[
"new equivalential formula", $CellContext`show$$ =
False; $CellContext`ranint$$ =
RandomInteger[{1, 23423}]], {{$CellContext`show$$, True,
"show proof/rules"}, {True, False}}},
"Options" :> {ContentSize -> {540, 450}},
"DefaultOptions" :> {ControllerLinking -> True}],
ImageSizeCache->{558., {265., 270.}},
SingleEvaluation->True],
Deinitialization:>None,
DynamicModuleValues:>{},
Initialization:>({$CellContext`randformulaT[
Pattern[$CellContext`k,
Blank[]]] :=
Module[{$CellContext`formula =
Part[$CellContext`formulaexample, $CellContext`k], $CellContext`kk =
Random[Integer, {
1, $CellContext`k}], $CellContext`set1, $CellContext`rul},
Do[$CellContext`formula =
ReplaceAll[$CellContext`formula, $CellContext`rulesG], \
{$CellContext`i,
1, $CellContext`kk}]; $CellContext`set1 = \
$CellContext`set[$CellContext`k]; $CellContext`rul =
Table[Part[$CellContext`rulesLetter1, $CellContext`i] ->
Part[$CellContext`set1, $CellContext`i], {$CellContext`i, 1,
2 $CellContext`k + 2}];
ReplaceAll[$CellContext`formula, $CellContext`rul]], \
$CellContext`formulaexample = {{{{$CellContext`x, $CellContext`y}, \
$CellContext`z}, $CellContext`w}, {{{{{$CellContext`x, $CellContext`y}, \
$CellContext`z}, $CellContext`w}, $CellContext`v}, $CellContext`a}, \
{{{{{{{$CellContext`x, $CellContext`y}, $CellContext`z}, $CellContext`w}, \
$CellContext`v}, $CellContext`a}, $CellContext`b}, $CellContext`c}, \
{{{{{{{{{$CellContext`x, $CellContext`y}, $CellContext`z}, $CellContext`w}, \
$CellContext`v}, $CellContext`a}, $CellContext`b}, $CellContext`c}, \
$CellContext`d}, $CellContext`e}, {{{{{{{{{{{$CellContext`x, $CellContext`y}, \
$CellContext`z}, $CellContext`w}, $CellContext`v}, $CellContext`a}, \
$CellContext`b}, $CellContext`c}, $CellContext`d}, $CellContext`e}, \
$CellContext`f}, $CellContext`g}}, $CellContext`rulesG = {{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]}} :> $CellContext`y, {{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]},
Pattern[$CellContext`z,
Blank[]]} :> {$CellContext`x, {$CellContext`y, $CellContext`z}}, {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :> {$CellContext`x, {$CellContext`y, {$CellContext`z, \
$CellContext`w}}}, {
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]}} :> {$CellContext`x, {$CellContext`z, \
$CellContext`y}}, {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :> {$CellContext`x, {$CellContext`z, {$CellContext`y, \
$CellContext`w}}}}, $CellContext`set[
Pattern[$CellContext`k,
Blank[]]] := Module[{$CellContext`kom = Random[Integer, {1,
Length[
Part[$CellContext`taut, $CellContext`k]]}], $CellContext`komb}, \
$CellContext`komb = Part[$CellContext`taut, $CellContext`k, $CellContext`kom];
Part[
Flatten[
Table[
Table[
Part[$CellContext`pletters, $CellContext`i], {
Part[$CellContext`komb, $CellContext`i]}], {$CellContext`i, 1,
Length[$CellContext`komb]}]],
$CellContext`Randompermut[
2 $CellContext`k + 2]]], $CellContext`taut = {{{2,
2}}, {{2, 2, 2}, {4, 2}}, {{2, 2, 2, 2}, {4, 2, 2}, {4, 4}}, {{2, 2,
2, 2, 2}, {4, 2, 2, 2}, {4, 4, 2}}, {{2, 2, 2, 2, 2, 2}, {4, 2, 2,
2, 2}, {4, 4, 2, 2}, {4, 4, 4}}}, $CellContext`pletters = {
"p", "q", "r", "s", "t", "u", "v"}, $CellContext`Randompermut[
Pattern[$CellContext`k,
Blank[]]] := $CellContext`RandomKsublist[
Range[$CellContext`k], $CellContext`k], $CellContext`RandomKsublist[
Pattern[$CellContext`set,
Blank[]],
Pattern[$CellContext`k,
Blank[]]] :=
Module[{$CellContext`sub = {}, $CellContext`rest = $CellContext`set, \
$CellContext`new}, Do[$CellContext`new = Part[$CellContext`rest,
RandomInteger[{1,
Length[$CellContext`rest]}]]; $CellContext`sub =
AppendTo[$CellContext`sub, $CellContext`new]; $CellContext`rest =
Complement[$CellContext`rest, {$CellContext`new}], \
{$CellContext`k}]; $CellContext`sub], $CellContext`rulesLetter1 = \
{$CellContext`x, $CellContext`y, $CellContext`z, $CellContext`w, \
$CellContext`v, $CellContext`a, $CellContext`b, $CellContext`c, \
$CellContext`d, $CellContext`e, $CellContext`f, $CellContext`g}, \
$CellContext`randformula[
Pattern[$CellContext`k,
Blank[]]] :=
Module[{$CellContext`formula =
Part[$CellContext`formulaexample, $CellContext`k], $CellContext`kk =
Random[Integer, {1, $CellContext`k}], $CellContext`rul},
Do[$CellContext`formula =
ReplaceAll[$CellContext`formula, $CellContext`rulesG], \
{$CellContext`i, 1, $CellContext`k}]; $CellContext`rul =
Table[Part[$CellContext`rulesLetter1, $CellContext`i] ->
Part[$CellContext`setpl, $CellContext`i], {$CellContext`i, 1,
2 $CellContext`k + 2}];
ReplaceAll[$CellContext`formula, $CellContext`rul]], \
$CellContext`setpl = {
"p", "q", "r", "r", "p", "p", "q", "r", "r", "q", "q",
"p"}, $CellContext`Convert[
Pattern[$CellContext`p,
Blank[]]] := Condition[$CellContext`p,
AtomQ[$CellContext`p]], $CellContext`Convert[{
Pattern[$CellContext`p,
Blank[]],
Pattern[$CellContext`q,
Blank[]]}] := StringJoin["E",
$CellContext`Convert[$CellContext`p],
$CellContext`Convert[$CellContext`q]], $CellContext`theq[
Pattern[$CellContext`formula,
Blank[]]] :=
Module[{$CellContext`expr = $CellContext`formula, $CellContext`theorem =
True, $CellContext`mapmatch, $CellContext`pos, $CellContext`subs, \
$CellContext`formule}, $CellContext`formule = {
$CellContext`Convert[$CellContext`expr]}; While[
And[$CellContext`theorem,
Not[
MatchQ[$CellContext`expr,
Condition[{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`x,
Blank[]]},
AtomQ[$CellContext`x]]]]], $CellContext`mapmatch =
Map[MatchQ[$CellContext`expr, #]& , $CellContext`rules1]; \
$CellContext`pos = Position[$CellContext`mapmatch, True]; If[
Not[
MemberQ[$CellContext`mapmatch, True]], $CellContext`theorem =
False, $CellContext`subs = $CellContext`Sub[$CellContext`expr,
Part[$CellContext`pos, 1, 1]]; $CellContext`expr =
ReplaceAll[$CellContext`expr,
Part[$CellContext`rules,
Part[$CellContext`pos, 1, 1]]]; $CellContext`formule =
Append[$CellContext`formule,
Row[{
$CellContext`Convert[$CellContext`expr], ", ",
Part[$CellContext`pos, 1, 1],
MapAt[$CellContext`Convert, $CellContext`subs,
Table[{$CellContext`i, 2}, {$CellContext`i, 1,
Length[$CellContext`subs]}]]}]]]]; Column[{
Style[
Column[$CellContext`formule], "MR"], "",
Text[
If[$CellContext`theorem, "The formula is a tautology.",
"The formula is not a tautology."]]}]], $CellContext`rules1 = {
Condition[{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]}},
AtomQ[$CellContext`x]], {{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]},
Pattern[$CellContext`z,
Blank[]]},
Condition[{
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]],
Condition[{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]],
Condition[{
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]]}, \
$CellContext`OccursQ[
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]] := If[
AtomQ[$CellContext`y], $CellContext`x === $CellContext`y,
MemberQ[
Flatten[$CellContext`y], $CellContext`x]], $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 1] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 2] := {$CellContext`x ->
Part[$CellContext`expr, 1, 1], $CellContext`y ->
Part[$CellContext`expr, 1, 2], $CellContext`z ->
Part[$CellContext`expr, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 3] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 1, 1], $CellContext`z ->
Part[$CellContext`expr, 2, 1, 2], $CellContext`w ->
Part[$CellContext`expr, 2, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 4] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 1], $CellContext`z ->
Part[$CellContext`expr, 2, 2]}, $CellContext`Sub[
Pattern[$CellContext`expr,
Blank[]], 5] := {$CellContext`x ->
Part[$CellContext`expr, 1], $CellContext`y ->
Part[$CellContext`expr, 2, 1, 1], $CellContext`z ->
Part[$CellContext`expr, 2, 1, 2], $CellContext`w ->
Part[$CellContext`expr, 2, 2]}, $CellContext`rules = {{
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]}} :> Condition[$CellContext`y,
AtomQ[$CellContext`x]], {{
Pattern[$CellContext`x,
Blank[]],
Pattern[$CellContext`y,
Blank[]]},
Pattern[$CellContext`z,
Blank[]]} :> {$CellContext`x, {$CellContext`y, $CellContext`z}}, {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :>
Condition[{$CellContext`x, {$CellContext`y, {$CellContext`z, \
$CellContext`w}}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]], {
Pattern[$CellContext`x,
Blank[]], {
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]}} :>
Condition[{$CellContext`x, {$CellContext`z, $CellContext`y}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]], {
Pattern[$CellContext`x,
Blank[]], {{
Pattern[$CellContext`y,
Blank[]],
Pattern[$CellContext`z,
Blank[]]},
Pattern[$CellContext`w,
Blank[]]}} :>
Condition[{$CellContext`x, {$CellContext`z, {$CellContext`y, \
$CellContext`w}}},
And[
AtomQ[$CellContext`x],
$CellContext`OccursQ[$CellContext`x, $CellContext`z],
Not[
$CellContext`OccursQ[$CellContext`x, $CellContext`y]]]]}, \
$CellContext`rulesE = {
"1. ExExy~y", "2. EExyz~ExEyz", "3. ExEEyzw~ExEyEzw",
"4. ExEyz~ExEzy", "5. ExEEyzw~ExEzEyw"}}; Typeset`initDone$$ = True),
SynchronousInitialization->True,
UnsavedVariables:>{Typeset`initDone$$},
UntrackedVariables:>{Typeset`size$$}], "Manipulate",
Deployed->True,
StripOnInput->False],
Manipulate`InterpretManipulate[1]]], "Output",
CellID->544441333]
}, Open ]],
Cell[CellGroupData[{
Cell["", "DetailsSection"],
Cell["\<\
The equivalential calculus is a subsystem of propositional calculus with \
equivalence as the only connective. In 1929 Le\:015bniewski recognized that \
the equivalential calculus could be axiomatized. He used two axioms and the \
rules of detachment and substitution. He also observed that a formula of \
propositional calculus in which equivalence was the only propositional \
function was a tautology if and only if each propositional letter has an even \
number of appearances in it.\
\>", "DetailNotes",
CellChangeTimes->{{3.564057262546875*^9, 3.564057268828125*^9}, {
3.564057305609375*^9, 3.564057306984375*^9}, {3.564057371328125*^9,
3.564057785734375*^9}, 3.564058338609375*^9, 3.5640767885*^9, {
3.564077079828125*^9, 3.5640771281875*^9}, {3.56407716021875*^9,
3.564077162109375*^9}, {3.56407720590625*^9, 3.56407739903125*^9}, {
3.56407751065625*^9, 3.56407765771875*^9}, {3.56407788971875*^9,
3.564077934609375*^9}, {3.564078234875*^9, 3.564078365453125*^9}, {
3.5640784055625*^9, 3.564078485828125*^9}, {3.56407851671875*^9,
3.56407864378125*^9}, {3.56407947665625*^9, 3.56407956734375*^9}, {
3.56422950715625*^9, 3.564229509140625*^9}, {3.564229896265625*^9,
3.564229970125*^9}, {3.564230311140625*^9, 3.5642303643125*^9}, {
3.565127425911615*^9, 3.565127428224704*^9}, 3.565127536871583*^9, {
3.565127578492996*^9, 3.565127599965611*^9}, {3.566131777007716*^9,
3.566131777257316*^9}, {3.566132175010516*^9, 3.566132175369316*^9}, {
3.566134142580193*^9, 3.566134143079393*^9}},
CellID->265751097],
Cell[TextData[{
"In 1932 Wajsberg showed that the calculus can be based on a single axiom. \
In 1933 \[CapitalLSlash]ukasiewicz found the shortest axiom ",
StyleBox["EEEpqErsEtu", "MR"],
" and gave a simple completeness proof. He derived certain tautologies, such \
as ",
StyleBox["EEEpqrEpEqr", "MR"],
", which were used as rules. The rule ",
StyleBox["EExyz", "MR"],
"~",
StyleBox["ExEyz", "MR"],
" says that a formula of the form ",
StyleBox["EExyz", "MR"],
" is equivalent to ",
StyleBox["ExEyz", "MR"],
". A formula of the calculus is a tautology if it is deductively equivalent \
to ",
StyleBox["Exx", "MR"],
", where ",
StyleBox["x", "MR"],
" is a propositional variable [1]. The realization of the completeness \
theorem as a Prolog program was given in [2]."
}], "DetailNotes",
CellChangeTimes->{{3.564057262546875*^9, 3.564057268828125*^9}, {
3.564057305609375*^9, 3.564057306984375*^9}, {3.564057371328125*^9,
3.564057785734375*^9}, 3.564058338609375*^9, 3.5640767885*^9, {
3.564077079828125*^9, 3.5640771281875*^9}, {3.56407716021875*^9,
3.564077162109375*^9}, {3.56407720590625*^9, 3.56407739903125*^9}, {
3.56407751065625*^9, 3.56407765771875*^9}, {3.56407788971875*^9,
3.564077934609375*^9}, {3.564078234875*^9, 3.564078365453125*^9}, {
3.5640784055625*^9, 3.564078485828125*^9}, {3.56407851671875*^9,
3.56407864378125*^9}, {3.56407947665625*^9, 3.56407956734375*^9}, {
3.56422950715625*^9, 3.564229509140625*^9}, {3.564229896265625*^9,
3.564229970125*^9}, {3.564230311140625*^9, 3.5642303643125*^9}, {
3.565127425911615*^9, 3.565127428224704*^9}, 3.565127536871583*^9, {
3.565127578492996*^9, 3.565127599965611*^9}, {3.566131777007716*^9,
3.566131777257316*^9}, {3.566132175010516*^9, 3.566132175369316*^9}, {
3.566134142580193*^9, 3.566134143032593*^9}, 3.5661341753089933`*^9,
3.566144151773443*^9},
CellID->59854584],
Cell["\<\
In 1981 Hafner gave a more complicated completeness proof showing the proof \
length (the number of proof steps) is linear in formula size [3].\
\>", "DetailNotes",
CellChangeTimes->{{3.564078663609375*^9, 3.56407882775*^9}, {
3.56422985978125*^9, 3.56422986365625*^9}, {3.565127693420207*^9,
3.565127694240055*^9}, {3.5661321780057163`*^9, 3.566132178083716*^9}},
CellID->44558525],
Cell["References", "DetailNotes",
CellChangeTimes->{{3.566131859984116*^9, 3.5661318614505157`*^9}},
CellID->120051664],
Cell[TextData[{
"[1] J. \[CapitalLSlash]ukasiewicz, \"The Equivalential Calculus,\" in ",
StyleBox["Polish Logic (1920\[Dash]1939)",
FontSlant->"Italic"],
", S. McCall, ed., Oxfordk: Clarendon Press, 1967 pp. 88\[Dash]115."
}], "DetailNotes",
CellChangeTimes->{{3.5640577915625*^9, 3.564057970421875*^9}, {
3.5642294971875*^9, 3.564229514328125*^9}, 3.565127559475412*^9, {
3.565127950833385*^9, 3.56512798535822*^9}, {3.5651281064344587`*^9,
3.56512812462225*^9}, {3.566131878641716*^9, 3.5661318897489157`*^9}, {
3.566133074434467*^9, 3.56613307855284*^9}, {3.566133121514965*^9,
3.5661331315925007`*^9}, {3.5661331952244925`*^9, 3.5661332016048517`*^9}},
CellID->148142249],
Cell[TextData[{
"[2] I. Hafner, \"The Completeness Theorem of Equivalential Calculus as \
Prolog Program,\" ",
StyleBox["Logic Programming Newsletter",
FontSlant->"Italic"],
", May 1987 pp. 7\[Dash]8."
}], "DetailNotes",
CellChangeTimes->{{3.5642296681875*^9, 3.56422986946875*^9},
3.56423039371875*^9, {3.565128179758849*^9, 3.565128198996766*^9},
3.566131920902116*^9, {3.5661321883641157`*^9, 3.5661321885045156`*^9}, {
3.566133404139193*^9, 3.566133404388793*^9}},
CellID->619662668],
Cell[TextData[{
"[3] I. Hafner, \"On Proof Length in the Equivalential Calculus,\" ",
StyleBox["Glasnik Matemati\[CHacek]ki",
FontSlant->"Italic"],
", ",
StyleBox["15",
FontWeight->"Bold"],
"(35), 1980 pp. 233\[Dash]242."
}], "DetailNotes",
CellChangeTimes->{{3.564229516296875*^9, 3.564229665671875*^9}, {
3.565128131520069*^9, 3.565128168452834*^9}, {3.566131896285316*^9,
3.5661319077981157`*^9}, {3.566132190438916*^9, 3.566132190610516*^9}},
CellID->263625051],
Cell[TextData[{
"[4] S. Wolfram, ",
StyleBox["A New Kind of Science",
FontSlant->"Italic"],
", Champaign, IL: Wolfram Media, 2002 p. 1170e. "
}], "DetailNotes",
CellChangeTimes->{{3.565125774135565*^9, 3.565125785013166*^9}},
CellID->2028368939]
}, Open ]],
Cell[CellGroupData[{
Cell["", "ControlSuggestionsSection"],
Cell[BoxData[
TooltipBox[
RowBox[{
CheckboxBox[False], Cell[" Resize Images"]}],
"\"Click inside an image to reveal its orange resize frame.\\nDrag any of \
the orange resize handles to resize the image.\"",
TooltipDelay->0.35]], "ControlSuggestions",
FontFamily->"Verdana",
CellTags->"ResizeImages"],
Cell[BoxData[
TooltipBox[
RowBox[{
CheckboxBox[False], Cell[" Rotate and Zoom in 3D"]}],
RowBox[{
"\"Drag a 3D graphic to rotate it. Starting the drag near the center \
tumbles\\nthe graphic; starting near a corner turns it parallel to the plane \
of the screen.\\nHold down \"",
FrameBox[
"Ctrl", Background -> GrayLevel[0.9], FrameMargins -> 2, FrameStyle ->
GrayLevel[0.9]], "\" (or \"",
FrameBox[
"Cmd", Background -> GrayLevel[0.9], FrameMargins -> 2, FrameStyle ->
GrayLevel[0.9]], "\" on Mac) and drag up and down to zoom.\""}],
TooltipDelay->0.35]], "ControlSuggestions",
FontFamily->"Verdana",
CellTags->"RotateAndZoomIn3D"],
Cell[BoxData[
TooltipBox[
RowBox[{
CheckboxBox[False], Cell[" Drag Locators"]}],
RowBox[{"\"Drag any locator (\"",
GraphicsBox[
LocatorBox[
Scaled[{0.5, 0.5}]], ImageSize -> 20],
"\", etc.) to move it around.\""}],
TooltipDelay->0.35]], "ControlSuggestions",
FontFamily->"Verdana",
CellTags->"DragLocators"],
Cell[BoxData[
TooltipBox[
RowBox[{
CheckboxBox[False], Cell[" Create and Delete Locators"]}],
RowBox[{"\"Insert a new locator in the graphic by holding down the \"",
FrameBox[
"Alt", Background -> GrayLevel[0.9], FrameMargins -> 2, FrameStyle ->
GrayLevel[0.9]],
"\" key\\nand clicking where you want it to be. Delete a locator by \
clicking it\\nwhile holding down the \"",
FrameBox[
"Alt", Background -> GrayLevel[0.9], FrameMargins -> 2, FrameStyle ->
GrayLevel[0.9]], "\" key.\""}],
TooltipDelay->0.35]], "ControlSuggestions",
FontFamily->"Verdana",
CellTags->"CreateAndDeleteLocators"],
Cell[BoxData[
TooltipBox[
RowBox[{
CheckboxBox[False], Cell[" Slider Zoom"]}],
RowBox[{"\"Hold down the \"",
FrameBox[
"Alt", Background -> GrayLevel[0.9], FrameMargins -> 2, FrameStyle ->
GrayLevel[0.9]],
"\" key while moving a slider to make fine adjustments in the slider \
value.\\nHold \"",
FrameBox[
"Ctrl", Background -> GrayLevel[0.9], FrameMargins -> 2, FrameStyle ->
GrayLevel[0.9]], "\" and/or \"",
FrameBox[
"Shift", Background -> GrayLevel[0.9], FrameMargins -> 2, FrameStyle ->
GrayLevel[0.9]], "\" at the same time as \"",
FrameBox[
"Alt", Background -> GrayLevel[0.9], FrameMargins -> 2, FrameStyle ->
GrayLevel[0.9]], "\" to make ever finer adjustments.\""}],
TooltipDelay->0.35]], "ControlSuggestions",
FontFamily->"Verdana",
CellTags->"SliderZoom"],
Cell[BoxData[
TooltipBox[
RowBox[{
CheckboxBox[False], Cell[" Gamepad Controls"]}],
"\"Control this Demonstration with a gamepad or other\\nhuman interface \
device connected to your computer.\"",
TooltipDelay->0.35]], "ControlSuggestions",
CellChangeTimes->{3.35696210375764*^9, 3.3895522232313623`*^9},
FontFamily->"Verdana",
CellTags->"GamepadControls"],
Cell[BoxData[
TooltipBox[
RowBox[{
CheckboxBox[False], Cell[" Automatic Animation"]}],
RowBox[{"\"Animate a slider in this Demonstration by clicking the\"",
AdjustmentBox[
Cell[
GraphicsData[
"CompressedBitmap",
"eJzzTSzJSM1NLMlMTlRwL0osyMhMLlZwyy8CCjEzMjAwcIKwAgOI/R/IhBKc\n\
/4EAyGAG0f+nTZsGwgysIJIRKsWKLAXGIHFmEpUgLADxWUAkI24jZs+eTaEt\n\
IG+wQKRmzJgBlYf5lhEA30OqWA=="], "Graphics", ImageSize -> {9, 9}, ImageMargins ->
0, CellBaseline -> Baseline], BoxBaselineShift -> 0.1839080459770115,
BoxMargins -> {{0., 0.}, {-0.1839080459770115, 0.1839080459770115}}],
"\"button\\nnext to the slider, and then clicking the play button that \
appears.\\nAnimate all controls by selecting \"",
StyleBox["Autorun", FontWeight -> "Bold"], "\" from the\"",
AdjustmentBox[
Cell[
GraphicsData[
"CompressedBitmap",
"eJyNULENwyAQfEySIlMwTVJlCGRFsosokeNtqBmDBagoaZjAI1C8/8GUUUC6\n\
57h7cQ8PvU7Pl17nUav7oj/TPH7V7b2QJAUAXBkKmCPRowxICy64bRvGGNF7\n\
X8CctGoDSN4xhIDGGDhzFXwUh3/ClBKrDQPmnGXtI6u0OOd+tZBVUqy1xSaH\n\
UqiK6pPe4XdEdAz6563tx/gejuORGMxJaz8mdpJn7hc="], "Graphics",
ImageSize -> {10, 10}, ImageMargins -> 0, CellBaseline -> Baseline],
BoxBaselineShift -> 0.1839080459770115,
BoxMargins -> {{0., 0.}, {-0.1839080459770115, 0.1839080459770115}}],
"\"menu.\""}],
TooltipDelay->0.35]], "ControlSuggestions",
FontFamily->"Verdana",
CellTags->"AutomaticAnimation"],
Cell[BoxData[
TooltipBox[
RowBox[{
CheckboxBox[False], Cell[" Bookmark Animation"]}],
RowBox[{
"\"See a prepared animation of this Demonstration by selecting\\n\"",
StyleBox["Animate Bookmarks", FontWeight -> "Bold"], "\" from the\"",
AdjustmentBox[
Cell[
GraphicsData[
"CompressedBitmap",
"eJyNULENwyAQfEySIlMwTVJlCGRFsosokeNtqBmDBagoaZjAI1C8/8GUUUC6\n\
57h7cQ8PvU7Pl17nUav7oj/TPH7V7b2QJAUAXBkKmCPRowxICy64bRvGGNF7\n\
X8CctGoDSN4xhIDGGDhzFXwUh3/ClBKrDQPmnGXtI6u0OOd+tZBVUqy1xSaH\n\
UqiK6pPe4XdEdAz6563tx/gejuORGMxJaz8mdpJn7hc="], "Graphics",
ImageSize -> {10, 10}, ImageMargins -> 0, CellBaseline -> Baseline],
BoxBaselineShift -> 0.1839080459770115,
BoxMargins -> {{0., 0.}, {-0.1839080459770115, 0.1839080459770115}}],
"\"menu.\""}],
TooltipDelay->0.35]], "ControlSuggestions",
FontFamily->"Verdana",
CellTags->"BookmarkAnimation"]
}, Open ]],
Cell[CellGroupData[{
Cell["", "SearchTermsSection"],
Cell["equivalential calculus", "SearchTerms",
CellChangeTimes->{{3.5640788870625*^9, 3.56407889565625*^9}},
CellID->150095177],
Cell["tautology", "SearchTerms",
CellChangeTimes->{{3.564079148828125*^9, 3.564079154171875*^9}},
CellID->35683761]
}, Open ]],
Cell[CellGroupData[{
Cell["", "RelatedLinksSection"],
Cell[TextData[ButtonBox["Propositional Calculus",
BaseStyle->"Hyperlink",
ButtonData->{
URL["http://mathworld.wolfram.com/PropositionalCalculus.html"], None},
ButtonNote->
"http://mathworld.wolfram.com/PropositionalCalculus.html"]], "RelatedLinks",\
CellChangeTimes->{{3.564079375296875*^9, 3.5640793753125*^9}},
CellID->135979115],
Cell[TextData[ButtonBox["Connective",
BaseStyle->"Hyperlink",
ButtonData->{
URL["http://mathworld.wolfram.com/Connective.html"], None},
ButtonNote->"http://mathworld.wolfram.com/Connective.html"]], "RelatedLinks",\
CellChangeTimes->{{3.5640794334375*^9, 3.5640794334375*^9}},
CellID->341954716]
}, Open ]],
Cell[CellGroupData[{
Cell["", "AuthorSection"],
Cell[TextData[{
"Contributed by: ",
ButtonBox["Izidor Hafner",
BaseStyle->"Hyperlink",
ButtonData->{
URL["http://demonstrations.wolfram.com/author.html?author=Izidor+Hafner"],
None},
ButtonNote->
"http://demonstrations.wolfram.com/author.html?author=Izidor+Hafner"]
}], "Author",
CellChangeTimes->{{3.56407886159375*^9, 3.564078867859375*^9}, {
3.564079163703125*^9, 3.564079165875*^9}}]
}, Open ]]
}, Open ]]
},
WindowSize->{740, 762},
WindowMargins->{{Automatic, 69}, {Automatic, 6}},
FrontEndVersion->"8.0 for Microsoft Windows (32-bit) (February 23, 2011)",
StyleDefinitions->FrontEnd`FileName[{"Wolfram"}, "Demonstration.nb",
CharacterEncoding -> "WindowsEastEurope"]
]
(* End of Notebook Content *)
(* Internal cache information *)
(*CellTagsOutline
CellTagsIndex->{
"ResizeImages"->{
Cell[128235, 3141, 312, 8, 29, "ControlSuggestions",
CellTags->"ResizeImages"]},
"RotateAndZoomIn3D"->{
Cell[128550, 3151, 678, 16, 29, "ControlSuggestions",
CellTags->"RotateAndZoomIn3D"]},
"DragLocators"->{
Cell[129231, 3169, 340, 11, 29, "ControlSuggestions",
CellTags->"DragLocators"]},
"CreateAndDeleteLocators"->{
Cell[129574, 3182, 637, 15, 29, "ControlSuggestions",
CellTags->"CreateAndDeleteLocators"]},
"SliderZoom"->{
Cell[130214, 3199, 844, 21, 29, "ControlSuggestions",
CellTags->"SliderZoom"]},
"GamepadControls"->{
Cell[131061, 3222, 369, 9, 29, "ControlSuggestions",
CellTags->"GamepadControls"]},
"AutomaticAnimation"->{
Cell[131433, 3233, 1464, 31, 29, "ControlSuggestions",
CellTags->"AutomaticAnimation"]},
"BookmarkAnimation"->{
Cell[132900, 3266, 908, 21, 29, "ControlSuggestions",
CellTags->"BookmarkAnimation"]}
}
*)
(*CellTagsIndex
CellTagsIndex->{
{"ResizeImages", 135729, 3357},
{"RotateAndZoomIn3D", 135839, 3360},
{"DragLocators", 135950, 3363},
{"CreateAndDeleteLocators", 136067, 3366},
{"SliderZoom", 136182, 3369},
{"GamepadControls", 136289, 3372},
{"AutomaticAnimation", 136403, 3375},
{"BookmarkAnimation", 136521, 3378}
}
*)
(*NotebookFileOutline
Notebook[{
Cell[CellGroupData[{
Cell[579, 22, 181, 2, 104, "DemoTitle"],
Cell[CellGroupData[{
Cell[785, 28, 33, 0, 266, "InitializationSection"],
Cell[821, 30, 1876, 61, 68, "Input",
InitializationCell->True,
CellID->8114744],
Cell[2700, 93, 385, 9, 27, "Input",
InitializationCell->True,
CellID->132417912],
Cell[3088, 104, 3085, 93, 68, "Input",
InitializationCell->True,
CellID->45531902],
Cell[6176, 199, 1908, 61, 108, "Input",
InitializationCell->True,
CellID->750369280],
Cell[8087, 262, 1558, 45, 68, "Input",
InitializationCell->True,
CellID->168982622],
Cell[9648, 309, 1922, 51, 88, "Input",
InitializationCell->True,
CellID->155615391],
Cell[11573, 362, 398, 10, 27, "Input",
InitializationCell->True,
CellID->17641989],
Cell[11974, 374, 1647, 44, 88, "Input",
InitializationCell->True,
CellID->521444088],
Cell[13624, 420, 759, 20, 48, "Input",
InitializationCell->True,
CellID->479318433],
Cell[14386, 442, 2515, 66, 108, "Input",
InitializationCell->True,
CellID->542360971],
Cell[16904, 510, 2681, 82, 88, "Input",
InitializationCell->True,
CellID->474890314],
Cell[19588, 594, 435, 11, 48, "Input",
InitializationCell->True,
CellID->115710270],
Cell[20026, 607, 1859, 56, 88, "Input",
InitializationCell->True,
CellID->98096639],
Cell[21888, 665, 5466, 121, 228, "Input",
InitializationCell->True,
CellID->259145725],
Cell[27357, 788, 3595, 113, 168, "Input",
InitializationCell->True,
CellID->101636556]
}, Open ]],
Cell[CellGroupData[{
Cell[30989, 906, 29, 0, 230, "ManipulateSection"],
Cell[CellGroupData[{
Cell[31043, 910, 5111, 115, 428, "Input"],
Cell[36157, 1027, 16639, 378, 547, "Output",
CellID->1958622864]
}, Open ]]
}, Open ]],
Cell[CellGroupData[{
Cell[52845, 1411, 36, 0, 166, "ManipulateCaptionSection"],
Cell[52884, 1413, 1012, 18, 53, "ManipulateCaption"],
Cell[53899, 1433, 163, 4, 22, "ManipulateCaption",
CellID->284197905],
Cell[54065, 1439, 210, 3, 22, "ManipulateCaption",
CellID->49185482],
Cell[54278, 1444, 953, 15, 37, "ManipulateCaption",
CellID->629924060],
Cell[55234, 1461, 319, 5, 22, "ManipulateCaption",
CellID->109221385],
Cell[55556, 1468, 204, 5, 22, "ManipulateCaption",
CellID->26379133]
}, Open ]],
Cell[CellGroupData[{
Cell[55797, 1478, 28, 0, 168, "ThumbnailSection"],
Cell[55828, 1480, 16562, 377, 547, "Output",
CellID->138927251]
}, Open ]],
Cell[CellGroupData[{
Cell[72427, 1862, 28, 0, 138, "SnapshotsSection"],
Cell[72458, 1864, 16561, 377, 547, "Output",
CellID->635583268],
Cell[89022, 2243, 16557, 377, 547, "Output",
CellID->664325098],
Cell[105582, 2622, 16553, 377, 547, "Output",
CellID->544441333]
}, Open ]],
Cell[CellGroupData[{
Cell[122172, 3004, 26, 0, 332, "DetailsSection"],
Cell[122201, 3006, 1572, 24, 79, "DetailNotes",
CellID->265751097],
Cell[123776, 3032, 1906, 39, 96, "DetailNotes",
CellID->59854584],
Cell[125685, 3073, 399, 7, 35, "DetailNotes",
CellID->44558525],
Cell[126087, 3082, 121, 2, 21, "DetailNotes",
CellID->120051664],
Cell[126211, 3086, 700, 12, 36, "DetailNotes",
CellID->148142249],
Cell[126914, 3100, 505, 11, 36, "DetailNotes",
CellID->619662668],
Cell[127422, 3113, 481, 12, 36, "DetailNotes",
CellID->263625051],
Cell[127906, 3127, 252, 7, 21, "DetailNotes",
CellID->2028368939]
}, Open ]],
Cell[CellGroupData[{
Cell[128195, 3139, 37, 0, 127, "ControlSuggestionsSection"],
Cell[128235, 3141, 312, 8, 29, "ControlSuggestions",
CellTags->"ResizeImages"],
Cell[128550, 3151, 678, 16, 29, "ControlSuggestions",
CellTags->"RotateAndZoomIn3D"],
Cell[129231, 3169, 340, 11, 29, "ControlSuggestions",
CellTags->"DragLocators"],
Cell[129574, 3182, 637, 15, 29, "ControlSuggestions",
CellTags->"CreateAndDeleteLocators"],
Cell[130214, 3199, 844, 21, 29, "ControlSuggestions",
CellTags->"SliderZoom"],
Cell[131061, 3222, 369, 9, 29, "ControlSuggestions",
CellTags->"GamepadControls"],
Cell[131433, 3233, 1464, 31, 29, "ControlSuggestions",
CellTags->"AutomaticAnimation"],
Cell[132900, 3266, 908, 21, 29, "ControlSuggestions",
CellTags->"BookmarkAnimation"]
}, Open ]],
Cell[CellGroupData[{
Cell[133845, 3292, 30, 0, 155, "SearchTermsSection"],
Cell[133878, 3294, 128, 2, 21, "SearchTerms",
CellID->150095177],
Cell[134009, 3298, 117, 2, 21, "SearchTerms",
CellID->35683761]
}, Open ]],
Cell[CellGroupData[{
Cell[134163, 3305, 31, 0, 141, "RelatedLinksSection"],
Cell[134197, 3307, 342, 8, 21, "RelatedLinks",
CellID->135979115],
Cell[134542, 3317, 303, 7, 21, "RelatedLinks",
CellID->341954716]
}, Open ]],
Cell[CellGroupData[{
Cell[134882, 3329, 25, 0, 141, "AuthorSection"],
Cell[134910, 3331, 410, 11, 21, "Author"]
}, Open ]]
}, Open ]]
}
]
*)
(* End of internal cache information *)