(************** Content-type: application/mathematica **************
CreatedBy='Mathematica 5.1'
Mathematica-Compatible Notebook
This notebook can be used with any Mathematica-compatible
application, such as Mathematica, MathReader or Publicon. The data
for the notebook starts with the line containing stars above.
To get the notebook into a Mathematica-compatible application, do
one of the following:
* Save the data starting with the line of stars above into a file
with a name ending in .nb, then open the file inside the
application;
* Copy the data starting with the line of stars above to the
clipboard, then use the Paste menu command inside the application.
Data for notebooks contains only printable 7-bit ASCII and can be
sent directly in email or through ftp in text mode. Newlines can be
CR, LF or CRLF (Unix, Macintosh or MS-DOS style).
NOTE: If you modify the data for this notebook not in a Mathematica-
compatible application, you must delete the line below containing
the word CacheID, otherwise Mathematica-compatible applications may
try to use invalid cache data.
For more information on notebooks and Mathematica-compatible
applications, contact Wolfram Research:
web: http://www.wolfram.com
email: info@wolfram.com
phone: +1-217-398-0700 (U.S.)
Notebook reader applications are available free of charge from
Wolfram Research.
*******************************************************************)
(*CacheID: 232*)
(*NotebookFileLineBreakTest
NotebookFileLineBreakTest*)
(*NotebookOptionsPosition[ 7235, 225]*)
(*NotebookOutlinePosition[ 7899, 248]*)
(* CellTagsIndexPosition[ 7855, 244]*)
(*WindowFrame->Normal*)
Notebook[{
Cell[CellGroupData[{
Cell["\<\
Case study in non-clausal proving:
Irrationality of the square root of a prime\
\>", "Subsection"],
Cell["Tudor Jebelean, Dec 2007", "Text",
FontWeight->"Bold"],
Cell[TextData[{
"Goal: We want to prove that ",
Cell[BoxData[
\(TraditionalForm\`\@p\)]],
" is not rational for any prime number ",
Cell[BoxData[
\(TraditionalForm\`p\)]],
"."
}], "Text"],
Cell[TextData[{
"The necessary assumptions are selected from the theory of numbers, and \
some of them are even instantiated appropriately with ",
Cell[BoxData[
\(TraditionalForm\`p\)]],
"."
}], "Text"],
Cell[CellGroupData[{
Cell["\<\
Version 0: Level saturation using unit generalized resolution\
\>", "Subsubsection"],
Cell[TextData[{
"The inference rule (",
StyleBox["unit generalized resolution",
FontWeight->"Bold"],
") is: If a ground atom \[Alpha] matches a negative subformula of a \
universal formula \[CurlyPhi], then obtain a new formula by replacing in the \
respective instance of \[CurlyPhi] the occurrences of \[Alpha] with ",
StyleBox["True",
FontSlant->"Italic"],
StyleBox[", and then by simplifying the truth constants.",
FontVariations->{"CompatibilityType"->0}]
}], "Text",
TextAlignment->Left,
TextJustification->1],
Cell[TextData[{
"The strategy (",
StyleBox["level saturation",
FontWeight->"Bold"],
") consists in saturating each level sequentially by obtaining all new \
formulae (using the inference rule above) from the formulae at the previous \
levels. Thus:\n - ",
StyleBox["level 0",
FontSlant->"Italic"],
" contains all the assumptions of the initial proof situation;\n - ",
StyleBox["level 1",
FontSlant->"Italic"],
" contains all formulae wich can be obtained by this inference rule using \
the formulae of ",
StyleBox["level 0;\n -",
FontSlant->"Italic"],
" ",
StyleBox["level 2",
FontSlant->"Italic"],
" contains all formulae which can be obtained by inferences among formulae \
at ",
StyleBox["level 1",
FontSlant->"Italic"],
" and among formulae at ",
StyleBox["level 1",
FontSlant->"Italic"],
" and ",
StyleBox["0",
FontSlant->"Italic"],
", etc.\n Level saturation is necessary in order to insure fairness: Each \
formula must be eventually used in the proof. For instance, if our set of \
assumptions contains: IsNat[a] and ",
Cell[BoxData[
\(TraditionalForm\`\[ForAll] \+x IsNat[x]\ \[DoubleLongRightArrow]\
IsNat[x\^2]\)]],
", then from these one can infer ",
Cell[BoxData[
\(TraditionalForm\`IsNat[a\^2]\)]],
", ",
Cell[BoxData[
\(TraditionalForm\`IsNat[a\^4]\)]],
", etc. That means one can use infinitely many times the universally \
quantified formula above, and the other universally quantified formulae are \
not used - although they may be necessary for a successful proof. "
}], "Text",
TextJustification->1],
Cell[TextData[{
" ",
ButtonBox["Link to proof",
ButtonData:>{"proof-sqrt2-version0-complete.nb", None},
ButtonStyle->"Hyperlink"],
": 600 formulae, 50 minutes"
}], "Text"]
}, Open ]],
Cell[CellGroupData[{
Cell["Version 1: Use also propositional saturation", "Subsubsection"],
Cell[TextData[{
"Propositional inferences are inferences which do not require instantiation \
of a universally quantified formula. Such an inference is, for instance, the \
rule for ",
StyleBox["modus ponens",
FontSlant->"Italic"],
". Since only a finite number of such inferences can be performed, we can \
allow, at each level of the saturation, the use of all possible propositional \
inferences, even if they use formulae generated at the respective level."
}], "Text"],
Cell["\<\
This is usually better because the last few inferences in the proof are \
usually propositional ones, thus one avoids few saturation levels at the end \
- which in fact usually contain most of the inferences.\
\>", "Text"],
Cell[TextData[{
" ",
ButtonBox["Link to proof",
ButtonData:>{"proof-sqrt2-version1-complete.nb", None},
ButtonStyle->"Hyperlink"],
": 350 formulae, 10 minutes"
}], "Text"]
}, Open ]],
Cell[CellGroupData[{
Cell["Version 2: Use also hyper-inferences", "Subsubsection"],
Cell[TextData[{
"Consider a quantified formula having the structure ",
Cell[BoxData[
\(TraditionalForm\`\[ForAll] \+x\)]],
"(A\[And]B\[And]C)\[DoubleLongRightArrow]D. In a typical proof, this \
formula will be used in order to infer a ground instance of D by using \
appropriate ground instances of the premises A, B, and C. Therefore, one \
should instantiate this formula only when having already compatible ground \
instances of the premises."
}], "Text"],
Cell["\<\
In order to apply this principle, we first analyse all universally quantified \
formulae and make a list of their negative atoms. A \"hyper-inference\" is \
performed when we have compatible ground atoms for all negative atoms of an \
universally quantified formula: in this case we replace their occurrences in \
the instatiated formula by True and we perform truth constant simplification.\
\
\>", "Text"],
Cell["\<\
This strategy is similar to a refinement of the resolution method which is \
called \"hyper-resolution\".\
\>", "Text"],
Cell[TextData[{
" ",
ButtonBox["Link to proof",
ButtonData:>{"proof-sqrt2-version2-complete.nb", None},
ButtonStyle->"Hyperlink"],
": hyper-resolution: 50 formulae, 3 minutes"
}], "Text"]
}, Open ]]
}, Open ]]
},
FrontEndVersion->"5.1 for Microsoft Windows",
ScreenRectangle->{{0, 1024}, {0, 670}},
WindowSize->{1014, 586},
WindowMargins->{{0, Automatic}, {Automatic, 0}},
Magnification->1.5
]
(*******************************************************************
Cached data follows. If you edit this Notebook file directly, not
using Mathematica, you must remove the line containing CacheID at
the top of the file. The cache data will then be recreated when
you save this file from within Mathematica.
*******************************************************************)
(*CellTagsOutline
CellTagsIndex->{}
*)
(*CellTagsIndex
CellTagsIndex->{}
*)
(*NotebookFileOutline
Notebook[{
Cell[CellGroupData[{
Cell[1776, 53, 108, 3, 82, "Subsection"],
Cell[1887, 58, 62, 1, 47, "Text"],
Cell[1952, 61, 209, 8, 47, "Text"],
Cell[2164, 71, 214, 6, 73, "Text"],
Cell[CellGroupData[{
Cell[2403, 81, 94, 2, 40, "Subsubsection"],
Cell[2500, 85, 541, 13, 99, "Text"],
Cell[3044, 100, 1632, 45, 289, "Text"],
Cell[4679, 147, 186, 6, 47, "Text"]
}, Open ]],
Cell[CellGroupData[{
Cell[4902, 158, 69, 0, 40, "Subsubsection"],
Cell[4974, 160, 483, 9, 125, "Text"],
Cell[5460, 171, 232, 4, 73, "Text"],
Cell[5695, 177, 185, 6, 47, "Text"]
}, Open ]],
Cell[CellGroupData[{
Cell[5917, 188, 61, 0, 40, "Subsubsection"],
Cell[5981, 190, 470, 9, 107, "Text"],
Cell[6454, 201, 417, 7, 125, "Text"],
Cell[6874, 210, 129, 3, 47, "Text"],
Cell[7006, 215, 201, 6, 47, "Text"]
}, Open ]]
}, Open ]]
}
]
*)
(*******************************************************************
End of Mathematica Notebook file.
*******************************************************************)