\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}}