# HG changeset patch # User Christian Urban # Date 1361250693 0 # Node ID 455411d69c120775b6e4fceda3c928b51e5e1cbc # Parent 2fad78b479a33f3fe9596abf851e01a71eb220e0 added link and comment to fourth edition of Boolos diff -r 2fad78b479a3 -r 455411d69c12 Paper/Paper.thy --- a/Paper/Paper.thy Tue Feb 19 04:56:33 2013 +0000 +++ b/Paper/Paper.thy Tue Feb 19 05:11:33 2013 +0000 @@ -1398,7 +1398,9 @@ Turing machines, an unexpected outcome of our work is that we identified an inconsistency in their use of a definition. This is unexpected since \cite{Boolos87} is a classic textbook which has - undergone several editions (we used the fifth edition). The central + undergone several editions (we used the fifth edition; the material + containing the inconsistency was introduced in the fourth edition + \cite{BoolosFourth}). The central idea about Turing machines is that when started with standard tapes they compute a partial arithmetic function. The inconsitency arises when they define the case when this function should \emph{not} return a diff -r 2fad78b479a3 -r 455411d69c12 Paper/document/root.bib --- a/Paper/document/root.bib Tue Feb 19 04:56:33 2013 +0000 +++ b/Paper/document/root.bib Tue Feb 19 05:11:33 2013 +0000 @@ -74,6 +74,14 @@ year = {2007} } +@book{BoolosFourth, + author = {G.~Boolos and J.~P.~Burgess and R.~C.~Jeffrey}, + title = {{C}omputability and {L}ogic (4th~ed.)}, + publisher = {Cambridge University Press}, + year = {2002} +} + + @inproceedings{WuZhangUrban11, author = {C.~Wu and X.~Zhang and C.~Urban}, title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions diff -r 2fad78b479a3 -r 455411d69c12 ROOT --- a/ROOT Tue Feb 19 04:56:33 2013 +0000 +++ b/ROOT Tue Feb 19 05:11:33 2013 +0000 @@ -10,3 +10,7 @@ "thys/Recursive" "thys/UF" "thys/UTM" + +session ITP = UTM + + theories + "Paper/Paper" \ No newline at end of file diff -r 2fad78b479a3 -r 455411d69c12 paper.pdf Binary file paper.pdf has changed