# HG changeset patch # User paulson # Date 951298897 -3600 # Node ID 95c022a866ca4c207a8b65124ad1f7e403b2f411 # Parent 0a319c5746eb218fca219a54067381c11115234b new reference korf85 diff -r 0a319c5746eb -r 95c022a866ca doc-src/Ref/classical.tex --- a/doc-src/Ref/classical.tex Tue Feb 22 21:53:17 2000 +0100 +++ b/doc-src/Ref/classical.tex Wed Feb 23 10:41:37 2000 +0100 @@ -470,10 +470,11 @@ successively to~20, \texttt{Blast.depth_tac} applies a user-supplied search bound. \begin{ttdescription} \item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove - subgoal~$i$ using iterative deepening to increase the search bound. + subgoal~$i$, increasing the search bound using iterative + deepening~\cite{korf85}. \item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries - to prove subgoal~$i$ using a search bound of $lim$. Often a slow + to prove subgoal~$i$ using a search bound of $lim$. Sometimes a slow proof using \texttt{blast_tac} can be made much faster by supplying the successful search bound to this tactic instead. diff -r 0a319c5746eb -r 95c022a866ca doc-src/manual.bib --- a/doc-src/manual.bib Tue Feb 22 21:53:17 2000 +0100 +++ b/doc-src/manual.bib Wed Feb 23 10:41:37 2000 +0100 @@ -18,6 +18,7 @@ @string{Edinburgh="Dept. Comp. Sci., Univ. Edinburgh"} %journals +@string{AI="Artificial Intelligence"} @string{FAC="Formal Aspects Comput."} @string{JAR="J. Auto. Reas."} @string{JCS="J. Comput. Secur."} @@ -390,9 +391,20 @@ title = {Locales: A Sectioning Concept for {Isabelle}}, crossref = {tphols99}} -@book{Knuth3-75,author={Donald E. Knuth}, -title={The Art of Computer Programming, Volume 3: Sorting and Searching}, -publisher={Addison-Wesley},year=1975} +@book{Knuth3-75, + author={Donald E. Knuth}, + title={The Art of Computer Programming, Volume 3: Sorting and Searching}, + publisher={Addison-Wesley}, + year=1975} + +@Article{korf85, + author = {R. E. Korf}, + title = {Depth-First Iterative-Deepening: an Optimal Admissible + Tree Search}, + journal = AI, + year = 1985, + volume = 27, + pages = {97-109}} @Book{kunen80, author = {Kenneth Kunen},