\relax 
\citation{Blackburn:ild}
\citation{Blackburn:rrars}
\citation{Tzakova:tcfhl}
\citation{Eijck02:hylotab}
\citation{Haskell98:rep}
\citation{Knuth:lp}
\citation{Areces:le}
\citation{AreBlaMar:hlcic}
\@writefile{toc}{\contentsline {paragraph}{Keywords:}{1}}
\@writefile{toc}{\contentsline {paragraph}{MSC codes:}{1}}
\@writefile{toc}{\contentsline {section}{\numberline {1}Hybrid Logic: Syntax and Semantics}{1}}
\citation{Blackburn:ild}
\citation{Blackburn:rrars}
\citation{Smullyan:fl}
\@writefile{toc}{\contentsline {section}{\numberline {2}A Tableau Calculus for ${\cal  HL}(@,\mathaccentV {breve}015{},\delimiter "3223379 )$}{2}}
\@writefile{toc}{\contentsline {paragraph}{Conjunctive rules ($\alpha $ rules)}{3}}
\@writefile{toc}{\contentsline {paragraph}{Disjunctive rules ($\beta $ rules)}{3}}
\@writefile{toc}{\contentsline {paragraph}{Negation rule}{3}}
\@writefile{toc}{\contentsline {paragraph}{$[{\scriptstyle \tmspace  +\medmuskip {.2222em}i\tmspace  +\medmuskip {.2222em} }]$ rules}{3}}
\@writefile{toc}{\contentsline {paragraph}{$\delimiter "426830A {\scriptstyle \tmspace  +\medmuskip {.2222em} i\tmspace  +\medmuskip {.2222em} }\delimiter "526930B $ rules}{3}}
\@writefile{toc}{\contentsline {paragraph}{$[{\scriptstyle \tmspace  +\medmuskip {.2222em} i\tmspace  +\medmuskip {.2222em}}]^{\tmspace  +\medmuskip {.2222em}\mathaccentV {breve}015{}}$ rules}{3}}
\@writefile{toc}{\contentsline {paragraph}{$\delimiter "426830A {\scriptstyle \tmspace  +\medmuskip {.2222em} i\tmspace  +\medmuskip {.2222em} }\delimiter "526930B ^{\mathaccentV {breve}015{}}$ rules}{3}}
\@writefile{toc}{\contentsline {paragraph}{Access rules}{4}}
\@writefile{toc}{\contentsline {paragraph}{Label rules}{4}}
\@writefile{toc}{\contentsline {paragraph}{Nominal substitution}{4}}
\@writefile{toc}{\contentsline {paragraph}{Inequality generation}{4}}
\@writefile{toc}{\contentsline {paragraph}{Binding rules}{4}}
\@writefile{toc}{\contentsline {paragraph}{Tableau Closure}{4}}
\@writefile{toc}{\contentsline {section}{\numberline {3}Examples of Refutation Proofs, for ${\cal  HL} (@)$}{4}}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Tableau refutation for (\G@refundefinedtrue \text  {\normalfont  \bfseries  ??}\GenericWarning  {               }{LaTeX Warning: Reference `Ex1' on page 5 undefined}).}}{5}}
\newlabel{FigEx1}{{1}{5}}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Tableau refutation for (\G@refundefinedtrue \text  {\normalfont  \bfseries  ??}\GenericWarning  {               }{LaTeX Warning: Reference `Ex1' on page 6 undefined}), without formula repetition.}}{6}}
\newlabel{FigEx1a}{{2}{6}}
\newlabel{Ex1}{{1}{7}}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Tableau refutation for $@m \neg ((\Diamond p \land \Diamond \neg p) \rightarrow (\Box (q \rightarrow i) \rightarrow \Diamond \neg q))$ .}}{7}}
\newlabel{FigEx2}{{3}{7}}
\citation{Tzakova:tcfhl}
\@writefile{toc}{\contentsline {section}{\numberline {4}Examples of Model Generation, for ${\cal  HL} (@)$}{8}}
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces Open tableau for $@m (\Diamond \Diamond m \land \neg \Diamond m)$.}}{8}}
\newlabel{FigRef1}{{4}{8}}
\@writefile{toc}{\contentsline {section}{\numberline {5}Examples of the treatment of $\delimiter "3223379 $}{8}}
\newlabel{ArrowEx2}{{2}{8}}
\@writefile{lof}{\contentsline {figure}{\numberline {5}{\ignorespaces Open tableau for $ @m (\Diamond i \land \Diamond j \land \Diamond k \land @ i \neg j \land @ j \neg k \land @ i \neg k)$.}}{9}}
\newlabel{FigRef2}{{5}{9}}
\@writefile{lof}{\contentsline {figure}{\numberline {6}{\ignorespaces Open tableau for $\Diamond (c \land \Diamond c \land \Box \Diamond c)$.}}{9}}
\newlabel{FigNewEx}{{6}{9}}
\@writefile{lof}{\contentsline {figure}{\numberline {7}{\ignorespaces Closed tableau for $@m \ \delimiter "3223379 x . \Box \Diamond x \land \neg (\Diamond \Box p \rightarrow p)$.}}{10}}
\newlabel{FigArrowEx1}{{7}{10}}
\@writefile{lof}{\contentsline {figure}{\numberline {8}{\ignorespaces Infinite tableau for (\G@refundefinedtrue \text  {\normalfont  \bfseries  ??}\GenericWarning  {               }{LaTeX Warning: Reference `ArrowEx2' on page 11 undefined}).}}{11}}
\newlabel{FigArrowEx2}{{8}{11}}
\@writefile{toc}{\contentsline {section}{\numberline {6}From Tableau Calculus to Proof Engine}{12}}
\newlabel{PP}{{6}{12}}
\@writefile{lof}{\contentsline {figure}{\numberline {9}{\ignorespaces Constraint Proof Engine for ${\cal  HL}(@,\mathaccentV {breve}015{},\delimiter "3223379 )$.}}{13}}
\newlabel{PPfig}{{9}{13}}
\@writefile{toc}{\contentsline {paragraph}{Closure, Success}{14}}
\@writefile{toc}{\contentsline {paragraph}{Selection Rule}{14}}
\@writefile{toc}{\contentsline {paragraph}{Search Rule}{14}}
\@writefile{toc}{\contentsline {paragraph}{Termination Condition}{14}}
\@writefile{toc}{\contentsline {section}{\numberline {7}Soundness, Fairness of Proof Engine, Completeness}{14}}
\newlabel{PPfair}{{2}{14}}
\@writefile{toc}{\contentsline {section}{\numberline {8}Adding the Universal Modality}{15}}
\@writefile{lof}{\contentsline {figure}{\numberline {10}{\ignorespaces Modified Constraint Proof Engine for ${\cal  HL}(@,\mathaccentV {breve}015{},\delimiter "3223379 ,A)$.}}{16}}
\newlabel{APEfig}{{10}{16}}
\newlabel{APEfair}{{5}{16}}
\@writefile{toc}{\contentsline {section}{\numberline {9}Tuning the Engine: Proof Procedures for Frame Classes}{16}}
\@writefile{toc}{\contentsline {section}{\numberline {10}Modifying the Calculus for Minimal Model Generation}{17}}
\@writefile{toc}{\contentsline {paragraph}{$\delimiter "426830A {\scriptstyle \tmspace  +\medmuskip {.2222em} i\tmspace  +\medmuskip {.2222em} }\delimiter "526930B $ rules, trial-and-error version}{17}}
\@writefile{toc}{\contentsline {paragraph}{$\delimiter "426830A {\scriptstyle \tmspace  +\medmuskip {.2222em} i\tmspace  +\medmuskip {.2222em} }\delimiter "526930B ^{\mathaccentV {breve}015{}}$ rules, trial-and-error version}{17}}
\citation{Benthem:panicl}
\newlabel{NinfConj}{{3}{18}}
\@writefile{toc}{\contentsline {section}{\numberline {11}Generation of Minimal Models Through Node Compression}{18}}
\@writefile{lof}{\contentsline {figure}{\numberline {11}{\ignorespaces Tableau for (\G@refundefinedtrue \text  {\normalfont  \bfseries  ??}\GenericWarning  {               }{LaTeX Warning: Reference `NinfConj' on page 19 undefined}).}}{19}}
\newlabel{FigNinfConj}{{11}{19}}
\@writefile{lof}{\contentsline {figure}{\numberline {12}{\ignorespaces Trial-and-error tableau for (\G@refundefinedtrue \text  {\normalfont  \bfseries  ??}\GenericWarning  {               }{LaTeX Warning: Reference `NinfConj' on page 20 undefined}).}}{20}}
\newlabel{FigTENinfConj}{{12}{20}}
\citation{Areces:le}
\citation{AreBlaMar:hlcic}
\citation{BlaRijVen:ml}
\@writefile{toc}{\contentsline {section}{\numberline {12}Deciding Some Fragments of ${\cal  HL}(\delimiter "3223379 ,\mathaccentV {breve}015{},@)$}{21}}
\newlabel{PdecidesAt}{{12}{21}}
\citation{Areces:le}
\citation{AreBlaMar:hlcic}
\citation{Marx02:nsas}
\citation{Graedel:otrpog}
\citation{Graedel:otrpog}
\citation{Graedel:otrpog}
\citation{Fitting:pmfmail}
\citation{Tzakova:tcfhl}
\citation{Blackburn:ild}
\citation{BlaBurWal:hydr01}
\@writefile{toc}{\contentsline {section}{\numberline {13}Related Work}{23}}
\@writefile{toc}{\contentsline {paragraph}{Comparison with other tableau systems}{23}}
\citation{Ohlbach88:arcfml}
\citation{EnjFar89:mricf}
\citation{AreNivRij:reso01}
\citation{AreHeg01:hylores}
\bibstyle{acm}
\bibdata{/home/jve/texmacros/mybibAG,/home/jve/texmacros/mybibHZ}
\@writefile{toc}{\contentsline {paragraph}{Comparison with resolution for hybrid logic}{24}}
\@writefile{toc}{\contentsline {paragraph}{Acknowledgement}{24}}