packages feed

hylotab (empty) → 1.2.0

raw patch · 39 files changed

+3794/−0 lines, 39 filesdep +basedep +hylolibdep +mtlsetup-changed

Dependencies added: base, hylolib, mtl

Files

+ LICENSE view
@@ -0,0 +1,339 @@+                    GNU GENERAL PUBLIC LICENSE+                       Version 2, June 1991++ Copyright (C) 1989, 1991 Free Software Foundation, Inc.,+ 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA+ Everyone is permitted to copy and distribute verbatim copies+ of this license document, but changing it is not allowed.++                            Preamble++  The licenses for most software are designed to take away your+freedom to share and change it.  By contrast, the GNU General Public+License is intended to guarantee your freedom to share and change free+software--to make sure the software is free for all its users.  This+General Public License applies to most of the Free Software+Foundation's software and to any other program whose authors commit to+using it.  (Some other Free Software Foundation software is covered by+the GNU Lesser General Public License instead.)  You can apply it to+your programs, too.++  When we speak of free software, we are referring to freedom, not+price.  Our General Public Licenses are designed to make sure that you+have the freedom to distribute copies of free software (and charge for+this service if you wish), that you receive source code or can get it+if you want it, that you can change the software or use pieces of it+in new free programs; and that you know you can do these things.++  To protect your rights, we need to make restrictions that forbid+anyone to deny you these rights or to ask you to surrender the rights.+These restrictions translate to certain responsibilities for you if you+distribute copies of the software, or if you modify it.++  For example, if you distribute copies of such a program, whether+gratis or for a fee, you must give the recipients all the rights that+you have.  You must make sure that they, too, receive or can get the+source code.  And you must show them these terms so they know their+rights.++  We protect your rights with two steps: (1) copyright the software, and+(2) offer you this license which gives you legal permission to copy,+distribute and/or modify the software.++  Also, for each author's protection and ours, we want to make certain+that everyone understands that there is no warranty for this free+software.  If the software is modified by someone else and passed on, we+want its recipients to know that what they have is not the original, so+that any problems introduced by others will not reflect on the original+authors' reputations.++  Finally, any free program is threatened constantly by software+patents.  We wish to avoid the danger that redistributors of a free+program will individually obtain patent licenses, in effect making the+program proprietary.  To prevent this, we have made it clear that any+patent must be licensed for everyone's free use or not licensed at all.++  The precise terms and conditions for copying, distribution and+modification follow.++                    GNU GENERAL PUBLIC LICENSE+   TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION++  0. This License applies to any program or other work which contains+a notice placed by the copyright holder saying it may be distributed+under the terms of this General Public License.  The "Program", below,+refers to any such program or work, and a "work based on the Program"+means either the Program or any derivative work under copyright law:+that is to say, a work containing the Program or a portion of it,+either verbatim or with modifications and/or translated into another+language.  (Hereinafter, translation is included without limitation in+the term "modification".)  Each licensee is addressed as "you".++Activities other than copying, distribution and modification are not+covered by this License; they are outside its scope.  The act of+running the Program is not restricted, and the output from the Program+is covered only if its contents constitute a work based on the+Program (independent of having been made by running the Program).+Whether that is true depends on what the Program does.++  1. You may copy and distribute verbatim copies of the Program's+source code as you receive it, in any medium, provided that you+conspicuously and appropriately publish on each copy an appropriate+copyright notice and disclaimer of warranty; keep intact all the+notices that refer to this License and to the absence of any warranty;+and give any other recipients of the Program a copy of this License+along with the Program.++You may charge a fee for the physical act of transferring a copy, and+you may at your option offer warranty protection in exchange for a fee.++  2. You may modify your copy or copies of the Program or any portion+of it, thus forming a work based on the Program, and copy and+distribute such modifications or work under the terms of Section 1+above, provided that you also meet all of these conditions:++    a) You must cause the modified files to carry prominent notices+    stating that you changed the files and the date of any change.++    b) You must cause any work that you distribute or publish, that in+    whole or in part contains or is derived from the Program or any+    part thereof, to be licensed as a whole at no charge to all third+    parties under the terms of this License.++    c) If the modified program normally reads commands interactively+    when run, you must cause it, when started running for such+    interactive use in the most ordinary way, to print or display an+    announcement including an appropriate copyright notice and a+    notice that there is no warranty (or else, saying that you provide+    a warranty) and that users may redistribute the program under+    these conditions, and telling the user how to view a copy of this+    License.  (Exception: if the Program itself is interactive but+    does not normally print such an announcement, your work based on+    the Program is not required to print an announcement.)++These requirements apply to the modified work as a whole.  If+identifiable sections of that work are not derived from the Program,+and can be reasonably considered independent and separate works in+themselves, then this License, and its terms, do not apply to those+sections when you distribute them as separate works.  But when you+distribute the same sections as part of a whole which is a work based+on the Program, the distribution of the whole must be on the terms of+this License, whose permissions for other licensees extend to the+entire whole, and thus to each and every part regardless of who wrote it.++Thus, it is not the intent of this section to claim rights or contest+your rights to work written entirely by you; rather, the intent is to+exercise the right to control the distribution of derivative or+collective works based on the Program.++In addition, mere aggregation of another work not based on the Program+with the Program (or with a work based on the Program) on a volume of+a storage or distribution medium does not bring the other work under+the scope of this License.++  3. You may copy and distribute the Program (or a work based on it,+under Section 2) in object code or executable form under the terms of+Sections 1 and 2 above provided that you also do one of the following:++    a) Accompany it with the complete corresponding machine-readable+    source code, which must be distributed under the terms of Sections+    1 and 2 above on a medium customarily used for software interchange; or,++    b) Accompany it with a written offer, valid for at least three+    years, to give any third party, for a charge no more than your+    cost of physically performing source distribution, a complete+    machine-readable copy of the corresponding source code, to be+    distributed under the terms of Sections 1 and 2 above on a medium+    customarily used for software interchange; or,++    c) Accompany it with the information you received as to the offer+    to distribute corresponding source code.  (This alternative is+    allowed only for noncommercial distribution and only if you+    received the program in object code or executable form with such+    an offer, in accord with Subsection b above.)++The source code for a work means the preferred form of the work for+making modifications to it.  For an executable work, complete source+code means all the source code for all modules it contains, plus any+associated interface definition files, plus the scripts used to+control compilation and installation of the executable.  However, as a+special exception, the source code distributed need not include+anything that is normally distributed (in either source or binary+form) with the major components (compiler, kernel, and so on) of the+operating system on which the executable runs, unless that component+itself accompanies the executable.++If distribution of executable or object code is made by offering+access to copy from a designated place, then offering equivalent+access to copy the source code from the same place counts as+distribution of the source code, even though third parties are not+compelled to copy the source along with the object code.++  4. You may not copy, modify, sublicense, or distribute the Program+except as expressly provided under this License.  Any attempt+otherwise to copy, modify, sublicense or distribute the Program is+void, and will automatically terminate your rights under this License.+However, parties who have received copies, or rights, from you under+this License will not have their licenses terminated so long as such+parties remain in full compliance.++  5. You are not required to accept this License, since you have not+signed it.  However, nothing else grants you permission to modify or+distribute the Program or its derivative works.  These actions are+prohibited by law if you do not accept this License.  Therefore, by+modifying or distributing the Program (or any work based on the+Program), you indicate your acceptance of this License to do so, and+all its terms and conditions for copying, distributing or modifying+the Program or works based on it.++  6. Each time you redistribute the Program (or any work based on the+Program), the recipient automatically receives a license from the+original licensor to copy, distribute or modify the Program subject to+these terms and conditions.  You may not impose any further+restrictions on the recipients' exercise of the rights granted herein.+You are not responsible for enforcing compliance by third parties to+this License.++  7. If, as a consequence of a court judgment or allegation of patent+infringement or for any other reason (not limited to patent issues),+conditions are imposed on you (whether by court order, agreement or+otherwise) that contradict the conditions of this License, they do not+excuse you from the conditions of this License.  If you cannot+distribute so as to satisfy simultaneously your obligations under this+License and any other pertinent obligations, then as a consequence you+may not distribute the Program at all.  For example, if a patent+license would not permit royalty-free redistribution of the Program by+all those who receive copies directly or indirectly through you, then+the only way you could satisfy both it and this License would be to+refrain entirely from distribution of the Program.++If any portion of this section is held invalid or unenforceable under+any particular circumstance, the balance of the section is intended to+apply and the section as a whole is intended to apply in other+circumstances.++It is not the purpose of this section to induce you to infringe any+patents or other property right claims or to contest validity of any+such claims; this section has the sole purpose of protecting the+integrity of the free software distribution system, which is+implemented by public license practices.  Many people have made+generous contributions to the wide range of software distributed+through that system in reliance on consistent application of that+system; it is up to the author/donor to decide if he or she is willing+to distribute software through any other system and a licensee cannot+impose that choice.++This section is intended to make thoroughly clear what is believed to+be a consequence of the rest of this License.++  8. If the distribution and/or use of the Program is restricted in+certain countries either by patents or by copyrighted interfaces, the+original copyright holder who places the Program under this License+may add an explicit geographical distribution limitation excluding+those countries, so that distribution is permitted only in or among+countries not thus excluded.  In such case, this License incorporates+the limitation as if written in the body of this License.++  9. The Free Software Foundation may publish revised and/or new versions+of the General Public License from time to time.  Such new versions will+be similar in spirit to the present version, but may differ in detail to+address new problems or concerns.++Each version is given a distinguishing version number.  If the Program+specifies a version number of this License which applies to it and "any+later version", you have the option of following the terms and conditions+either of that version or of any later version published by the Free+Software Foundation.  If the Program does not specify a version number of+this License, you may choose any version ever published by the Free Software+Foundation.++  10. If you wish to incorporate parts of the Program into other free+programs whose distribution conditions are different, write to the author+to ask for permission.  For software which is copyrighted by the Free+Software Foundation, write to the Free Software Foundation; we sometimes+make exceptions for this.  Our decision will be guided by the two goals+of preserving the free status of all derivatives of our free software and+of promoting the sharing and reuse of software generally.++                            NO WARRANTY++  11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY+FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW.  EXCEPT WHEN+OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES+PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED+OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF+MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS+TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU.  SHOULD THE+PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,+REPAIR OR CORRECTION.++  12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR+REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,+INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING+OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED+TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY+YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER+PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE+POSSIBILITY OF SUCH DAMAGES.++                     END OF TERMS AND CONDITIONS++            How to Apply These Terms to Your New Programs++  If you develop a new program, and you want it to be of the greatest+possible use to the public, the best way to achieve this is to make it+free software which everyone can redistribute and change under these terms.++  To do so, attach the following notices to the program.  It is safest+to attach them to the start of each source file to most effectively+convey the exclusion of warranty; and each file should have at least+the "copyright" line and a pointer to where the full notice is found.++    <one line to give the program's name and a brief idea of what it does.>+    Copyright (C) <year>  <name of author>++    This program is free software; you can redistribute it and/or modify+    it under the terms of the GNU General Public License as published by+    the Free Software Foundation; either version 2 of the License, or+    (at your option) any later version.++    This program is distributed in the hope that it will be useful,+    but WITHOUT ANY WARRANTY; without even the implied warranty of+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the+    GNU General Public License for more details.++    You should have received a copy of the GNU General Public License along+    with this program; if not, write to the Free Software Foundation, Inc.,+    51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.++Also add information on how to contact you by electronic and paper mail.++If the program is interactive, make it output a short notice like this+when it starts in an interactive mode:++    Gnomovision version 69, Copyright (C) year name of author+    Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.+    This is free software, and you are welcome to redistribute it+    under certain conditions; type `show c' for details.++The hypothetical commands `show w' and `show c' should show the appropriate+parts of the General Public License.  Of course, the commands you use may+be called something other than `show w' and `show c'; they could even be+mouse-clicks or menu items--whatever suits your program.++You should also get your employer (if you work as a programmer) or your+school, if any, to sign a "copyright disclaimer" for the program, if+necessary.  Here is a sample; alter the names:++  Yoyodyne, Inc., hereby disclaims all copyright interest in the program+  `Gnomovision' (which makes passes at compilers) written by James Hacker.++  <signature of Ty Coon>, 1 April 1989+  Ty Coon, President of Vice++This General Public License does not permit incorporating your program into+proprietary programs.  If your program is a subroutine library, you may+consider it more useful to permit linking proprietary applications with the+library.  If this is what you want to do, use the GNU Lesser General+Public License instead of this License.
+ NF.tex view
@@ -0,0 +1,113 @@+\section{Normal Forms}++\bc\begin{verbatim}+module NF +where +import Form+import Hylotab+\end{verbatim}\ec++Function \verb^fuseLists^ will be used to keep the literals in the +clauses ordered. ++\bc\begin{verbatim}+fuseLists :: Ord a => [a] -> [a] -> [a]+fuseLists [] ys = ys+fuseLists xs [] = xs+fuseLists (x:xs) (y:ys) | x < y  = x:(fuseLists xs (y:ys))+                        | x == y = x:(fuseLists xs ys) +                        | x > y  = y:(fuseLists (x:xs) ys)+\end{verbatim}\ec+++\bc\begin{verbatim}+disjList :: [Form] -> [Form]+disjList []   = [Bool False]+disjList [fm] = [fm]+disjList (fm:fms) = map (disj fm) (disjList fms)+  where +  disj (Disj fms) (Disj fms') = Disj (fuseLists fms fms') +  disj (Disj fms) fm          = Disj (fuseLists fms [fm]) +  disj fm         (Disj fms)  = Disj (fuseLists [fm] fms)+  disj fm         fm'         = Disj [fm,fm']+\end{verbatim}\ec+  +Negation normal form: like negation normal form for modal logic, +except for the case that we also apply the following rules: +\[ +\Ibox{i} (\phi_1 \land \cdots \land \phi_n) \Rightarrow +  (\Ibox{i} \phi_1 \land \cdots \land \Ibox{i} \phi_n) +\]+\[+\Icbox{i} (\phi_1 \land \cdots \land \phi_n) \Rightarrow +  (\Icbox{i} \phi_1 \land \cdots \land \Icbox{i} \phi_n) +\]++\[+\downarrow x.  (\phi_1 \land \cdots \land \phi_n) \Rightarrow +  (\downarrow x. \phi_1 \land \cdots \land \downarrow x. \phi_n) +\]++++\bc\begin{verbatim}+nnf :: Form -> [Form]+nnf (Bool True) = []+nnf (Neg (Bool True)) = [Bool False]+nnf (Bool False) = [Bool False]+nnf (Neg (Bool False)) = []+nnf (Nom nom) = [Nom nom]+nnf (Neg (Nom nom)) = [Neg (Nom nom)]+nnf (Prop prop) = [Prop prop]+nnf (Neg (Prop prop)) = [Neg (Prop prop)]+nnf (Conj fms) = concat (map nnf fms)+nnf (Neg (Conj fms)) = disjList (map Neg fms)+nnf (Disj fms) = disjList fms+nnf (Neg (Disj fms)) = concat (map nnf (map Neg fms))+nnf (Impl fm fm') = nnf (Disj [Neg fm,fm'])+nnf (Neg (Impl fm fm')) = nnf (Conj [fm,Neg fm'])+nnf (A fm) = map A (nnf fm) +nnf (Neg (A fm)) = map E (nnf (Neg fm))+nnf (E fm) = map E (nnf fm) +nnf (Neg (E fm)) = map A (nnf (Neg fm))+nnf (Box rel fm) = map (\x -> (Box rel x)) (nnf fm) +nnf (Neg (Box rel fm)) = [Dia rel (Conj (nnf (Neg fm)))]+nnf (Dia rel fm) = [Dia rel (Conj (nnf fm))]+nnf (Neg (Dia rel fm)) = map (\x -> (Box rel x)) (nnf (Neg fm))+nnf (Cbox rel fm) = map (\x -> (Cbox rel x)) (nnf fm) +nnf (Neg (Cbox rel fm)) = [Cdia rel (Conj (nnf (Neg fm)))]+nnf (Cdia rel fm) = [Cdia rel (Conj (nnf fm))]+nnf (Neg (Cdia rel fm)) = map (\x -> (Cbox rel x)) (nnf (Neg fm))+nnf (At nom fm) = map (\x -> (At nom x)) (nnf fm)+nnf (Neg (At nom fm)) = map (\x -> (At nom x)) (nnf (Neg fm))+nnf (Down v fm) = map (\x -> (Down v x)) (nnf fm)+nnf (Neg (Down v fm)) = map (\x -> (Down v x)) (nnf (Neg fm))+nnf (Neg (Neg fm)) = nnf fm+\end{verbatim}\ec+++\bc\begin{verbatim}+compress :: Form -> Form +compress (At k (At n fm)) = compress (At n fm)+compress (At k fm) = At k (compress fm) +compress (A (A fm)) = compress (A fm)+compress (A (E fm)) = compress (E fm)+compress (E (E fm)) = compress (E fm)+compress (E (A fm)) = compress (A fm)+compress (A fm)     = A (compress fm) +compress (E fm)     = E (compress fm) +compress (Neg fm)   = Neg (compress fm)+compress (Box rel fm) = Box rel (compress fm)+compress (Dia rel fm) = Dia rel (compress fm) +compress (Cbox rel fm) = Cbox rel (compress fm)+compress (Cdia rel fm) = Cdia rel (compress fm)+compress (Down v fm) = Down v (compress fm) +compress fm          = fm+\end{verbatim}\ec++\bc\begin{verbatim}+nf :: Form -> [Form]+nf fm = map compress (nnf fm)+\end{verbatim}\ec++
+ Setup.lhs view
@@ -0,0 +1,4 @@+#! /usr/bin/env runhaskell++> import Distribution.Simple+> main = defaultMain
+ cthl.tex view
@@ -0,0 +1,1885 @@+\documentclass[oribibl]{llncs}+\usepackage{url}+\usepackage{latexsym,amssymb,amsmath,theorem,proof,calc,alltt}+%\usepackage{parsetree}+%\usepackage{tree-dvips}+\usepackage{pst-tree}+++%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+%                                  % +%  VERSION FEB 2002                %+%                                  %+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%++%\input{mymacros}++\newcommand{\commentout}[1]{}+++\newcommand{\close}[1]{\begin{array}{c}{#1} \\ {\times} \end{array}}+\newcommand{\clsubs}[2]{\begin{array}{c}{#1} \\ {#2} \end{array}}+\newcommand{\stack}[1]{\begin{array}{c}{#1} \end{array}}+\newcommand{\barr}{\begin{array}{c}}+\newcommand{\earr}{\end{array}}++\newcommand{\EQ}{\approx}+\newcommand{\NEQ}{\not\approx}++\newcommand{\var}{{\rm var\:}}+%\newcommand{\dom}{{\rm dom\:}}+%\newcommand{\rng}{{\rm rng\:}}++\newcommand{\bB}{\mbox{\boldmath $B$}}++\newcommand{\ttop}{\mbox{\boldmath $\top\!\!\!\!\top$}}+\newcommand{\bbot}{\mbox{\boldmath $\bot\!\!\!\!\bot$}}++\newcommand{\bT}{\mbox{\boldmath $T$}}+\newcommand{\cB}{\mbox{$\cal B$}}++\newcommand{\cE}{{\cal E}}++\newcommand{\href}[1]{}+\newcommand{\Nat}{\mathbb{N}}+\newcommand{\Exists}{\boldsymbol{\exists\!\!\!\exists}}+\newcommand{\Forall}{\boldsymbol{\forall\!\!\!\forall}}+\newcommand{\Neg}{\boldsymbol{\neg\!\!\!\neg}}+\newcommand{\SC}{\ \boldsymbol{;}\ }++\newsavebox{\fminibox}+\newlength{\fminilength}+\newenvironment{fminipage}[1][\linewidth]+ {\setlength{\fminilength}{#1-2\fboxsep-2\fboxrule-1em}%+  \bigskip\begin{lrbox}{\fminibox}\quad\begin{minipage}{\fminilength}\bigskip}+ {\smallskip\end{minipage}\end{lrbox}\noindent\fbox{\usebox{\fminibox}}\bigskip}++\newcommand{\bc}{\begin{fminipage}}+\newcommand{\ec}{\end{fminipage}}++\newenvironment{code}{\begin{fminipage}\begin{alltt}}%+{\end{alltt}\end{fminipage}}++\newenvironment{pcode}{\begin{fminipage}\begin{alltt}}%+{\end{alltt}\end{fminipage}+}++\newcommand{\impl}{\Rightarrow}+\newcommand{\M}{{\cal M}}+\newcommand{\N}{{\cal N}}+\newcommand{\forces}{\mbox{\ $\vdash\!\!\!\vdash$\ }}+\newcommand{\sref}[1]{(\ref{#1})}+\newcommand{\bfx}{\mbox{\bf x}}+\newcommand{\bfy}{\mbox{\bf y}}+\newcommand{\bfz}{\mbox{\bf z}}++\newcommand{\produces}{\longrightarrow}+\newcommand{\yields}{\Rightarrow}++\setlength{\textheight}{22cm}+\setlength{\textwidth}{16cm}+\setlength{\topmargin}{0cm}+\setlength{\oddsidemargin}{0cm}+\setlength{\evensidemargin}{0cm}++\setlength{\parindent}{0 ex} +\setlength{\parskip}{1.5 ex}++\newcommand{\Ibox}[1]{[{\scriptstyle\:#1\: }]}+\newcommand{\Idia}[1]{\langle{\scriptstyle\: #1\: }\rangle}+\newcommand{\Icbox}[1]{[{\scriptstyle\: #1\:}]^{\:\breve{}}}+\newcommand{\Icdia}[1]{\langle{\scriptstyle\: #1\: }\rangle^{\breve{}}}+\newcommand{\Cbox}{\Box^{\:\breve{}}}+\newcommand{\Cdia}{\Diamond^{\breve{}}}+++\title{Constraint Tableaux for Hybrid Logics}++\author{Jan van Eijck}+\institute{CWI and ILLC, Amsterdam, Uil-OTS, Utrecht; + \email{jve@cwi.nl}}+++\begin{document}++\maketitle ++\begin{abstract} \noindent+  Hybrid logics are modal logics with names for worlds. We present+  an improved tableau system for hybrid logic that handles equality+  for nominals by substitution and generation of inequality+  constraints. This compiles out the equalities while storing the+  inequalities, thus allowing for efficient equality reasoning. The+  proof procedure based on the tableau calculus --- the constraint+  proof engine --- uses two other kinds of constraints: box+  constraints and inverse box constraints. Completeness of the system+  follows in the usual way from fairness of the proof procedure,+  together with a model generation argument.++  Next, calculus and proof engine are extended to incorporate the +  universal modality. Among other things, universal modalities allow+  us to tune the proof engine to specific frame classes. This +  leads to a general completeness result for the calculus, for all+  frame classes that can be described by a formula in the first order +  correspondence language of hybrid logic. We propose a sound and +  complete calculus for minimal model generation; this is useful +  for processing formulas without fixed depth. +% , and a compression algorithm for generating+%  minimal models from complete open tableau nodes. +  Finally, we focus on some fragments of hybrid logic that are decided +  by the constraint  proof engine.++  A theorem prover for hybrid logic based on the constraint proof+  engine, {\em HyLoTab}, has been implemented. A companion paper+  \cite{Eijck02:hylotab} contains the full code of of this+  implementation in Haskell \cite{Haskell98:rep}, in `literate+  programming' style \cite{Knuth:lp}. This documented code can be+  found at \url{http://www.cwi.nl/~jve/hylotab}.+\end{abstract} ++\paragraph{Keywords:} Hybrid logic, tableau reasoning, + equality reasoning, model generation, decision methods. +\paragraph{MSC codes:} 03B10, 03F03, 68N17, 68T15 ++\section{Hybrid Logic: Syntax and Semantics} ++Our starting point is ${\cal HL}(@,\breve{},\downarrow)$, a hybrid+logic language+\cite{Areces:le,AreBlaMar:hlcic} with the following syntax. Assume +$p$ ranges over a set of propositions $\{ p_0, p_1, \ldots \}$, +$c$ over a set of constant nominals $\{ c_0, c_1,\ldots \}$, +$x$ over a set of variable nominals $\{ x_0, x_1, \ldots \}$, +$n$ over the sets of constant nominals and variable nominals, +and $i$ over a set of relation indices $\{ i_0, i_1 , \ldots \}$. +Then  ${\cal HL}(@,\breve{},\downarrow)$ is given by: ++\begin{eqnarray*}+\phi & ::= & \top \mid \bot \mid  p +\mid c \mid x \mid \neg \phi +\mid \phi \land \phi' +\mid \phi \lor \phi' +\mid \phi \rightarrow \phi' +\mid \Ibox{i} \phi +\mid \Icbox{i} \phi +\mid \Idia{i} \phi +\mid \Icdia{i} \phi +\mid @ n \phi +\mid \downarrow\! x. \phi. +\end{eqnarray*}++${\cal HL}(@,\breve{})$ is the hybrid language that results from+leaving out the binders $\downarrow\! x. \phi$ from ${\cal+HL}(@,\breve{},\downarrow)$, and ${\cal HL}(@)$ is the hybrid language+that results from leaving out the converse modalities $\Icbox{i}\phi$+and $\Icdia{i} \phi$ from ${\cal HL}(@,\breve{})$.++Models for ${\cal HL}(@,\breve{},\downarrow)$ consist of a set of+woirld $W$, a set $R = \{ R_i \mid i \in I \}$ of binary relations on+$W$, a valuation function $V$ that maps proposition letters to subsets+of $W$, and constant nominals to singleton subsets of $W$. Let $\M =+(M,R,V)$ be such a model, and let $w$ be a world from $\M$. Let $g$ be+a valuation that maps variable nominals to members of $W$. Then the+crucial clauses of the semantics for ${\cal HL}(@,\breve{},\downarrow)$+are given by: +\begin{eqnarray*}+  \M, g, w \forces p &  \text{ iff } & w \in V(p) \\+  \M, g, w \forces c &  \text{ iff } & \{ w \} = V(c) \\+ \M, g, w \forces x  & \text{ iff } & w = g(x) \\+\M, g, w \forces \Ibox{i} \phi &  \text{ iff } & \text{ for all }w'+\text{ with } wR_iw' \text{ it holds that } \M, g, w' \forces \phi \\+\M, g, w \forces \Idia{i} \phi &  \text{ iff } & +  \text{ for some }w' \text{ with } wR_iw' \text{ it holds that } +   \M, g, w' \forces \phi \\ +\M, g, w \forces \Icbox{i} \phi &  \text{ iff } & \text{ for all }w'+\text{ with } w'R_iw \text{ it holds that } \M, g, w' \forces \phi \\+\M, g, w \forces \Icdia{i} \phi &  \text{ iff } & +  \text{ for some }w' \text{ with } w'R_iw \text{ it holds that } +   \M, g, w' \forces \phi \\ +  \M, g, w \forces @ n \phi &  \text{ iff } & \M, g, w' \forces \phi +   \text{ where } \{ w' \} = V(n) \\+  \M, g, w \forces \downarrow\! x. \phi & \text{ iff } & +\M, g^x_w, w \forces \phi.+\end{eqnarray*}+Here $g^x_w$ is like $g$, except possibly for the+fact that it maps $x$ to $w$. +++\section{A Tableau Calculus for ${\cal HL}(@,\breve{},\downarrow)$}++The tableau rules for ${\cal HL}(@, \breve{},\downarrow)$ work on+the labelled version of this language, with inequalities and access+statements added. The tableau rules use the following language ($\phi+\in {\cal HL}(@,\breve{},\downarrow)$):+\begin{eqnarray*}+\psi & ::= & m \NEQ n \mid mRn \mid @ n \phi. +\end{eqnarray*} +We assume a linear ordering $<$ on the set of nominals. An +inequality $m \NEQ n$ generated by the tableau rules will +always satisfy $m \leq n$. Inequalities $m \NEQ m$ are written +as $\bot$. As in \cite{Blackburn:ild,Blackburn:rrars},+the tableau rules are rules for labelled formulas. In fact, the tableau+system of this paper is a variation on these calculi, with a different+approach to equality reasoning for nominals.++The $\Ibox{i}$ and $\Icbox{i}$ rules are the only rules that cannot be+treated once and for all in the proof procedure. They have the+`standing order' nature of the $\gamma$ tableau rules in first order+logic \cite{Smullyan:fl}. In the proof procedure based on the calculus they+are translated into constraints (see Section \ref{PP}). ++\paragraph{Conjunctive rules ($\alpha$ rules)}++\[+\text{}\cfrac{@m (\phi \land \psi)}{+   \begin{array}{c}@m \phi \\+                   @m \psi+   \end{array}} +\hspace*{3em}+\text{}\cfrac{@m \neg (\phi \lor \psi)}{+   \begin{array}{c}@m \neg \phi \\+                   @m \neg \psi+   \end{array}}+\hspace*{3em}+\text{}\cfrac{@m \neg (\phi \rightarrow \psi)}{+   \begin{array}{c}@m \phi \\+                   @m \neg \psi+   \end{array}}+\]++\paragraph{Disjunctive rules ($\beta$ rules)}++\[+\text{}\cfrac{@m (\phi \lor \psi)}{+   @m \phi \ \mid \ @m \psi}+\hspace*{3em}+\text{}\cfrac{@m \neg (\phi \land \psi)}{+   @m \neg \phi \ \mid \ @m \neg \psi}+\hspace*{3em}+\text{}\cfrac{@m (\phi \rightarrow \psi)}{+   @m \neg \phi \ \mid \ @m \psi}+\]++\paragraph{Negation rule} As this is a single-sided calculus, the only +negation rule we need is the rule for double negation. ++\[+\cfrac{@m \neg \neg \phi}{+       @m \phi}+\]++\paragraph{$\Ibox{i}$ rules} Like the $\gamma$ rules in FOL tableaux, these+are `standing orders'. ++\[+\cfrac{@m \Ibox{i} \phi, mR_in}{+       @n \phi}+\hspace*{3em}+\cfrac{@m \neg \Idia{i}\phi, mR_in}{+       @n \neg \phi}+\]++\paragraph{$\Idia{i}$ rules} ++\[+\cfrac{@n \Idia{i} \phi}{+ \begin{array}{c}  nR_im  \\+                   @m \phi+   \end{array}}\text{ $\phi$ not a nominal, $m$ fresh}+\hspace*{3em}+\cfrac{@n \neg \Ibox{i} \phi}{+ \begin{array}{c}  nR_im  \\+                   @ m \neg \phi+   \end{array}}\text{ $\phi$ not a negated nominal, $m$ fresh}+\]++\paragraph{$\Icbox{i}$ rules} +Like the $\gamma$ rules in FOL tableaux, these are `standing orders'. ++\[+\cfrac{@m \Icbox{i} \phi, nR_im}{+       @n \phi}+\hspace*{3em}+\cfrac{@m \neg \Icdia{i} \phi, nR_im}{+       @n \neg \phi}+\]++\paragraph{$\Icdia{i}$ rules}++\[+\cfrac{@n \Icdia{i} \phi}{+ \begin{array}{c}  mR_in  \\+                   @m \phi+   \end{array}}\text{ $\phi$ not a nominal, $m$ fresh}+\hspace*{3em}+\cfrac{@n \neg \Icbox{i} \phi}{+ \begin{array}{c}  mR_in  \\+                   @ m \neg \phi+   \end{array}}\text{ $\phi$ not a negated nominal, $m$ fresh}+\]++\paragraph{Access rules} Formulas of the forms $\Idia{i} n$,+ $\neg \Ibox{i} \neg n$, $\Icdia{i} n$,  $\neg \Icbox{i} \neg n$,+are called access formulas. They are treated by a separate rule. ++\[+\cfrac{@n \Idia{i} m}{nR_im}+\hspace*{3em}+\cfrac{@n \neg \Ibox{i} \neg m}{nR_im}+\hspace*{3em}+\cfrac{@n \Icdia{i} m}{mR_in}+\hspace*{3em}+\cfrac{@n \neg \Icbox{i} \neg m}{mR_in}+\]++\paragraph{Label rules}++\[+\text{}\cfrac{@m @n \phi}{+   @n \phi}+\hspace*{3em}+\text{}\cfrac{@m \neg @ n \phi}{+   @ n \neg \phi}+\]++\paragraph{Nominal substitution}++Here comes the new element, a substitution rule that makes use of the+fact that nominals are unique names. $\bB^t_s$ is the result of+substituting $s$ for $t$ everywhere in tableau branch $\bB$. The rules+make use of the linear order $<$ on nominals.++\[+\cfrac{\bB + @m m}{\bB}+\hspace*{3em}+\cfrac{\bB + @m n}{\bB^t_s} s = \min(m,n), t = \max(m,n)+\]++\paragraph{Inequality generation}++Write $\bot$ for $m \NEQ m$. ++\[+\cfrac{@m \neg m}{\bot}+\hspace*{3em}+\cfrac{@m \neg n}{s \NEQ t} \ s = \min(m,n), t = \max(m,n)+\]+\[+\cfrac{@m \phi, @m \neg \phi}{\bot}+\hspace*{3em}+\cfrac{@m \phi, @n \neg \phi}{s \NEQ t} \ s = \min(m,n), t = \max(m,n)+\]+The rule that derives an inequality constraint from $@m \phi, @n \neg+\phi$ is a so-called admissible rule. It does not change the set of+formulas that can be refuted or proved satisfiable, but admitting it+to the calculus may shorten some tableau proofs.++\paragraph{Binding rules} ++\[+\cfrac{@m \downarrow\! x. \phi}{@m \phi^x_m}+\hspace*{3em}+\cfrac{@m \neg \downarrow\! x. \phi}{@m \neg \phi^x_m}+\]++Here $\phi^x_m$ denotes the result of substituting $m$ for all +{\em free}\/ occurrences of $x$ in $\phi$. +++\paragraph{Tableau Closure} ++A tableau branch is closed if it contains $\bot$. A tableau is closed+if all its branches are closed. Note that {\bf nominal substitution}\/ can+lead to branch closure. ++\section{Examples of Refutation Proofs, for ${\cal HL} (@)$}++\begin{figure}[htbp]+\begin{center}+$ + \pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%+  {\Tr{@m (\Diamond (i \land p) \land \Diamond (i \land q) \land +            \Box (\neg p \lor \neg q))}}{+    \pstree{\Tr{@m \Diamond  (i \land p), +                  @m \Diamond  (i \land q),+                  @m \Box(\neg p \lor \neg q)}}{+    \pstree{\Tr{mRn, @n (i \land p), +                @m \Diamond  (i \land q),+                @m \Box(\neg p \lor \neg q)+                                             }}{+    \pstree{\Tr{mRn, @n i, @n p, +                @m \Diamond  (i \land q),+                @m \Box(\neg p \lor \neg q)+                                             }}{+    \pstree{\Tr{mRi, @i p, +                @m \Diamond  (i \land q),+                @m \Box(\neg p \lor \neg q)+                                             }}{+    \pstree{\Tr{mRi, @i p, +                mRk, @k(i \land q),+                @m \Box(\neg p \lor \neg q)+                                             }}{+    \pstree{\Tr{mRi, @i p, +                mRk, @ki, @ k q,+                @m \Box(\neg p \lor \neg q)+                                             }}{+    \pstree{\Tr{mRi, @i p, +                @i q,+                @m \Box(\neg p \lor \neg q)+                                             }}{+    \pstree{\Tr{mRi, @i p, +                @i q,+                @m \Box(\neg p \lor \neg q), +                @i (\neg p \lor \neg q)+                                             }}{+      \pstree{\Tr{+                \begin{array}{l} +                mRi, @i p, @i q, \\+                @m \Box(\neg p \lor \neg q), +                @i \neg p  +                \end{array}+                                             }}{\Tr{\bot}}+      \pstree{\Tr{\begin{array}{l}+                mRi, @i p, @i q, \\+                @m \Box(\neg p \lor \neg q), +                @i \neg q +                \end{array}+                                             }}{\Tr{\bot}}+}+}+}+}+}+}+}+}+}+$+\end{center}+\caption{Tableau refutation for (\ref{Ex1}).} + \label{FigEx1}+\end{figure}++\commentout{+\begin{figure}[htbp]+\begin{center}+$ + \pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%+  {\Tr{@m (\Diamond (i \land p) \land \Diamond (i \land q) \land +            \Box (\neg p \lor \neg q))}}{+    \pstree{\Tr{@m \Diamond  (i \land p), +                  @m \Diamond  (i \land q),+                  @m \Box(\neg p \lor \neg q)}}{+    \pstree{\Tr{mRn, @n (i \land p)+                                             }}{+    \pstree{\Tr{@n i, @n p +                                             }}{+    \pstree{\Tr{n \mapsto i+                                             }}{+    \pstree{\Tr{mRk, @k(i \land q)+                                             }}{+    \pstree{\Tr{@ki, @ k q+                                             }}{+    \pstree{\Tr{k \mapsto i +                                             }}{+    \pstree{\Tr{@i (\neg p \lor \neg q)+                                             }}{+      \pstree{\Tr{+                @i \neg p  +                                             }}{\Tr{\bot}}+      \pstree{\Tr{+                @i \neg q +                                             }}{\Tr{\bot}}+}+}+}+}+}+}+}+}+}+$+\end{center}+\caption{Tableau refutation for (\ref{Ex1}), without formula repetition.} + \label{FigEx1a}+\end{figure}+}++Figure \ref{FigEx1} gives a tableau refutation of \sref{Ex1}, with the+active formulas of the branch repeated at each node.++\commentout{ + Figure+\ref{FigEx1} gives another version of this, without repetition of+formulas, but with the substitution instructions indicated along the+branch.+}++\begin{equation} \label{Ex1}+ @m (\Diamond (i \land p) \land \Diamond (i \land q) \land +            \Box (\neg p \lor \neg q)).+\end{equation}++The tableau refutation of \sref{Ex1} proves the validity of +$\Diamond (i \land p) \land \Diamond (i \land q) + \rightarrow \Diamond (p \land q)$, which expresses that +if from the current world $i$ is accessible, and at $i$ both +$p$ and $q$ hold, then from the current world a $p\land q$ +world is accessible. ++\begin{figure}[htbp]+\begin{center}+$ + \pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%+  {\Tr{@m \neg ((\Diamond p \land \Diamond \neg p) +    \rightarrow (\Box (q \rightarrow i) \rightarrow \Diamond \neg q))}}{+   \pstree{\Tr{+     @m (\Diamond p \land \Diamond \neg p), +     @m \neg (\Box (q \rightarrow i) \rightarrow \Diamond \neg q)}}{+   \pstree{\Tr{+     @m \Diamond p, @m \Diamond \neg p, +                                                     }}{+   \pstree{\Tr{+     @m \Box (q \rightarrow i), @m \neg \Diamond \neg q +                                                     }}{+   \pstree{\Tr{+     mRn, @n p+                                                     }}{+    \pstree{\Tr{+     mRk, @k \neg p+                                                     }}{+   \pstree{\Tr{+     @n (q \rightarrow i), @n q     +                                                     }}{+   \pstree{\Tr{+     @k (q \rightarrow i), @k q     +                                                     }}{+      \pstree{\Tr{+        @n \neg q    +                                                     }}{\Tr{\bot}}+      \pstree{\Tr{+        @n i    +                                                     }}{+      \pstree{\Tr{n \mapsto i +                                                     }}{+         \pstree{\Tr{@k \neg q}}{\Tr{\bot}}+         \pstree{\Tr{@k i}}{+          \pstree{\Tr{k \mapsto i }}{\Tr{\bot}}+}+}+}+}+}+}+}+}+}+}+}+$+\end{center}+\caption{Tableau refutation for +$@m \neg ((\Diamond p \land \Diamond \neg p) +    \rightarrow (\Box (q \rightarrow i) \rightarrow \Diamond \neg q))$+.}+%(\ref{Ex2}).} + \label{FigEx2}+\end{figure}++Figure \ref{FigEx2} gives a tableau refutation of $@m \neg ((\Diamond+p \land \Diamond \neg p) \rightarrow (\Box (q \rightarrow i)+\rightarrow \Diamond \neg q))$, without repetition of+formulas, but with the substitution instructions indicated along the+branch. The nominal substitutions $n \mapsto+i$ and $k \mapsto i$ act on the formulas $@ n p$ and $@ k \neg p$ to+give $@ i p, @ i \neg p$ on the branch, and therefore branch+closure. The tableau refutation proves the validity of $((\Diamond p+\land \Diamond \neg p) \rightarrow (\Box (q \rightarrow i) \rightarrow+\Diamond \neg q))$, a principle which expresses that if from the+current world there are at least two worlds accessible, and if $i$ is+the only accessible $q$ world, then there has to be an accessible+$\neg q$ world.++\commentout{+\section{Examples of Model Generation, for ${\cal HL} (@)$} ++\begin{figure}[htbp]+\begin{center}+$ + \pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%+  {\Tr{ +       @m (\Diamond \Diamond m \land \neg \Diamond m) +                                                              }}{+    \pstree{\Tr{+       @m \Diamond \Diamond m, @m \neg \Diamond m+                                                              }}{+    \pstree{\Tr{+       mRn, @n \Diamond m+                                                              }}{+    \pstree{\Tr{+       @n \neg m+                                                              }}{+    \pstree{\Tr{+       n \NEQ m +                                                              }}{+    \pstree{\Tr{+       nRk, @k m+                                                              }}{+    \pstree{\Tr{+        m \mapsto k+                                                              }}{+}+}+}+}+}+}+}+$+\end{center}+\caption{Open tableau for +$@m (\Diamond \Diamond m \land \neg \Diamond m)$.}+ \label{FigRef1}+\end{figure}++Figure \ref{FigRef1} gives an open tableau for +$@m (\Diamond \Diamond m \land \neg \Diamond m)$. +Since the formula contains no proposition letters, it defines a+frame property. The smallest frame with the property is $\bullet+\leftrightarrow \bullet$.++\begin{figure}[htbp]+\begin{center}+$ + \pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%+  {\Tr{ +       @m (\Diamond i \land \Diamond j \land \Diamond k+       \land @ i \neg j \land @ j \neg k \land @ i \neg k)+                                                              }}{+  \pstree{\Tr{+       @m \Diamond i, +       @m \Diamond j, +       @m \Diamond k, +       @m @ i \neg j, +       @m @ j \neg k, +       @m @ i \neg k+                                                              }}{+  \pstree{\Tr{+       mRi, mRj, mRk+                                                              }}{+  \pstree{\Tr{+       @i \neg j, @j \neg k, @i \neg k+                                                              }}{+  \pstree{\Tr{+       i \NEQ j, j \NEQ k, i \NEQ k+                                                              }}{+}+}+}+}+}+$+\end{center}+\caption{Open tableau for +$ @m (\Diamond i \land \Diamond j \land \Diamond k+       \land @ i \neg j \land @ j \neg k \land @ i \neg k)$.}+%(\ref{Ref2}).} + \label{FigRef2}+\end{figure}++Figure \ref{FigRef2} gives an open tableau for+$ @m (\Diamond i \land \Diamond j \land \Diamond k+       \land @ i \neg j \land @ j \neg k \land @ i \neg k)$.++\begin{figure}[htbp]+\begin{center}+$ + \pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%+  {\Tr{@m \Diamond (c \land \Diamond c \land \Box \Diamond c)}}{+    \pstree{\Tr{mRn, @n (c \land \Diamond c \land \Box \Diamond c)}}{+    \pstree{\Tr{@n c, @ n \Diamond c, @ n \Box \Diamond c+                                             }}{+    \pstree{\Tr{n \mapsto c+                                             }}{+    \pstree{\Tr{cRc, @c  \Box \Diamond c+                                             }}{+    \pstree{\Tr{@ c \Diamond c+                                             }}{+    \Tr{cRc}}+}+}+}+}+}+$+\end{center}+\caption{Open tableau for $\Diamond (c \land+\Diamond c \land \Box \Diamond c)$.} + \label{FigNewEx}+\end{figure}++Figure \ref{FigNewEx} shows that the formula $\Diamond (c \land+\Diamond c \land \Box \Diamond c)$ is satisfiable. Note that this+formula causes the first of the two tableau proof procedures in+\cite{Tzakova:tcfhl} to loop.+++\section{Examples of the treatment of $\downarrow$} ++\begin{figure}[htbp]+\begin{center}+$ + \pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%+  {\Tr{ +       @m(\downarrow x. \Box \Diamond x +       \land \neg (\Diamond \Box p \rightarrow p))+                                                              }}{+    \pstree{\Tr{+       @m \downarrow x. \Box \Diamond x,  +       @m \neg (\Diamond \Box p \rightarrow p)+                                                              }}{+    \pstree{\Tr{+       @m \Box \Diamond m+                                                              }}{+    \pstree{\Tr{+       @m \Diamond \Box p, @m \neg p+                                                              }}{+    \pstree{\Tr{+      mRn, @n \Box p+                                                              }}{+    \pstree{\Tr{+      @n \Diamond m+                                                              }}{+   \pstree{\Tr{+       nRm+                                                              }}{+   \pstree{\Tr{+       @m p +                                                              }}{\Tr{\bot}}+}+}+}+}+}+}+}+$ +\end{center}+\caption{Closed tableau for $@m \ \downarrow x . \Box \Diamond x \land +    \neg (\Diamond \Box p \rightarrow p)$.} + \label{FigArrowEx1}+\end{figure}++Figure \ref{FigArrowEx1} gives a closed tableau for +$@m \ \downarrow x . \Box \Diamond x \land +    \neg (\Diamond \Box p \rightarrow p)$.+The formula $\downarrow x . \Box \Diamond x$ holds at the point $m$ if+$mRn$ implies $nRm$. The formula $\Diamond \Box p \rightarrow p$ is+true at points where $R$ is symmetric. Therefore, $\downarrow x . \Box+\Diamond x \rightarrow (\Diamond \Box p \rightarrow p)$ is valid. ++\begin{figure}[htbp]+\begin{center}+$ + \pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%+  {\Tr{ +       @s (\Diamond \top \land \Box \Box \downarrow x. @ s \Diamond x +       \land \Box (\Diamond \top \land \phi))+                                                              }}{+    \pstree{\Tr{+       @s \Diamond \top, +       @s \Box \Box \downarrow x. @ s \Diamond x, +       @s \Box (\Diamond \top \land \phi)+                                                              }}{+    \pstree{\Tr{+      sRt+                                                              }}{+    \pstree{\Tr{+      @t \Diamond \top, @ t \phi+                                                              }}{+    \pstree{\Tr{+      tRt'+                                                              }}{+    \pstree{\Tr{+      @t \Box \downarrow x. @ s \Diamond x +                                                              }}{+    \pstree{\Tr{+      @t' \downarrow x. @ s \Diamond x +                                                              }}{+    \pstree{\Tr{+      @t' @ s \Diamond t' +                                                              }}{+    \pstree{\Tr{+      @ s \Diamond t' +                                                              }}{+    \pstree{\Tr{+      sRt' +                                                              }}{+    \pstree{\Tr{+      @t' \Diamond \top, @ t' \phi+                                                              }}{+    \pstree{\Tr{+     t'Rt''+                                                              }}{\Tr{\vdots}}+}+}+}+}+}+}+}+}+}+}+}+$ +\end{center}+\caption{Infinite tableau for (\ref{ArrowEx2}).} + \label{FigArrowEx2}+\end{figure}+}++In ${\cal HL}(\downarrow, @)$ it is easy to describe situations that+only have infinite models. See \sref{ArrowEx2}+%Figure \ref{FigArrowEx2} gives an infinite+%tableau for \sref{ArrowEx2}.+\begin{equation} \label{ArrowEx2}+ @s (\Diamond \top \land \Box \Box \downarrow x. @ s \Diamond x +       \land \Box (\Diamond \top \land \phi)), +\end{equation}+where $\phi$ is the formula +\[ +\downarrow x . \Box \neg x \land \downarrow x. \Box \Box \neg x +  \land +\downarrow x . \Box \Box \downarrow y . @ x \Diamond y.+\]+The formula $\downarrow x .  \Box \neg x$ expresses irreflexivity, the+formula $\downarrow x . \Box \Box \neg x$ asymmetry, the formula+$\downarrow x . \Box \Box \downarrow y . @ x \Diamond y$+transitivity. Formula \sref{ArrowEx2} expresses that from the spypoint+$s$ a serial, irreflexive, asymmetric and transitive, hence infinite,+relation is visible.++\section{From Tableau Calculus to Proof Engine}+\label{PP}++\begin{figure}[htbp] \small+\bc+\[+ \cfrac{\text{start } \phi}{[m],[],[],[],[],[],[@ m \phi]}\ m \text{ fresh+ }+\]+\[+ \cfrac{U,A,I,P,N,C,F}+       {\text{closure}} +\ \bot \in I \lor P \cap N \neq+ \emptyset \hspace{3em} +\cfrac{U,A,I,P,N,C,[]}+      {\text{success}} +\ \bot \notin I, P \cap N = \emptyset+\]+\[+\cfrac{U,A,I,P,N,C,(@m \phi:F)}+      {U,A,I,P,N,C,[@m \phi_1, \ldots, @m \phi_n] +\!\!+ F}\ \phi \in+      \alpha+\]+\[+\cfrac{U,A,I,P,N,C,(@m \phi:F)}+      {U,A,I,P,N,C,(@m \phi_1:F)\ \mid \ \ \cdots \ \ \mid \+       U,A,I,P,N,C,(@m \phi_n:F)}\ \phi \in \beta+\]+\[+\cfrac{U,A,I,P,N,C,(@m \neg \neg \phi:F)}+      {U,A,I,P,N,C,(@m \phi:F)}+\]+\[+\cfrac{U,A,I,P,N,C,(@m p:F)}+      {U,A,I,(@m p:P),N,C,F} \hspace{3em}+\cfrac{U,A,I,P,N,C,(@m \neg p:F)}+      {U,A,I,P,(@ n p:N),C,F}+\]+\[+\cfrac{U,A,I,P,N,C,(@m n:F)}+      {U^t_s,A^t_s,I^t_s,P^t_s,N^t_s,C^t_s,F^t_s +\!\!+ F'} +  \ s = \min(m,n), t = \max(m,n), F' = \text{ stuff to restore invariant }+\]+\[+\cfrac{U,A,I,P,N,C,(@m \neg n:F)}+      {U,A,(s\NEQ t:I),P,N,C,F} + \ s = \min(m,n), t = \max(m,n)+\]+\[+\cfrac{U,A,I,P,N,C,(@m @n \phi:F)}+      {U,A,I,P,N,C,(@n \phi:F)} \hspace{3em}+\cfrac{U,A,I,P,N,C,(@m \neg @n \phi:F)}+      {U,A,I,P,N,C,(@n \neg \phi:F)}+\]+\[+ \cfrac{U,A,I,P,N,C,(@m \phi:F)} +       {U,A,I,P,N,(@m \phi:C),F +\!\!+\, [@ n+ \phi' \mid mR_in \in A]} \ \phi \in \Ibox{i}+\]+\[+ \cfrac{U,A,I,P,N,C,(@m \Idia{i} n:F)} +       {U,(mR_in:A),I,P,N,C, F ++  +\!\!+\, [@ n \psi \mid @ m \Ibox{i} \psi \in C] +  +\!\!+\, [@ m \psi \mid @ n \Icbox{i} \psi \in C]}+\]+\[+ \cfrac{U,A,I,P,N,C,(@m \phi:F)} +       {(n:U),(mR_in:A),I,P,N,C,(@ n \phi':F) + +\!\!+\, [@ n \psi \mid @ m \Ibox{i} \psi \in C]} + \ \phi \in \Idia{i}, n \text{ fresh }+\]+\[+ \cfrac{U,A,I,P,N,C,(@m \phi:F)} +       {U,A,I,P,N,(@m \phi:C), F +   +\!\!+\, [@ n \phi' \mid nR_im \in A]}+  \ \phi \in \Icbox{i}+\]+\[+ \cfrac{U,A,I,P,N,C,(@m \Icdia{i} n:F)} +       {U, (nR_im:A),I,P,N,C, F +\!\!+\, [@+ m \psi \mid @ n \Ibox{i} \psi \in C] F +\!\!+\, [@ n \psi \mid @ m+ \Icbox{i} \psi \in C]}+\]+\[+ \cfrac{U,A,I,P,N,C,(@m \phi:F)} +       {(n:U),(nR_im:A),I,P,N,C,(@ n \phi':F) +  +\!\!+\,  [@ n \psi \mid @ m \Icbox{i} \psi \in C]} +  \ \phi \in \Icdia{i}, n  \text{ fresh }+\]+\[+ \cfrac{U,A,I,P,N,C,(@m \downarrow x.\phi:F)} {U,A,I,P,N,C,(@m+ \phi^x_m:F)} \hspace{3em} \cfrac{U,A,I,P,N,C,(@m \neg \downarrow+ x.\phi:F)} {U,A,I,P,N,C,(@m \neg \phi^x_m:F)}+\]+\ec+\caption{Constraint Proof Engine for +         ${\cal HL}(@,\breve{},\downarrow)$.}+\label{PPfig}+\end{figure}++A proof procedure (or proof engine) for $\phi$ is a systematic search+for a Kripke model satisfying $\phi$, by means of a search tree+starting out from a node {\em start $\phi$}. Our proof engine for+hybrid logic based on the calculus given above is presented in Figure+\ref{PPfig}. The proof rules work on tuples $(U,A,I,P,N,C,F)$+consisting of a node universe (or node domain) $U$, a +list of accessibilities $A$, a list of inequality+constraints $I$, a list of positive propositional attributions $P$, a+list of negative propositional attributions $N$, a list of box+constraints and converse box constraints $C$, and a list of pending+formulas $F$. Write $\phi:F$ for the list with head $\phi$ and tail+$F$, and $F_1 +\!\!+ F_2$ for the result of concatenating lists $F_1,+F_2$. Write $[]$ for the empty list, $[\phi]$ for the unit list with+$\phi$ as its element, and $[\phi_1,+\ldots \phi_n]$ for the list consisting of $\phi_1$ through $\phi_n$.+We will assume throughout that the lists do not contain duplicates,+i.e., that the lists behave as ordered sets. In particular, $U^s_t$ +means that $s$ gets replaced by $t$ in $U$, and the duplicate of +$t$ that this may generate is removed. ++The table uses abbreviations $\phi \in \alpha, \phi \in \beta, \phi+\in \Ibox{i}, \phi \in \Idia{i}, \phi \in \Icbox{i}, \phi \in \Icdia{i}$ +for ``$\phi$ is an $\alpha$ formula'', +and so on. We do not count $\Idia{i} n$ or $\Icdia{i} n$ +or $\neg \Ibox{i} \neg n$ or $\neg \Icbox{i} \neg n$+as $\Idia{i}$ or $\Icdia{i}$ formulas, as these `access+formulas' are treated by a separate rule. If $\phi \in \alpha \cup+\beta$, the components of $\phi$ are referred to as $\phi_1, \ldots,+\phi_n$. If $\phi \in \Ibox{i} \cup \Idia{i}\cup \Icbox{i} +\cup \Icdia{i}$, its component is referred to as $\phi'$.++The key to understanding the table is the following invariant of the rule +applications: the constraint store of the node contains only constraints that +have been combined with all access relations of the node. This invariant +may get violated when a new access relation gets added, when a new constraint+gets added, or when a substitution is applied to a node. In all such cases, +the invariant is restored by applying the appropriate constraints, thus +generating extra material on the pending formula list. ++Here is what has to happen in the case of applying a substitution to a node: +\begin{itemize} +\item If the substitution results in new access relations, these +      get combined with all box and converse box constraints of the node. +\item If the substitution results in new box constraints, these get +      combined with all access relations of the node. +\item If the substitution results in new converse box constraints, these +     get combined with all access relations of the node. +\end{itemize}+In the substitution rule in the table, this procedure is abbreviated+as `add stuff to restore the invariant'.++\paragraph{Closure, Success}++A node $(U,A,I,P,N,C,F)$ is closed if either $\bot \in I$ or $P \cap N+\neq \emptyset$, otherwise it is open. An open node $(U,A,I,P,N,C,F)$+is a success node if it has $F = []$. A node is {\em incomplete}\/ if+it is neither closed nor a success node.++\paragraph{Selection Rule}++To develop an incomplete node, use the table from Figure+\ref{PPfig}. Since an incomplete node contains a non-empty list of+pending formulas, and the table has exactly one rule that applies to+the head $\phi$ of the pending formula list, this specifies the {\em+selection rule}\/ of the proof engine. ++\paragraph{Search Rule} ++To select an incomplete leaf node to develop, use any breadth first+search method for tree traversal. This specifies a {\em search rule}\/+for the proof engine. ++\paragraph{Termination Condition}++The proof procedure ends when there are no more nodes to develop. The+proof procedure can be used both for satisfiablity checking and for+refutation. For satisfiability checking, the satisfiability procedure+outputs {\em true}\/ when a success node is encountered, and outputs+{\em false}\/ if the proof procedure ends with closed nodes at all+leaves. For refutation, the refutation procedure outputs {\em false}\/+when a success node is encountered, and outputs {\em true}\/ if the+proof procedure ends with closed nodes at all leaves.++\section{Soundness, Fairness of Proof Engine, Completeness}++\begin{theorem}+The tableau calculus for ${\cal HL}(@,\breve{},\downarrow)$ is+sound.+\end{theorem}+\begin{proof}+By an easy inspection, all tableau rules are sound. Soundness of the+calculus follows from this by induction on tableau structure.+\end{proof} ++For completeness, we need a fair proof procedure $P$. Consider the+(possibly infinite) set of tableaux for formula $\phi$, according to+procedure $P$. Since $P$ determines which rule (selection) to apply to+which node (search), this tableau set is ordered. The successor of a+tableau $\bT$ is tableau $\bT'$ computed from $\bT$ according to+$P$. Let $\bT_0$ be the initial tableau for $\phi$. Then there is +a possibly infinite ascending chain $\bT_0, \ldots$ of tableaux +for $\phi$. By Zorn's lemma, this chain has a supremum $\bT_\infty$. ++A proof procedure for hybrid logic is fair if the following hold for+all open branches $\bB$ in $\bT_\infty$: +\begin{enumerate}+\item All atomic formulas of the form $@m n$ on $\bB$ were used +      were used to perform a substitution on $\bB$. +\item All non-atomic formulas of types other than +      $\Ibox{i}$ or $\Icbox{i}$ on $\bB$ were used to expand $\bB$.+\item All formulas of type $\Ibox{i}$ or $\Icbox{i}$ on $\bB$ were +      combined with all $mR_in$ accessibilities on $\bB$ to expand +      $\bB$. +\end{enumerate}++\begin{theorem} \label{PPfair}+The Constraint Proof Engine of Section \ref{PP} is fair.+\end{theorem}+\begin{proof}+Inspection of the table in Figure \ref{PPfig} makes clear that (1) is+satisfied. That (2) is also satisfied follows from an induction+argument: it can be proved by induction on path length that the+constraint set at each node $N$ consists of exactly the $\Ibox{i} \cup+\Icbox{i}$ formulas at the node that were used to expand all+appropriate $mR_in$ accessibilities introduced on the path along $\bB$+from the root up to $N$. Finally, note that formulas resulting from+combining an accessibility relation $mR_in$ and a constraint $@ m+\Ibox{i} \phi$ or $@ n \Icbox{i}\phi$ are appended to the list of+pending formulas, thus ensuring that every formula on the pending+formula list will eventually get treated.+\end{proof}++Call a tableau {\em finished}\/ if it does not contain incomplete end+nodes. It is easy to see that each limit tableau $\bT_\infty$ is+finished. Every open branch of a finished tableau for $\phi$ yields a+Kripke model for $\phi$: take the nominals as worlds, put $m+\stackrel{i}{\longrightarrow} n$ if a $mR_in$ relation +occurs along the branch, make+all proposition letters $p$ with $@m p$ along the branch true at $m$,+and all other proposition letters false at $m$. From the facts that+the tableau is finished and that the branch is open it follows that+this model is well-defined, and from the fact that the tableau rules+are truth preserving in both directions it follows that it is indeed a+model for $\phi$.++\begin{theorem}+The tableau calculus for ${\cal HL}(@,\breve{},\downarrow)$ is complete.+\end{theorem}+\begin{proof}+Immediate from Theorem \ref{PPfair}, plus the fact that every open+branch of a finished tableau for $\phi$ yields a Kripke model for+$\phi$.+\end{proof}++\section{Adding the Universal Modality}++We now extend the language with the universal modality $A$ and +its dual $E$, with the following intended meanings:+\begin{eqnarray*}+\M, g, w \forces A\phi &  \text{ iff } & \text{ for all }w' \in M+\text{ it holds that } \M, g, w' \forces \phi \\+\M, g, w \forces E\phi &  \text{ iff } & \text{ for some }w' \in M+\text{ it holds that } \M, g, w' \forces \phi +\end{eqnarray*}+It is well known that binding together with universal modality makes+it possible to express full quantification. The definition of the +quantifiers is as follows: +\begin{eqnarray*}+\M, g, w \forces \forall x \phi &  \text{ iff } & \text{ for all }g' +\text{ with } g \stackrel{x}{\sim} g' \text{ it holds that } +\M, g', w \forces \phi \\+\M, g, w \forces \exists x \phi &  \text{ iff } & \text{ for some }g' +\text{ with } g \stackrel{x}{\sim} g' \text{ it holds that } +\M, g', w \forces \phi +\end{eqnarray*}+It is not hard to see that $\forall x \phi$+can be taken as shorthand for $\downarrow\! y . A\downarrow\! x . @ y+\phi$, and $\exists x \phi$ as shorthand for $\downarrow \!y +. E\downarrow \!x . @ y \phi$. So we have full quantification once we+know how to deal with the modalities $A$ and $E$. Tableau rules for+$A$ and $E$ can look like this:++\[+\cfrac{@m A \phi}{@n \phi}\ n \text{ on the branch }+\hspace*{3em}+\cfrac{@m \neg E \phi}{@n \neg \phi} \  n \text{ on the branch }+\]+\[+\cfrac{@m E \phi}{@n \phi}\ n \text{ fresh }+\hspace*{3em}+\cfrac{@m \neg A \phi}{@n \neg \phi} \  n \text{ fresh }+\]+Since the tableau rules for $A$ and $E$ are obviously sound, we +get by induction on tableau structure: +\begin{theorem}+The tableau calculus for ${\cal HL}(@,\breve{},\downarrow,A)$ is+sound.+\end{theorem}++\begin{figure}[htbp] \footnotesize+\bc+\[+ \cfrac{U,A,I,P,N,C,(@m \phi:F)} +       {(n:U),A,I,P,N,C,(@ n \phi':F) +  +\!\!+\, [@ n \psi \mid A \psi \in C] } + \ \phi \in E, n  \text{ fresh }+\]+\[+ \cfrac{U,A,I,P,N,C,(@m \phi:F)} +       {U,A,I,P,N,(\phi:C),F  +  +\!\!+\, [@ n \phi' \mid n \in U ] } + \ \phi \in A+\]+\[+ \cfrac{U,A,I,P,N,C,(@m \Idia{i} n:F)} +       {U,(mR_in:A),I,P,N,C, F +  +\!\!+\, [@ n \psi \mid @ m \Ibox{i} \psi \in C] +  +\!\!+\, [@ m \psi \mid @ n \Icbox{i} \psi \in C]+  +\!\!+\, [@ m \psi \mid A \psi \in C]}+\]+\[+ \cfrac{U,A,I,P,N,C,(@m \phi:F)} +       {(n:U),(mR_in:A),I,P,N,C,(@ n \phi':F) +  +\!\!+\, [@ n \psi \mid @ m \Ibox{i} \psi \in C] +  +\!\!+\, [@ n \psi \mid A \psi \in C] } +  \ \phi \in \Idia{i}, n \text{ fresh }+\]+\[+ \cfrac{U,A,I,P,N,C,(@m \Icdia{i} n:F)} +       {U,(nR_im:A),I,P,N,C, F +  +\!\!+\, [@ n \psi \mid @ m \Icbox{i} \psi \in C] +  +\!\!+\, [@ n \psi \mid A \psi \in C] }+\]+\[+ \cfrac{U,A,I,P,N,C,(@m \phi:F)} +       {(n:U),(nR_im:A),I,P,N,C,(@ n \phi':F) +  +\!\!+\,  [@ n \psi \mid @ m \Icbox{i} \psi \in C]+  +\!\!+\, [@ n \psi \mid A \psi \in C] }+  \ \phi \in \Icdia{i}, n  \text{ fresh }+\]+\ec+\caption{Modified Constraint Proof Engine for +         ${\cal HL}(@,\breve{},\downarrow,A)$.}+\label{APEfig}+\end{figure}++Figure \ref{APEfig} lists the modifications in the constraint proof+engine that are necessary to accommodate the universal modality. The+conditions $\phi \in A$, $\phi \in E$ have the obvious+meanings. $A$-type formulas are of the forms $A\psi$, with component+$\psi$, and $\neg E \psi$, with component $\neg+\psi$. $E$-type formulas are of the forms $E\psi$, with component+$\psi$, and $\neg A\psi$, with component $\neg \psi$.+The constraint store $C$ now also contains universal formulas +$A \psi$, and the corresponding constraints have to be imposed on +{\em all}\/ nominals that turn up at the branch.++The results about fairness and completeness extend to the new +calculus and proof engine: ++\begin{theorem} \label{APEfair}+The modified Constraint Proof Engine of Figure \ref{APEfig} is fair.+\end{theorem}++\begin{theorem}+The tableau calculus for ${\cal HL}(@,\breve{},\downarrow,A)$ is +complete.+\end{theorem}+++\section{Tuning the Engine: Proof Procedures for Frame Classes}++The calculus and proof engine give a systematic search for Kripke+models, without imposing any constraint on the kind of Kripke+model. In other words, it interprets `validity' as `validity in models+based on the class of {\em all}\/ Kripke frames'. It is+straightforward to adapt our reasoning engine for hybrid logic to+other frame classes than the universal frame class. +Since we have a way of dealing with the universal modality, the only +thing we have to do is modify the start rule, by storing the appropriate+constraint for the frame class we want. Here are some examples:+\begin{description}+\item[Irreflexive Frames for $R_i$]+Modify the start rule to: +\[+ \cfrac{\text{start } \phi}+       {[m],+        [],+        [],+        [],+        [],+        [A \downarrow x. \Ibox{i} \neg x],+        [@ m \phi]}+\ m \text{ fresh  }+\]+\item[Reflexive Frames for $R_i$]+Modify the start rule to: +\[+ \cfrac{\text{start } \phi}+       {[m],+        [],+        [],+        [],+        [],+        [A \downarrow x. \Idia{i} x],+        [@ m \phi]}+\ m \text{ fresh  }+\]+\item[Transitive Frames for $R_i$]+Modify the start rule to: +\[+ \cfrac{\text{start } \phi}+       {[m],+        [],+        [],+        [],+        [],+        [A \downarrow x. \Ibox{i}\Ibox{i}\Icdia{i}x],+        [@ m \phi]}+\ m \text{ fresh  }+\]+\item[S4 Frames for $R_i$]+Modify the start rule to: +\[+ \cfrac{\text{start } \phi}+       {[m],+        [],+        [],+        [],+        [],+        [A \downarrow x. (\Idia{i} x \land \Ibox{i}\Ibox{i}\Icdia{i}x)],+        [@ m \phi]}+\ m \text{ fresh  }+\]+\end{description}  +It is obvious that this can be done for any frame class that can be+described (hence characterized) by a formula in the first order+correspondence language of hybrid logic. This is so since we have the+full power of quantification available now; see+\cite{BlaSel:what98}. This gives the following:++\begin{theorem}[General Completeness] +The tableau calculus for ${\cal HL}(@,\breve{},\downarrow,A)$ is+complete for any frame class that can be described in the first order+correspondence language of ${\cal HL}(@,\breve{},\downarrow,A)$.+\end{theorem}++\section{Modifying the Calculus for Minimal Model Generation}++A model $\M$ is minimal for $\phi$ if there are $g,w$ with $\M, g, w+\forces \phi$, and for all $\N,h,w'$ with $\N,h, w' \forces \phi$ it+holds that $|N| \geq |M|$. E.g., the formula $\neg c \land+\Box\Diamond \top$ has minimal models of size $2$.++To generate minimal models, replace the $\Idia{i}$ and $\Icdia{i}$ +rules by the following trial-and-error versions: ++\paragraph{$\Idia{i}$ rules, trial-and-error version}++\[+\cfrac{@n \Idia{i}\phi}{+ \begin{array}{c}  nRk_1 \\+                   @ k_1 \phi+   \end{array}+ | + \cdots + | + \begin{array}{c}  nRk_s \\+                   @ k_s \phi+   \end{array}+ | + \begin{array}{c}  nRm  \\+                   @m \phi+   \end{array}+  }\text{ $k_1, \ldots k_s$ all nominals on the branch,  +               $m$ fresh}+\]++\[+\cfrac{@n \neg \Ibox{i} \phi}{+ \begin{array}{c}  nRk_1 \\+                   @ k_1 \neg \phi+   \end{array}+ | \cdots | + \begin{array}{c}  nRk_s  \\+                   @ k_s \neg \phi+   \end{array}+ |+ \begin{array}{c}  nRm  \\+                   @ m \neg \phi+   \end{array}+  }\text{ $k_1, \ldots k_s$ all nominals on the branch,+                           $m$ fresh}+\]++\paragraph{$\Icdia{i}$ rules, trial-and-error version}++\[+\cfrac{@n \Icdia{i}\phi}{+ \begin{array}{c}  k_1Rn \\+                   @ k_1 \phi+   \end{array}+ | + \cdots + | + \begin{array}{c}  Rk_sRn \\+                   @ k_s \phi+   \end{array}+ | + \begin{array}{c}  mRn \\+                   @m \phi+   \end{array}+  }\text{ $k_1, \ldots k_s$ all nominals on the branch,  +               $m$ fresh}+\]++\[+\cfrac{@n \neg \Icbox{i} \phi}{+ \begin{array}{c}  k_1Rn \\+                   @ k_1 \neg \phi+   \end{array}+ | \cdots | + \begin{array}{c}  k_sRn  \\+                   @ k_s \neg \phi+   \end{array}+ |+ \begin{array}{c}  mRn  \\+                   @ m \neg \phi+   \end{array}+  }\text{ $k_1, \ldots k_s$ all nominals on the branch,+                           $m$ fresh}+\]+Similarly, replace the $E$ rule also by its trial-and-error version. ++\begin{figure}[htbp]+\begin{center}+$ + \pstree[nodesep=3pt,levelsep=1.2cm,treesep=3cm]%+  {\Tr{ +@ s \Diamond \neg s, @ s \Box \downarrow x. \Diamond (\neg s \land \neg x),+@ s \Box \Box \downarrow x. @ s \Diamond x+                                                              }}{+    \pstree{\Tr{+       sRt, @ t \neg s+                                                              }}{+    \pstree{\Tr{+      t \NEQ s+                                                              }}{+    \pstree{\Tr{+      @ t \downarrow x. \Diamond (\neg s \land \neg x)+                                                              }}{+    \pstree{\Tr{+     @ t \Diamond (\neg s \land \neg t)+                                                              }}{+    \pstree{\Tr{+      tRt', t' \NEQ s, t' \NEQ t+                                                              }}{+    \pstree{\Tr{+      @t \Box \downarrow x . @ s \Diamond x+                                                              }}{+    \pstree{\Tr{+      @t'\downarrow x . @ s \Diamond x+                                                              }}{+    \pstree{\Tr{+      @t' @ s \Diamond t'+                                                              }}{+    \pstree{\Tr{+      @ s \Diamond t' +                                                              }}{+    \pstree{\Tr{+      sRt'+                                                              }}{+    \pstree{\Tr{+     @ t' \downarrow x. \Diamond ( \neg s \land \neg x)+                                                              }}{+    \pstree{\Tr{+     @ t' \Diamond ( \neg s \land \neg t')+                                                              }}{+    \pstree{\Tr{+     t'Rt'', t'' \NEQ s, t'' \NEQ t'+                                                              }}{\Tr{\vdots}}+}+}+}+}+}+}+}+}+}+}+}+}+}+$ +\end{center}+\caption{Tableau for (\ref{NinfConj}).} + \label{FigNinfConj}+\end{figure}++\begin{figure}[htbp]+\begin{center}+$ + \pstree[nodesep=3pt,levelsep=1.2cm,treesep=1cm]%+  {\Tr{ +@ s \Diamond \neg s, @ s \Box \downarrow x. \Diamond (\neg s \land \neg x),+@ s \Box \Box \downarrow x. @ s \Diamond x+                                                              }}{+    \pstree{+     \Tr{+       sRs, @s \neg s+                                                              }}{+            \Tr{\bot}}+    \pstree{+     \Tr{+       sRt, @ t \neg s+                                                              }}{+    \pstree{\Tr{+      t \NEQ s+                                                              }}{+    \pstree{\Tr{+      @ t \downarrow x. \Diamond (\neg s \land \neg x)+                                                              }}{+    \pstree{\Tr{+     @ t \Diamond (\neg s \land \neg t)+                                                              }}{+       \pstree{\Tr{tRs, @s(\neg s \land \neg t)}}+               {\Tr{\begin{array}{c}+                    \vdots \\+                    \bot +                    \end{array}}}+       \pstree{\Tr{tRt, @s(\neg s \land \neg t)}}+               {\Tr{\begin{array}{c}+                    \vdots \\+                    \bot +                    \end{array}}}+    \pstree{\Tr{+      tRt', t' \NEQ s, t' \NEQ t+                                                              }}{+    \pstree{\Tr{+      @t \Box \downarrow x . @ s \Diamond x+                                                              }}{+    \pstree{\Tr{+      @t'\downarrow x . @ s \Diamond x+                                                              }}{+    \pstree{\Tr{+      @t' @ s \Diamond t'+                                                              }}{+    \pstree{\Tr{+      @ s \Diamond t' +                                                              }}{+    \pstree{\Tr{+      sRt'+                                                              }}{+    \pstree{\Tr{+     @ t' \downarrow x. \Diamond ( \neg s \land \neg x)+                                                              }}{+    \pstree[nodesep=3pt,levelsep=1.7cm,treesep=1cm]{\Tr{+     @ t' \Diamond ( \neg s \land \neg t')+                                                              }}{+            \Tr{\begin{array}{c}+                    t'Rs \\+                    \vdots \\+                    \bot +                    \end{array}}+            \Tr{\begin{array}{c}+                    t'Rt' \\+                    \vdots \\+                    \bot +                    \end{array}}+             \Tr{\begin{array}{c}+                    t'Rt \\+                    \vdots \\+                    \text{open}+                    \end{array}}+             \Tr{\begin{array}{c}+                    t'Rt'' \\+                    \vdots+                    \end{array}}+}+}+}+}+}+}+}+}+}+}+}+}+}+$ +\end{center}+\caption{Trial-and-error tableau for (\ref{NinfConj}).} + \label{FigTENinfConj}+\end{figure}++Figure \ref{FigNinfConj} gives an infinite tableau expansion for +Formula \sref{NinfConj}. ++\begin{equation} \label{NinfConj}+@ s \Diamond \neg s \land  +@ s \Box \downarrow x. \Diamond (\neg s \land \neg x)+\land+@ s \Box \Box \downarrow x. @ s \Diamond x+\end{equation}++Still, the formula has finite models, and we can find finite models of+minimal size by means of (the proof engine based on) the+trial-and-error version of the tableau system. See Figure+\ref{FigTENinfConj}.++Again, the new rules are obviously sound, so we get: +\begin{theorem}+The minimal model calculus for ${\cal HL}(@,\breve{},\downarrow,A)$ is+sound.+\end{theorem}+The rules lead to an obvious modification of the proof engine, +which gives us a fair proof procedure for minimal model generation. +From this, by the same reasoning as above: ++\begin{theorem}+The minimal model calculus for ${\cal HL}(@,\breve{},\downarrow,A)$ is +complete.+\end{theorem}++\commentout{+\section{Generation of Minimal Models Through Node Compression}++Open branches in finished tableaux in general correspond to partial+models rather than full models. E.g., in the propositional case, it+does not matter what truth value one assigns to proposition letters+not mentioned along open branches+\cite{Benthem:panicl}. The same phenomenon presents itself in +the case of hybrid logic. In general, an open tableau node of the form+$(U,A,I,P,N,C,[])$ for $\phi$ can be used to generate a whole range of+Kripke models for $\phi$, including minimal models. The following node+compression algorithm accomplishes this.++\bc+   \begin{center}{ \bf Node Compression Algorithm }\end{center}++Let a finished open constraint tableau node $(U,A,I,P,N,C,[])$ be+given. +\begin{itemize}+\item If there are no pairs of nominals $m,n$ with $m$ preceding $n$+and $m\NEQ n \notin I$ then return the unit list+$[(U,A,I,P,N,C,[])]$. +\item Otherwise, nondeterministically pick a pair of+nominals $m,n$ with $m$ preceding $n$ and $m\NEQ n \notin I$.+\begin{description}+\item[Compression Step] Develop the tableau +      $[(U^n_m,A^n_m,I^n_m,P^n_m,N^n_m,[],C^n_m)]$. +   \begin{itemize} +     \item If this remains open, then compress the finished open nodes+           and collect the results. +     \item If it closes, then compress $(U,A,(m\NEQ n:I),P,N,C,[])$.+    \end{itemize}+\end{description}+\end{itemize}+\ec++\begin{theorem}[Soundness of Node Compression Algorithm]+If the node compression algorithm is applied to a finished open tableau node +for $\phi$, then all finished open tableau nodes that result from the +algorithm satisfy $\phi$. +\end{theorem}+\begin{proof}+Induction on the number of nominal pairs $m,n$ +with $m$ preceding $n$ and $m \NEQ n \notin I$ on a finished open +tableau node for $\phi$. +\end{proof}++\begin{theorem}[Completeness of Node Compression Algorithm]+If the node compression algorithm is applied to a finished open tableau+node for $\phi$ it yields at least one open node +\[+  (U,A,I,P,N,C,[])+\]+that corresponds to a minimal model for $\phi$.+\end{theorem}+\begin{proof}+If the algorithm is called with a finite node, termination is ensured,+for every step either removes a pair $m,n$ from the list of candidates+for merging, or merges the pair. Also, upon termination, there are+open nodes, for if $(U,A,I,P,N,C,[])$ is open then +\[ + (U,A,(m\NEQ n:I),P,N,C,[])+\]+is open. Since the resulting open nodes cannot be+compressed any further, at least one of them is minimal.+\end{proof}++To define the notion of a minimal model for a fragment of hybrid logic+per se, we can use the notion of a hybrid bisimulation+\cite{Areces:le,AreBlaMar:hlcic}, with the obvious extension to +take care of the converse modalities. A Kripke model $\M$ is minimal+for a hybrid language if for all models $\N$, all sequences $\bar{m}+\in {}^k M$ and $\bar{n} \in {}^k N$, any hybrid bisimulation (for+that language) $\stackrel{\omega}{\sim}$ with $(\M, \bar{m})+\stackrel{\omega}{\sim} (\N, \bar{n})$ and $\bar{m}(i) = \bar{m}(j)$+satisfies $\bar{n}(i) = \bar{n}(j)$. Intuitively, $\M$ is minimal +for some hybrid logic language if no distinct worlds in $\M$ are ever +identified by a hybrid bisimulation for that language. We leave the +investigation of this notion for a future occasion.+}++\section{Deciding Some Fragments of Hybrid Logic}++It is well known that ${\cal HL}(@)$ and ${\cal HL}(@,\breve{})$ are+decidable. Theorem \ref{PdecidesAt} states that the constraint proof+engine from Section \ref{PP} decides hybrid logic formulas without+binders.++\begin{theorem} \label{PdecidesAt}+The constraint proof engine for hybrid logic decides satisfiability of+${\cal HL}(@,\breve{})$ formulas. +\end{theorem}+\begin{proof}+The result follows from a modal depth argument. ${\cal+HL}(@,\breve{})$ has a notion of finite degree (\cite{BlaRijVen:ml},+Ch. 7); in particular, modal depth for its formulas can be defined as+follows:+\begin{eqnarray*}+ d(p) = d(c) = d(x) & = & 0 \\+ d(\phi * \psi)     & = & \max(d(\phi), d(\psi)), +                          * \in \{ \land, \lor, \rightarrow \} \\+ d(\neg \phi)       & = & d(\phi) \\+ d(M \phi)          & = & d(\phi) + 1, +               M \in \{ \Ibox{i}, \Idia{i}, \Icbox{i}, \Icdia{i} \} \\+ d(@ m \phi)        & = & d(\phi) +\end{eqnarray*}+Every non-literal formula $\phi \notin \{\Ibox{i}, \Icbox{i} \}$ gets+decomposed by the rule that applies to it. Every formula $\phi \in+\{\Ibox{i},+\Icbox{i} \}$ generates a constraint. When a constraint $@ m \Box+\phi$ is combined with an $mRn$ relation, it generates a new formula+$@ n \phi$ on the list of pending formulas, but $d(\phi) = d(\Box\phi)+- 1$. Thus, the box formula $@m \Box \phi$ gets replaced by a finite+number of $@ n \phi$ formulas, and each of these is appended to the+list of pending formulas, so fairness of the procedure is preserved. +\end{proof}++\commentout{+At first sight, there is something puzzling about the undecidability+of ${\cal HL}(@,\breve{},\downarrow)$, especially since the so-called+standard translation given in \cite{Areces:le,AreBlaMar:hlcic} seems+to suggest that hybrid sentences (hybrid formulas without unbound+world variables) are in the two-variable bounded fragment of first+order logic. In fact, the translation instruction has a flaw, as can+be seen when we use it to translate the transitivity sentence+$\downarrow u . \Box \Box \downarrow w. @ u \Diamond w$. Carrying out+the instruction starting out from $\text{ST}_x(\downarrow u . \Box+\Box \downarrow w. @ u \Diamond w)$, we end up with an injunction to+substitute $x$ for $u$ in $\forall y (Rxy \rightarrow \forall x (Ryx+\rightarrow \exists y (Ruy \land y = x)))$, with capture of $x$ by+$\forall x$ as a result. The standard translation can be repaired by+replacing the instructions for the modalities and the binders as+follows:+\begin{eqnarray*}+ \text{ST}_x (\Idia{i}\phi) & := & \exists y (R_ixy \land \text{ST}_y+ \phi) \text{ with $y$ a fresh variable,} \\ + \text{ST}_x (\downarrow  w.\phi) +  & := & (\text{ST}_y \phi)^w_y \text{ with $y$ a fresh+ variable.}+\end{eqnarray*}+A fresh variable, of course, is a variable that has not been used+before in the translation. This makes clear that the translation does+not ensure a bound on the number of variables that are needed. E.g.,+the translation of the transitivity sentence needs as least three+different variables.++We will now demonstrate that it is the presence of $\downarrow$ in the+scope of box modalities that causes undecidability of ${\cal+HL}(@,\breve{},\downarrow)$. Consider the version of ${\cal+HL}(@,\breve{},\downarrow)$ without $\Ibox{i}, \Icbox{i}, \rightarrow$+that can be got by paraphrasing d with the help of $\Ibox{i} \phi+\leftrightarrow \neg \Idia{i}\neg \phi$, $\Icbox{i} \phi+\leftrightarrow \neg \Icdia{i}\neg \phi$, and $(\phi \rightarrow \psi)+\leftrightarrow \neg \phi \lor \psi$.  A subformula $\psi$ of $\phi$+is {\em existential}\/ in $\phi$ if every $\Diamond$ that outscopes+$\psi$ in $\phi$ is in the scope of an even number of negation+operators. Thus, $\psi$ is existential in $\Diamond+\neg \psi$ and $@ m \neg(\Diamond m \land \neg \Diamond \psi)$,+but not in $\neg \Diamond \psi$. Call a formula $\phi$ {\em+innocent}\/ if every binder subformula $\downarrow x. \psi$ of $\phi$+is existential in $\phi$.++\begin{theorem}+The innocent fragment of  ${\cal HL}(@\breve,\downarrow)$+is decidable. +\end{theorem}+\begin{proof}+Consider the following translation from (located formulas of) ${\cal+HL}(@,\breve{},\downarrow)$ to ${\cal HL}(@,\breve{})$. +\begin{eqnarray*} +  (@m p)^T    & :=  & @m p \\+  (@m n)^T    & :=  & @m n \\+  (@m \neg \phi)^T & :=  & \neg (@ m\phi)^T \\+  (@m \phi \land \psi)^T & :=  & (@ m\phi)^T \land  (@ m\psi)^T \\+  (@m \phi \lor \psi)^T & :=  & (@ m\phi)^T \lor  (@ m\psi)^T \\+  (@m @n \phi)^T  & :=  & (@ n \phi)^T \\+  (@m \Idia{i}\phi)^T & :=  & @m \Idia{i} (n \land (@ n \phi)^T), +   \text{ $n$ a fresh nominal } \\+  (@m \Icdia{i}\phi)^T & :=  & @m \Icdia{i} (n \land (@ n \phi)^T), +   \text{ $n$ a fresh nominal } \\+  (@m \downarrow x. \phi)^T & := & (@ m \phi [ x:= m])^T+\end{eqnarray*}+Check by induction on formula structure that this translation is+truth-preserving for all formulas in the innocent fragment.+\end{proof}++Another way of seeing this is by observing that the tableaux for + $\phi$ and $\phi^T$ are essentially the same, which leads immediately +to: +\begin{theorem}+The constraint proof engine for ${\cal HL}(@,\breve{},\downarrow)$ +decides the innocent fragment. +\end{theorem}++}++Consider the following fragment of {\em existential}\/ formulas of +${\cal HL}(@,\breve{})$:+\begin{eqnarray*}+  \psi & ::= & n \mid \neg n \mid \neg \Idia{i} n \mid  +   \neg \Icdia{i} n \mid  \psi \land \psi' \mid \psi \lor \psi'+  \mid  \Idia{i} \psi \mid  \Icdia{i} \psi +\end{eqnarray*}+Use this to define ${\cal HL}(@,\breve{},\downarrow^\exists)$, +by changing the definition of binder formulas from $\downarrow x. +\phi$ to  $\downarrow x. \psi$. In other words, binding is only +allowed over existential formulas. If, moreover, we only allow one +binding variable $w$, we get \cite{Marx02:nsas}: ++\begin{theorem}[M. Marx]+The language ${\cal HL}(@,\breve{},(\downarrow w)^\exists)$ is +decidable in EXPTIME. +\end{theorem}+\begin{proof}+Using a standard translation we can map this language to the universal+guarded fragment (where universal quantifiers are guarded, but+existential quantifiers need not be) in three variables $x,y,w$. By a+remark in \cite{Graedel:otrpog}, existential guards can be dispensed+with, for the sentence $(\forall \bfx . \alpha) \exists \bfy+\phi(\bfx\bfy)$, with $\exists \bfy$ unguarded, is satisfiable if and+only if the properly guarded sentence $(\forall \bfx . \alpha) \exists+\bfy R\bfx\bfy\ \land (\forall \bfx . R\bfx \bfy) \phi(\bfx\bfy)$,+with $R$ a new relation symbol of the appropriate arity, is+satisfiable. Satisfiability of the universal guarded fragment in a+bounded number of variables is shown to be decidable in EXPTIME in+\cite{Graedel:otrpog}.+\end{proof}++If we allow an unrestricted number of binding variables $x_1, \ldots$+the fragment is still decidable, but since there is no bound now on the +number of variables employed in the translation, the complexity is +in 2EXPTIME \cite{Graedel:otrpog}.++\begin{theorem} +The constraint proof engine for hybrid logic decides satisfiability of+${\cal HL}(@,\breve{},\downarrow^\exists)$ formulas.+\end{theorem}+\begin{proof}+Suppose the proof engine is invoked to check satisfiability of+$\phi$. We only need to be concerned about formulas of the forms+$\Ibox{i} \downarrow x .\psi$, $\Idia{i} \neg \downarrow x. \psi$,+$\Icbox{i} \downarrow x . \psi$ $\Icdia{i} \neg\downarrow x . \psi$ that+turn up along a tableau branch during the processing of $\phi$, for+these are the formulas that cause binders to appear in the $\Ibox{i}$+and $\Icbox{i}$ constraints. Suppose $@m \Box \downarrow x. \psi$ is+in the box constraint store, and gets combined with an $mRn$+accessibility along the branch. Then $@n \downarrow x. \psi$ will get+appended to the pending formula list. When $@n \downarrow x. \psi$+gets decomposed, it gets replaced by $\psi^x_n$, and further+decomposition will not affect the constraint stores because $\psi$ is+existential.+\end{proof}++\section{Related Work}++%\paragraph{Comparison with other tableau systems}+Tableau calculi for hybrid logic are still in their infancy. A+prefixed tableau calculus along the lines of the prefixed tableau+style theorem proving of \cite{Fitting:pmfmail} is given in+\cite{Tzakova:tcfhl}. This does not yet make full use of the+possibility to let the role of prefixes be played by nominals. In+\cite{Blackburn:ild} it is pointed out that nominals can play the role+of labels in labelled deduction style theorem proving, and a tableau+calculus is proposed that handles equality reasoning on nominals by+means of rewrite rules that express reflexivity, symmetry and+transitivity of equality, and that allows substitution of equal+nominals. However, since this rewrite system is not normalizing,+equality reasoning in the resulting calculus is awkward, and proof+engines based on it will spend too much effort on pointless+rewrite steps for equality \cite{BlaBurWal:hydr01}.+%\paragraph{Comparison with resolution for hybrid logic}+%The resolution approach to modal logic dates back to at least+%\cite{Ohlbach88:arcfml,EnjFar89:mricf}. +A prefixed resolution calculus for description and hybrid logic was+proposed in \cite{AreNivRij:reso01}, and implemented in+\cite{AreHeg01:hylores}. Detailed efficiency comparison with this +is work in progress. ++++\paragraph{Acknowledgement} +Thanks to the Dynamo team (Wim Berkelmans, Balder ten Cate, Juan+Heguiabehere, Breannd\'an \'O Nuall\'ain) and to Carlos Areces,+Patrick Blackburn and Maarten Marx, for useful comments and fruitful+discussion. This work was carried out as part of the INRIA funded+partnership between LITG (Language and Inference Technology Group at+ILLC, University of Amsterdam) and LED (Langue et Dialogue, LORIA,+Nancy).+++\bibliographystyle{acm}+\bibliography{/home/jve/texmacros/mybibAG,/home/jve/texmacros/mybibHZ}+++\end{document}+
+ examples/runsat.sh view
@@ -0,0 +1,10 @@+#!/bin/bash++BINPATH="../dist/build/hylotab/hylotab"+FORMPATH="sat"++for file in `ls ${FORMPATH}/*`;+do echo $file;${BINPATH} -f $file $1 $2 $3 $4;+done++
+ examples/rununsat.sh view
@@ -0,0 +1,10 @@+#!/bin/bash++BINPATH="../dist/build/hylotab/hylotab"+FORMPATH="unsat"++for file in `ls ${FORMPATH}/*`;+do echo $file;${BINPATH} -f $file $1 $2 $3 $4;+done++
+ examples/sat/form04.frm view
@@ -0,0 +1,3 @@+begin+ <>(n1 & (<>n1) & ([]<>n1))+end
+ examples/sat/form05.frm view
@@ -0,0 +1,5 @@+begin+ down x1 . [][] <->x1 ;  { transitivity } + [] down x1 . <> true ;  { irreflexivity }+ <>true                  { initial successor }+end
+ examples/sat/form06.frm view
@@ -0,0 +1,5 @@+begin+ ([R1](<R3>p1 v p3)) <--> ([R3](p3 -> <R2>-p3));+ [R2](p1 -> <R2>(p1 <--> (p3 v p4 v -p5)));+ [R1][R2][R3](p1 v -p3 v -p5)+end
+ examples/sat/form08.frm view
@@ -0,0 +1,12 @@+begin++@ N1 (  (<>true)+      & ([][]<->N1)+      & ([] (   (<>true)+              & (down x1 . []-x1)+              & (down x1 . [][]-x1)+              & (down x1 . [][]<->x1)+            )+        )+     )+end
+ examples/sat/form09.frm view
@@ -0,0 +1,13 @@+begin++@ N1 (  (<>true)+      & (<><>true)+      & ([][]<->N1)+      & ([] (   (<>true)+              & (down x1 . []-x1)+              & (down x1 . [][]-x1)+              & (down x1 . [][]<->x1)+            )+        )+     )+end
+ examples/sat/form11.frm view
@@ -0,0 +1,9 @@+begin++@ n1 -<>n1;+@ n1 <>true;+@ n1 [][] down x1 . @ n1 <> x1;+@ n1 [] down x1 . [] down x2 . @ x1 [] down x3 .@ x1 [] down x4 . ((@ x2 x3 ) v (@ x2 x4) v (@ x3 x4));+@ n1 [] down x1 . [][] down x2 . @ x1 [][] down x3 . @ x1 [][] down x4 . @ x1 [][] down x5 . ((@ x2 x3) v (@ x2 x4) v (@ x2 x5) v (@ x3 x4) v (@ x3 x5) v (@ x4 x5))++end
+ examples/sat/form12.frm view
@@ -0,0 +1,13 @@+begin++<>p1;+<>(p1 & <>p1);+[] (p1 & (<>p1) & (<>(<>-p1 & []p2)));+[]-p2;+(p1 <--> p3);+[](p1 <--> p3);+(p11 v p12 v p13 v p14 v p15);+(-p11 v -p12 v -p13);+[][][](p11 <--> p12)++end
+ examples/sat/form13.frm view
@@ -0,0 +1,6 @@+begin+<>p1 ;+<><>-p1;+<><><>p1;+[](p1 & [](-p1 & [](p1 & []-p1)))+end
+ examples/sat/form14.frm view
@@ -0,0 +1,7 @@+begin+<>p1;+<><>-p1;+<><><>p1;+<><><><>-p1;+[](p1 & [](-p1 & [](p1 & [](-p1 & []p1))))+end
+ examples/sat/form15.frm view
@@ -0,0 +1,9 @@+begin+<>p1;+<><>-p1;+<><><>p1;+<><><><>-p1;+<><><><><>p1;+<><><><><><>-p1;+[](p1 & [](-p1 & [](p1 & [](-p1 & [](p1 & []-p1)))))+end
+ examples/sat/form16.frm view
@@ -0,0 +1,5 @@+begin+ ([R1](<R3>p1 v p3) <--> [R3](p3 -> <R2>-p3));+ [R2](p1 -> <R2>(p1 <--> (p3 v p4 v -p5)));+ [R1][R2][R3] (p1 v -p3 v -p5)+end
+ examples/sat/form17.frm view
@@ -0,0 +1,9 @@+begin++(@ n1 p1) v (@ n2 p2) v (@ n3 p3) v (@ n4 p4); +[]-p1;+[]-p2;+[]-p3;+[]-p4++end
+ examples/sat/form18.frm view
@@ -0,0 +1,11 @@+begin+<>p1;+<>(p1 & <>p1);+[] (p1 & (<>p1) & <>(<>-p1 & []p2));+[]-p2;+(p1 <--> p3);+[](p1 <--> p3);+(p11 v p12 v p13 v p14 v p15);+(-p11 v -p12 v -p13);+[][][](p11 <--> p12)+end
+ examples/sat/form23.frm view
@@ -0,0 +1,6 @@+begin+  (- <> @ n1 n2)+v (- @ n1 (<>p2 -> p1)) +v (- @ n2 <>p2)+v (@ n1 p1)+end
+ examples/sat/form27.frm view
@@ -0,0 +1,3 @@+begin+ (@ n2 (p2 v p1) -> @n1 p3)+end
+ examples/sat/form28.frm view
@@ -0,0 +1,5 @@+begin++ -(@ n2 (p1 v p2) -> @n1 p3)++end
+ examples/unsat/form01.frm view
@@ -0,0 +1,5 @@+begin+<> (n1 & p2);+<>(n1 & p1);+[] (-p2 v -p1)+end
+ examples/unsat/form02.frm view
@@ -0,0 +1,4 @@+begin+   (@ n1 <>[-]-n1)+ v (@ n1 <->[]-n1)+end
+ examples/unsat/form03.frm view
@@ -0,0 +1,6 @@+begin+ <>p1;+ <>-p1;+ [](p1 -> n1);+ []p1+end
+ examples/unsat/form07.frm view
@@ -0,0 +1,5 @@+begin++down x1 .  []<>x1 & -(<>[]p1 -> p1)++end
+ examples/unsat/form10.frm view
@@ -0,0 +1,5 @@+begin+ down x1 . [][]<->x1;  { transitive }+ down x1 . [][]-x1;    { asymmetric }+ down x1 . <>x1        { reflexive  }+end
+ examples/unsat/form19.frm view
@@ -0,0 +1,7 @@+begin++-(((p3 v (-p4 & p5)) <--> (p7 v (p4 -> p2))) <--> +  (((p3 v (-p4 & p5)) -> (p7 v (p4 -> p2))) & +   ((p7 v (p4 -> p2)) -> (p3 v (-p4 & p5)))))++end
+ examples/unsat/form20.frm view
@@ -0,0 +1,22 @@+begin+-(+   (+      (<><><><>(@ n1 n2))+      &+         @ n1 (+                 ([]<>(p1 v @ n2 (p1 <--> <>p3)))+                 ->+                 (<>p1 <--> []<>(@n2 (n3 & P4)))+              )+   )++   ->++   (+      @ n2 ([]<>(p1 v @ n2 (p1 <--> <>p3)))+      ->+      @ n1 (<>p1 <--> []<>(@ n2 (n3 & P4)))+   )+)++end
+ examples/unsat/form21.frm view
@@ -0,0 +1,22 @@+begin+-(+   (+      <>(@n1 n2)+      &+         @ n1 (+                 ([]<>(p1 v @ n2 (p1 <--> <>p3)))+                 ->+                 (<>p1 <--> []<>(@n2 (n3 & P4)))+              )+   )++   ->++   (+      @ n2 ([]<>(p1 v @ n2 (p1 <--> <>p3)))+      ->+      @ n1 (<>p1 <--> []<>(@ n2 (n3 & P4)))+   )+)++end
+ examples/unsat/form22.frm view
@@ -0,0 +1,6 @@+begin+<>(@n1 n2);+@ n1 ([]p1 -> p2);+@ n2 []p1;+- @ n1 p2+end
+ examples/unsat/form24.frm view
@@ -0,0 +1,9 @@+begin++- ( +   (@ n1 (n2 & (@ n1 (p2 v @ n2 p1) -> p3)))+   -> +   (@ n2 (p2 v @ n2 p1) -> @n1 p3)+  )++end
+ examples/unsat/form25.frm view
@@ -0,0 +1,8 @@+begin+ ( +   (@ n1 n2 & @ n1 ((p2 v @ n2 p1) -> p3))+    & +   - (@ n2 (p2 v @ n2 p1) -> @n1 p3)+  )++end
+ examples/unsat/form26.frm view
@@ -0,0 +1,6 @@+begin+<>@ n1 n2;+@ n1 (p2 -> @n2 p1);+@n1 p2;+- @ n2 p1+end
+ hylotab.bib view
@@ -0,0 +1,31 @@+@Unpublished{Eijck02:lthl,+  author = 	 {Eijck, J. van},+  title = 	 {Labelled Tableaux for Hybrid Logics},+  note = 	 {manuscript, {CWI}},+  OPTkey = 	 {},+  OPTmonth = 	 {},+  year = 	 {2002},+  OPTannote = 	 {}+}++@Unpublished{Eijck02:lcwl,+  author = 	 {Eijck, J. van},+  title = 	 {Loop Checking with Labels}+  note = 	 {manuscript, {CWI}},+  OPTkey = 	 {},+  OPTmonth = 	 {},+  year = 	 {2002},+  OPTannote = 	 {}+}++@Unpublished{Eijck02:hylotab,+  author = 	 {Eijck, J. van},+  title = 	 {Hy{L}o{T}ab --- +                 {T}ableau-based Theorem Proving for Hybrid Logics},+  note = 	 {manuscript, {CWI}, +                  available from \verb^http://www.cwi.nl/~jve/hylotab^}, +  OPTkey = 	 {},+  OPTmonth = 	 {},+  year = 	 {2002},+  OPTannote = 	 {}+}
+ hylotab.cabal view
@@ -0,0 +1,39 @@+Name:                hylotab+Version:             1.2.0+Homepage:            http://www.glyc.dc.uba.ar/intohylo/hylotab.php+Synopsis:            Tableau based theorem prover for hybrid logics+Description:         HyLoTab is a proof-of-concept tableaux prover for+                     hybrid logics originally written in 2002 by Jan van Eijck.+                     It is no longer developped, but we made it compatible+                     with the syntax used in HyLoLib to easen comparison+                     with other provers.+License:             GPL+License-file:        LICENSE+Author:              Jan van Eijck, Guillaume Hoffmann+Maintainer:          guillaumh@gmail.com+Category:            Theorem Provers+Cabal-version:       >= 1.6.0+Build-type:          Simple++data-files: NF.tex+            hylotab.bib+            cthl.tex+            examples/*.sh+            examples/sat/*.frm+            examples/unsat/*.frm++Flag static+  Description: Build a static binary+  Default:     False++Executable          hylotab+  Main-is:             Main.hs+  Other-modules:       Form Hylotab+  Build-Depends:       base >= 4, base < 5,+                       mtl >= 1, mtl < 2,+                       hylolib >= 1.3, hylolib < 1.4+  hs-source-dirs:      src+  ghc-options:          -Wall+  ghc-prof-options:    -auto-all+  if flag(static)+    ghc-options: -static -optl-static -optl-pthread
+ src/Form.hs view
@@ -0,0 +1,85 @@+module Form+( Form(..),  PropSymbol(..), NomSymbol(..), RelSymbol(..), Rel, parse )+where++import HyLo.Signature.Simple( PropSymbol(..),+                              NomSymbol(..),+                              RelSymbol(..) )++import qualified HyLo.InputFile as InputFile+import qualified HyLo.Formula as F++type Rel  = Int++data Form =  Top+           | Bot+           | Prop PropSymbol+           | Nom  NomSymbol+           | Neg  Form+           | Conj [Form]+           | Disj [Form]+           | Impl Form Form+           | A    Form+           | E    Form+           | Box  RelSymbol Form+           | Dia  RelSymbol Form+           | At   NomSymbol Form+           | Down NomSymbol Form+     deriving (Eq,Ord)++instance Show Form where +   show Top                 = "T"+   show Bot                 = "F"+   show (Prop i)            = show i+   show (Nom i)             = show i+   show (Neg f)             = '-' : show f+   show (Conj [])           = "T" +   show (Conj fs)           = "(" ++ separate " & " fs ++ ")"+   show (Disj [])           = "F" +   show (Disj fs)           = "(" ++ separate " v " fs ++ ")"+   show (Impl f1 f2)        = "(" ++ show f1 ++ " -> " ++ show f2 ++ ")"+   show (A f)               = 'A' : show f+   show (E f)               = 'E' : show f+   show (Box name f)        = "[" ++ show name ++ "]" ++ show f+   show (Dia name f)        = "<" ++ show name ++ ">" ++ show f+   show (At nom f)          = show nom ++ ":" ++ show f+   show (Down i f)          = "down " ++ show i ++ "." ++ show f+++parse :: String -> Form+parse = convert . InputFile.parseOldFormat++convert :: [F.Formula NomSymbol PropSymbol RelSymbol] -> Form+convert fs = conv_ $ foldr1 (F.:&:) fs++conv_ :: F.Formula NomSymbol PropSymbol RelSymbol -> Form+conv_ F.Top            = Top+conv_ F.Bot            = Bot+conv_ (F.Prop p)       = Prop p+conv_ (F.Nom n)        = Nom n+conv_ (F.Neg f)        = Neg $ conv_ f+conv_ (f1 F.:&: f2)    = Conj $ flattenConj [conv_ f1,conv_ f2]+conv_ (f1 F.:|: f2)    = Disj $ flattenDisj [conv_ f1,conv_ f2]+conv_ (f1 F.:-->: f2)  = conv_ f1 `Impl` conv_ f2+conv_ (f1 F.:<-->: f2) = Conj [Impl cf1 cf2, Impl cf2 cf1] where cf1 = conv_ f1 ; cf2 = conv_ f2+conv_ (F.Diam r f)     = Dia r (conv_ f)+conv_ (F.Box r f)      = Box r (conv_ f)+conv_ (F.At n f)       = At n (conv_ f)+conv_ (F.A f)          = A (conv_ f)+conv_ (F.E f)          = E (conv_ f)+conv_ (F.Down v f)     = Down v (conv_ f)+conv_ _ = error "not implemented"++flattenConj :: [Form] -> [Form]+flattenConj []              = []+flattenConj (Conj conjs:fs) = flattenConj conjs ++ flattenConj fs+flattenConj ( f        :fs) = f : flattenConj fs++flattenDisj :: [Form] -> [Form]+flattenDisj []              = []+flattenDisj (Disj disjs:fs) = flattenDisj disjs ++ flattenDisj fs+flattenDisj ( f        :fs) = f : flattenDisj fs++separate :: Show a => String -> [a] -> String+separate _ [] = ""+separate s os = foldl1 (\a1 a2 -> (a1 ++ s ++ a2)) $ map show os
+ src/Hylotab.hs view
@@ -0,0 +1,836 @@+module Hylotab where ++import Data.List  ( nub, intersect, (\\) )+import Form ( Form(..), NomSymbol(..), PropSymbol(..), RelSymbol(..), Rel, parse )+import Control.Monad(when)++type Index    = Int+type Domain   = [NomSymbol]++{- Generic Satisfiability Checking -}++-- Distinguish between two modes of satisfiability checking: ++data Mode = Extend -- for extending with a new nominal at each+                   --                 encounter with a diamond+          | Try    -- for trial and error extension, including+                   --               checking existing nominals++-- If psi defines a frame property, then any model M satisfying (A psi)+-- will be in the frame class with that property. For suppose that+-- M does not have the frame property. Then there is a world w with+-- M , w |/= psi, hence M |/= A psi. Thus, we can+-- build an engine for the frame class of psi by loading the proof+-- engine with (A psi) as a universal constraint. This leads to the+-- following generic satisfiability checker (the first argument gives+-- the mode of satisfiability checking, the second argument lists the+-- formulas defining the frame class under consideration):++data SatFlag = SAT Tableau | UNSAT++genSat  :: Bool -> Mode -> [Form] -> Form -> IO SatFlag+genSat verbose Extend props form =+ do res <- expand verbose (initTab form props)+    case res of+     OPEN nodes -> return $ SAT nodes+     CLOSED     -> return UNSAT+genSat verbose Try    props form =+ do res <- cautiousExpand verbose (initTab form props)+    case res of+     OPEN nodes -> return $ SAT nodes+     CLOSED     -> return UNSAT++{- Theorem Proving -}++-- The function initTab creates an initial tableau for a+-- formula. The initial tableau for phi is just one node, with list of+-- pending formulas [@ m phi], where m is a fresh nominal. We assume+-- that no nominals of the form (N i) appear in the formula. The+-- node index is set to the index of the first fresh constant nominal,+-- i.e., 1.++initTab :: Form  -> [Form] -> Tableau +initTab form props = +   [Nd {idx = 1 + newIdx,+        dom = dom',+        neqs = [], accs = [], ufs = [],+        boxes = [], cboxes = [], pos = [],+        neg = [], forms= forms'+       }+   ]+  where noms = nomsInForms (form:props)+        newIdx = case noms of+                   [] -> 0+                   _  -> 1 + maximum [ n | (N n)  <- noms]+        newNom = N newIdx+        dom' =  newNom : nomsInForms (form:props)+        forms' = [At newNom form] +++                  case props of+                   []     -> []+                   [prop] -> [At newNom (A prop)]+                   _      -> [At newNom (A (Conj props))]++{- Tableau Nodes and Tableaux -}++                                                       -- A node of a tableau consists of +data Node = Nd {   idx :: Index,                       -- a tableau index (needed to generate fresh tableau parameters)+                   dom :: Domain,                      -- a domain (all nominals occurring at the node)+                  neqs :: [(NomSymbol,NomSymbol)],     -- a list of n != m constraints on the node+                  accs :: [(NomSymbol,Rel,NomSymbol)], -- a list of n<Ri>m accessibilities on the node +                   ufs :: [Form],                      -- the A formulas that have been applied to all nominals in the domain of the node +                 boxes :: [(NomSymbol,Rel,Form)],      -- the (@n [i] phi) formulas of the node that have been combined+                                                       -- with all the (n<i>m) accessibilities on the node+                                                       -- (the boxed constraints of the node)+                cboxes :: [(NomSymbol,Rel,Form)],      -- the (@n [-i] phi) formulas of the node that have+                                                       -- been combined with all the (m<i>n) accessibilities on the node+                                                       -- (the converse boxed constraints of the node)+                   pos :: [(NomSymbol,PropSymbol)],    -- the positive atom attributions (@ n p_i) on the node+                   neg :: [(NomSymbol,PropSymbol)],    -- the negative atom attributions (@ n - p_i) on the node+                 forms :: [Form]                       -- pending formulas yet to be treated by the proof engine +               }+              deriving (Eq)++instance Show Node where+ show nd+   = unlines ["Node:",+              "index: "    ++ show (idx nd),+              "domain: "   ++ show (dom nd),+              "neqs: "     ++ show (neqs nd),+              "accs: "     ++ show (accs nd),+              "ufs:  "     ++ show (ufs nd),+              "boxes: "    ++ show (boxes nd),+              "cboxes: "   ++ show (cboxes nd),+              "pos: "      ++ show (pos nd),+              "neg: "      ++ show (neg nd),+              "formulas: " ++ show (forms nd)]++type Tableau = [Node]++-- collect the constant nominals and the free occurrences of+-- variable nominals from a formula or a formula list. +nomsInForm :: Form -> [NomSymbol]+nomsInForm (Nom nom)      = [nom]+nomsInForm (Neg f)        = nomsInForm f+nomsInForm (Conj fs)      = nomsInForms fs+nomsInForm (Disj fs)      = nomsInForms fs+nomsInForm (Impl f1 f2)   = nomsInForms [f1,f2]+nomsInForm (A f)          = nomsInForm f+nomsInForm (E f)          = nomsInForm f+nomsInForm (Box _ f)      = nomsInForm f+nomsInForm (Dia _ f)      = nomsInForm f+nomsInForm (At nom f)     = add nom (nomsInForm f)+nomsInForm (Down x f)     = filter (/= x) (nomsInForm f)+nomsInForm _              = []++nomsInForms :: [Form] -> [NomSymbol]+nomsInForms = nub . concatMap nomsInForm ++type Subst = (NomSymbol,NomSymbol)++-- Application of a substitution to a nominal:+appNom :: Subst -> NomSymbol -> NomSymbol+appNom (n,m) nom = if n == nom then m else nom ++-- Application of a substitution to a domain. Note that the substitution+-- may identify individuals, so after the substitutition we have to clean+-- up the list with nub to remove possible duplicates.+appDomain :: Subst -> Domain -> Domain+appDomain = map . appNom++appNNs :: Subst -> [(NomSymbol,NomSymbol)] -> [(NomSymbol,NomSymbol)]+appNNs b = map (\ (n,m) -> (appNom b n, appNom b m))++appNRNs :: Subst -> [(NomSymbol,Rel,NomSymbol)] -> [(NomSymbol,Rel,NomSymbol)]+appNRNs b = map (\ (n,r,m) -> (appNom b n, r, appNom b m))++appNPs :: Subst -> [(NomSymbol,PropSymbol)] -> [(NomSymbol,PropSymbol)]+appNPs b = map (\ (n,name) -> (appNom b n, name))++-- Application of a substitution to a formula or a formula list.  +-- Note that substitutions only affect the _free_ +-- variables of a formula++appF :: Subst -> Form -> Form +appF _ Top             = Top+appF _ Bot             = Bot+appF _ (Prop p)        = Prop p+appF b (Nom nom)       = Nom (appNom b nom)+appF b (Neg f)         = Neg (appF b f)+appF b (Conj fs)       = Conj (appFs b fs)+appF b (Disj fs)       = Disj (appFs b fs)+appF b (Impl f1 f2)    = Impl (appF b f1) (appF b f2)+appF b (A f)           = A (appF b f)+appF b (E f)           = E (appF b f)+appF b (Box r f)       = Box r (appF b f)+appF b (Dia r f)       = Dia r (appF b f)+appF b (At n f)        = At (appNom b n) (appF b f)+appF b (Down n f)      = Down (appNom b n) (appF b f) ++appFs :: Subst -> [Form] -> [Form]+appFs = map . appF ++appNRFs :: Subst -> [(NomSymbol,Rel,Form)] -> [(NomSymbol,Rel,Form)]+appNRFs b = map (\ (n,r,f) -> (appNom b n, r, appF b f))++{- Formulas compensating lack of pattern matching -}+  +isAlpha, isBeta :: Form -> Bool+isAlpha (Conj _)         = True+isAlpha (Neg (Disj _))   = True+isAlpha (Neg (Impl _ _)) = True+isAlpha _                = False +isBeta (Disj _)          = True+isBeta (Impl _ _)        = True +isBeta (Neg (Conj _))    = True+isBeta _                 = False++isA, isE :: Form -> Bool+isA (A _)             = True+isA (Neg (E _))       = True+isA _                 = False+isE (E _)             = True+isE (Neg (A _))       = True+isE _                 = False++isBox, isDiamond :: Form -> Bool+isBox (Box _ _)             = True+isBox (Neg (Dia _ _))       = True+isBox  _                    = False+isDiamond (Dia _ _)         = True+isDiamond (Neg (Box _ _))   = True +isDiamond  _                = False++isDown, isLabel :: Form -> Bool +isDown (Down _ _ )       = True+isDown (Neg (Down _ _ )) = True+isDown _                 = False +isLabel (At _ _)         = True+isLabel (Neg (At _ _))   = True+isLabel _                = False ++isTrue,isFalse,isPlit, isNlit :: Form -> Bool+isTrue Top              = True+isTrue _                = False+isFalse Bot             = True+isFalse _               = False+isPlit (Prop _)         = True +isPlit _                = False+isNlit (Neg (Prop _))   = True +isNlit _                = False ++isNom, isNgNom, isAcc, isDneg :: Form -> Bool+isNom (Nom _)                       = True +isNom  _                            = False +isNgNom (Neg (Nom _))               = True +isNgNom _                           = False +isAcc (Dia _ (Nom _))               = True+isAcc (Neg (Box _ (Neg (Nom _))))   = True+isAcc _                             = False+isDneg (Neg (Neg _))                = True+isDneg _                            = False++isInvRel :: Form -> Bool+isInvRel (Box (RelSymbol _)  _)         = False+isInvRel (Dia (RelSymbol _)  _)         = False+isInvRel (Neg (Box (RelSymbol _)    _)) = False+isInvRel (Neg (Dia (RelSymbol _)    _)) = False+isInvRel (Box (InvRelSymbol _) _)       = True+isInvRel (Dia (InvRelSymbol _) _)       = True+isInvRel (Neg (Box (InvRelSymbol _) _)) = True+isInvRel (Neg (Dia (InvRelSymbol _) _)) = True+isInvRel f                              = error $ "error isInvRel: " ++ show f++-- Function for converting a literal (a propositional atom or a negation+-- of a propositional atom) at a nominal n to a pair consisting of the+-- n and the name of the atom.++nf2np :: NomSymbol -> Form -> (NomSymbol,PropSymbol)+nf2np nom (Prop name)       = (nom,name)+nf2np nom (Neg (Prop name)) = (nom,name)+nf2np _ _                   = error "error nf2np"++-- Function for converting a nominal m or negated nominal !m, at a +-- nominal n, to the pair (n,m). ++nf2nn :: NomSymbol -> Form -> (NomSymbol,NomSymbol)+nf2nn n (Nom m)       = (n,m)+nf2nn n (Neg (Nom m)) = (n,m) +nf2nn _ _             = error "error nf2nn"++-- Function for getting the nominal out of a nominal formula, a negated +-- nominal formula, or an access formula ++getNom :: Form -> NomSymbol +getNom (Nom nom)                      = nom+getNom (Neg (Nom nom))                = nom+getNom (Dia _ (Nom nom))              = nom+getNom (Neg (Box _ (Neg (Nom nom))))  = nom+getNom _                              = error "error getNom"++-- Function for getting the relation and the target nominal out of a +-- box or diamond formula: ++getRel :: Form -> Rel+getRel (Neg f)                           = getRel f+getRel (Dia (RelSymbol rel) _)           = rel+getRel (Dia (InvRelSymbol rel) _)        = rel+getRel (Box (RelSymbol rel) _)           = rel+getRel (Box (InvRelSymbol rel) _)        = rel+getRel _                  = error "error getRel"++-- The components of a (non-literal) formula are given by: ++components :: Form -> [Form]+components (Conj fs)          = fs+components (Disj fs)          = fs +components (Impl f1 f2)       = [Neg f1,f2]+components (Neg (Conj fs))    = map Neg fs +components (Neg (Disj fs))    = map Neg fs +components (Neg (Impl f1 f2)) = [f1,Neg f2]+components (Neg (Neg f))      = [f]+components (A f)              = [f]+components (Neg (A f))        = [Neg f]+components (E f)              = [f]+components (Neg (E f))        = [Neg f]+components (Box _ f)          = [f]+components (Neg (Box _ f))    = [Neg f]+components (Dia _ f)          = [f]+components (Neg (Dia _ f))    = [Neg f]+components (Down _ f)         = [f]+components (Neg (Down _ f))   = [Neg f]+components (At _ f)           = [f] +components (Neg (At _ f))     = [Neg f]+components _                  = error "error components"++-- Located components of a (non-literal) formula: ++lcomponents :: NomSymbol -> Form -> [Form]+lcomponents nom f = [At nom f' | f' <- components f ]++-- For label formulas, the following function returns the label: ++getLabel :: Form -> NomSymbol+getLabel (At nom _)       = nom+getLabel (Neg (At nom _)) = nom+getLabel _                = error "error getLabel"++-- For binder formulas, the following function returns the binder: ++binder :: Form -> Int +binder (Down (X x) _)       = x+binder (Neg (Down (X x) _)) = x+binder _                    = error "error binder"++-- Check a list of formulas for nominal contradiction. ++checkNom :: [Form] -> Bool+checkNom fs = null [ m | (At n (Neg (Nom m))) <- fs, m == n ]++-- Checking a node for closure, with closure indicated by return of [] ++check :: Node -> [Node]+check node =+  if checkNN (neqs node)+     && checkPN (pos node) (neg node)+     && checkNom (forms node)+  then [node] else []+  where checkNN           = all (\(m,n) -> m /= n)     +        checkPN poss negs = intersect poss negs == []++-- Sometimes we just have to check the final component of a node: ++checkNdNom :: Node -> [Node]+checkNdNom node = if checkNom (forms node) then [node] else []+++{- Tableau Expansion -}++step :: Node -> Tableau++-- Applying an expansion step to a node N yields a tableau, i.e., a list +-- of nodes. If the expansion step results in closure of N, we return +-- []. Otherwise we return a non-empty list of open tableau nodes. ++-- If the function is called for a node N with an empty pending formula+-- list, there is nothing left to do, so we return [N].++step node | null (forms node) = check node++-- If the list of pending formulas starts with a Boolean constant, then +-- remove it if it is the constant True, otherwise close the node: ++step node +  | isTrue  f = [node{forms=fs}]+  | isFalse f = []++-- The list of pending formulas starts with a propositional literal:+-- check for closure; if the node does not close, then add the literal to+-- the appropriate list.++  | isPlit f = let +                 ni   = nf2np nom f +                 pos' = add ni (pos node)+               in +    if ni `elem` neg node then [] +    else [node{forms=fs, pos=pos'}]++  | isNlit  f = let +                 ni   = nf2np nom f  +                 neg' = add ni (neg node)+                in +    if ni `elem` pos node then [] +    else [node{forms=fs, neg=neg'}]++-- The list of pending formulas starts with a nominal. In this case we+-- perform a substitution and check for closure. Note the following: ++-- * Applying a substitution to a list of access relations may result+--  in a _change_ in the access relations, and thus in a violation of +--  a universal constraint, thus destroying the invariant that the universal+--  constraints hold for all nominals present at the node. To restore +-- that invariant, we have to take care that the universal constraints +-- get (re-)applied to the new nominal that fuses two old ones. ++-- * Applying a+-- substitution to a list of access relations may result in new access+-- relations, thus destroying the invariant that the box and converse box+-- constraints of the node have been applied for all access relations of+-- the node. To restore that invariant, we have to take care that all box+-- and converse box constraints get applied to the new access relations.++-- * Applying a substitution to a list of box constraints may result +-- in new box constraints, thus destroying the invariant that the box+-- constraints of the node have been applied for all access relations of+-- the node. To restore that invariant, we have to apply all new box+-- constraints to all access relations of the node.++-- * Applying a substitution to a list of converse box constraints may result +-- in new converse box constraints, thus destroying the invariant that+-- the converse box constraints of the node have been applied for all+-- access relations of the node. To restore that invariant, we have to+-- apply all new converse box constraints to all access relations of the+-- node.++  | isNom f =+    if getNom f == nom+     then [node{forms=fs}]+     else +          let +            k_        = getNom f +            m         = min k_ nom+            n         = max k_ nom+            dom'      = nub $ appDomain (n,m) (dom node)+            neqs'     = nub $ appNNs (n,m) (neqs node)+            accs'     = nub $ appNRNs (n,m) (accs node)+            ufs'      = nub $ appFs (n,m) (ufs node)+            boxes'    = nub $ appNRFs (n,m) (boxes node)+            newboxes  = boxes' \\ boxes node+            cboxes'   = nub $ appNRFs (n,m) (cboxes node)+            newcboxes = cboxes' \\ cboxes node+            pos'      = nub $ appNPs (n,m) (pos node)+            neg'      = nub $ appNPs (n,m) (neg node)+            forms'    = nub $ appFs  (n,m) (forms node)+            newaccs   = accs' \\ accs node+            us        = [ At m g | g <- ufs'          ]+            bs1       = [ At l g | (k,r,l)   <- newaccs, +                                   (k',r',g) <- boxes',+                                   k == k', r == r'   ]+            bs2       = [ At l g | (k,r,l)   <- accs',+                                   (k',r',g) <- newboxes,+                                   k == k', r == r'   ]+            cs1       = [ At k g | (k,r,l)   <- newaccs, +                                   (l',r',g) <- cboxes',+                                    l == l', r == r'   ]+            cs2       = [ At k g | (k,r,l)   <- accs', +                                   (l',r',g) <- newcboxes,+                                    l == l', r == r'   ]+            newforms  = nub $ forms' ++ us ++ bs1 ++ bs2 ++ cs1 ++ cs2+         in+     check node{dom = dom',+                neqs = neqs',+                accs = accs',+                ufs = ufs',+                boxes = boxes',+                cboxes = cboxes',+                pos = pos',+                neg = neg',+                forms = newforms}++-- The list of pending formulas starts with a negated nominal: check for+-- closure. If the node does not close, add a new inequality (m != n)+-- to the inequality list of the node.++  | isNgNom f =+      if getNom f == nom+       then []+       else +          let +            k = getNom f+            m = min k nom+            n = max k nom+            neqs' = add (m,n) (neqs node)+          in+         [node{neqs = neqs', forms = fs}]++-- The list of pending formulas starts with an access formula++  | isAcc f && not (isInvRel f)+      =+          let +            (r,n) = (getRel f, getNom f)+            accs' = add (nom,r,n) (accs node)+            dom'  = add n (dom node)+            fs'   = if (nom,r,n) `elem` accs node -- check is the access relation is already in the node+                     then fs +                     else nub $ fs ++ us ++ bs ++ cs+            us    = [ At n g   | g <- ufs node           ] -- add universal constraints +            bs    = [ At n g   | (m,s,g) <- boxes node,+                                  m == nom, s == r       ] -- add box constaints+            cs    = [ At nom g | (m,s,g) <- cboxes node,+                                  m == n, s == r         ] -- add inverse box constraints+          in +    checkNdNom node{dom = dom',+                    accs = accs',+                    forms = fs'+                   }++  | isAcc f && isInvRel f+      =+           let +             (r,n) = (getRel f, getNom f)+             accs' = add (n,r,nom) (accs node)+             dom'  = add n (dom node)+             fs'   = if (n,r,nom) `elem` accs node+                      then fs+                      else nub $ fs ++ us ++ bs ++ cs+             us    = [ At n g     | g <- ufs node            ]+             bs    = [ At nom g   | (m,s,g) <- boxes node,+                                     m == n, s == r          ]+             cs    = [ At n g     | (m,s,g) <- cboxes node,+                                     m == nom, s == r        ]+           in +    checkNdNom node{dom = dom',+                    accs = accs',+                    forms = fs'+                   }++-- The list of pending formulas starts with a double negation: apply the +-- double negation rule. ++  | isDneg  f +            =  let +                [g] = lcomponents nom f+                fs' = add g fs+               in+              [node{forms=fs'}]++-- The list of pending formulas starts with an alpha formula: +-- add the components alpha_i to the node. ++  | isAlpha f = +              let +                fs' = nub $ lcomponents nom f ++ fs+              in +    [node{forms=fs'}]+   +-- The list of pending formulas starts with a beta formula: +-- split the node and add a component beta_i to each new branch. ++  | isBeta  f = [ node{forms=(f':fs)} | f' <- lcomponents nom f ]++-- The list of pending formulas starts with an A formula (@ k phi).+-- Add { @ m phi' | m in D } where D is +-- the domain of the node, to the list of pending formulas, and store +-- phi' as a universal constraint. ++  | isA   f = let +                newfs  = [ At n g | n <- dom node,+                                    g <- components f ]+                fs'    = nub $ fs ++ newfs+                [f']   = components f+                ufs'   = nub (f':ufs node)+              in+    checkNdNom node{ufs = ufs',+                    forms = fs'}++-- The list of pending formulas starts with an E formula (@ k phi).+-- Take a fresh nominal n, add it to the domain of the node, +-- add (@ n phi') and { @ n psi | psi in U } to the list +-- of pending formulas.++  | isE   f = let +                n      = N (idx node)+                dom'   = add n (dom node)+                ls     = lcomponents n f+                us     = [ At n g | g <- ufs node ]+                fs'    = nub $ fs ++ ls ++ us+              in+    [node{idx=(succ $ idx node), dom=dom', forms=fs'}]++-- The list of pending formulas starts with a [i] formula (@k phi).+-- Add the list [@ m phi' | k<i>m in A ], +-- where A is the list of access formulas of the node, to the list of+-- pending formulas, and store the [i] formula as a box+-- constraint. Actually, for convenience, we store (k,i,phi').++  | isBox   f  && not (isInvRel f)+        = let+                r      = getRel f+                newfs  = [ At n g | (m,s,n) <- accs node,+                                     g      <- components f,+                                     m == nom, s == r           ]+                fs'    = nub $ fs ++ newfs+                boxes' = nub $+                          [(nom,r,g) | g <- components f] ++ boxes node+              in+    checkNdNom node{boxes=boxes',forms=fs'}++-- The list of pending formulas starts with a [-i] formula +-- (@k phi). Add the list [@ m phi' | m<i>k in A]+-- where A is the list of access formulas of the node, to the list of+-- pending formulas, and store the [-i] formula as a converse box+-- constraint.  Actually, for convenience we store (k,i,phi').++  | isBox  f && isInvRel f+      = let+                r       = getRel f+                newfs   = [ At n g | (n,s,m) <- accs node,+                                      g      <- components f, +                                      m == nom, s == r           ]+                fs'     = nub $ fs ++ newfs+                cboxes' = nub $+                           [(nom,r,g) | g <- components f] ++ cboxes node+              in+    checkNdNom node{cboxes=cboxes', forms=fs'}++-- The list of pending formulas starts with a diamond formula: use the+-- node index i to generate a fresh nominal constant n_i, increment+-- the node index, add (k<j>n_i) to the access list of the node, and put+-- (@ n_i phi'), where phi' is the component of the diamond+-- formula, on the list of pending formulas.  Also, generate appropriate+-- formulas for n_i from the universal constraints and from the +-- box constraints on k, and append them to the list of pending formulas.++  | isDiamond f && not (isInvRel f)+      =+             let +               n     = N (idx node)+               idx'  = succ $ idx node+               r     = getRel f+               accs' = (nom,r,n):(accs node)+               dom'  = add n (dom node)+               ls    = lcomponents n f+               us    = [ At n g   | g <- ufs node  ]+               bs    = [ At n g | (m,s,g) <- boxes node,+                                   m == nom, s == r  ]+               fs'   = nub $ fs ++ ls ++ us ++ bs+             in+    [node{idx=idx', dom=dom', accs=accs', forms=fs'}]++-- The list of pending formulas starts with a inverse diamond+-- formula: use the node index i to generate a fresh nominal constant+-- n_i, increment the node index, add (n_i<j>k) to the access list of+-- the node, generate the appropriate formulas for n_i from the converse+-- box constraints of the node, and append them, together with the+-- component of the <-> formula, to the list of pending formulas.++  | isDiamond f && isInvRel f+      =+             let +               n      = N (idx node)+               idx'   = succ $ idx node+               r      = getRel f+               accs'  = (n,r,nom):(accs node)+               dom'   = add n (dom node)+               ls     = lcomponents n f+               us     = [ At n g | g <- ufs node     ]+               cs     = [ At n g | (m,s,g) <- cboxes node,+                                    m == nom, s == r  ]+               fs'    = nub $ fs ++ ls ++ us ++ cs+              in+    [node{idx = idx', dom=dom', accs=accs', forms=fs'}]++-- The list of pending formulas starts with an @ formula (@k @n phi)+-- (or (@ k - @ n phi)): add (@ n phi) (or (@ n - phi)) to the+-- list of pending formulas.++  | isLabel f+            = let +                fs'  = add f' fs+                n    = getLabel f+                [f'] = lcomponents n f+              in+    [node{forms=fs'}] ++-- The list of pending formulas starts with a down-arrow formula: add+-- its component to the list of pending formulas, after the appropriate+-- substitution.++  | isDown  f+            = let +                x   = binder f+                [g] = components f+                f'  = At nom (appF (X x,nom) g)+                fs' = add f' fs +              in +    [node{forms=fs'}]+ where (At nom f:fs) = forms node++step nd = error $ "error step: " ++ show nd+  +-- These are all the possible cases, so this ends the treatment of +-- a single tableau expansion step. ++-- A tableau node is fully expanded (complete) if its list of pending+-- formulas is empty.++complete :: Node -> Bool +complete node | null $ forms node = True+complete  _                       = False++-- In general, we are not interested in generating all models for +-- a satisfiable formula: one model is enough. This allows for +-- a considerable reduction.++data OpenFlag = OPEN [Node] | CLOSED++expand :: Bool -> Tableau -> IO OpenFlag+expand verbose []   = do when verbose $ putStrLn "Closed"+                         return CLOSED+expand verbose (node:nodes) =+ do when verbose $ putStrLn (show node)+    if complete node+     then return $ OPEN [node]+     else do let newnodes = step node+             expand verbose (nodes ++ newnodes)++{- Cautious Tableau Expansion -}++-- Tableau expansion according to the `trial and error' versions of the+-- E, Diamond and Cdia rules is useful for finding minimal+-- models. In cautious tableau expansion we reuse existing nominals, and+-- we should check carefully whether this disturbs our constraints+-- invariant. The following functions take care of this:++noAccTo, noAccFrom :: [(NomSymbol,Rel,NomSymbol)] -> NomSymbol -> Rel -> Bool+noAccTo   accs_ m r = null [ (k,r,m) | (k,r',m') <- accs_, r==r', m==m' ]+noAccFrom accs_ m r = null [ (m,r,k) | (m',r',k) <- accs_, r==r', m==m' ]++-- Thus, if (noAccTo accs m r) is true at a node, where accs+-- is the list of access arrows of the node, this means that there +-- is no arrow (x <r> m) at the+-- node. This means in turn that adding a new r arrow that+-- points to m may disturb the box constraint invariant. Similarly, +-- truth of (noAccFrom accs m r) at a node, accs+-- is the list of access arrows of the node, indicates that the addition +-- of a new r-relation arrow that departs from m may violate +-- the converse box constraint invariant of the node. +-- +-- We are ready now to replace the step function by the following+-- alternative:++cautiousStep :: Node -> Tableau++-- Cautious step are like ordinary steps, except for the cases where+-- the formula to be decomposed is a E, Diamond and Cdia formula.+-- +-- If the function is called for a node  N with an empty pending formula+-- list, again, there is nothing left to do, and we return [N].+ +cautiousStep node+  | null $ forms node = [node]++-- If the list of pending formulas starts with an E formula, we branch+-- to all the possible ways of letting the existential obligation be+-- fulfilled by an existing nominal, and append the result of doing the+-- extension step that introduces a fresh nominal. Note that no accessibilities +-- are added, so no box or converse box constraints can be violated. Also, +-- no nominals are added, so no universal constraints can be violated. +  | isE   f = +    [ node{forms = nub (lcomponents n f ++ fs)} | n <- dom node]+    ++ step node++-- If the list of pending formulas starts with a Diamond or Cdia formula, +-- we branch to all the ways of letting an existing nominal discharge+-- the existential obligation, and append the result of the+-- expansion step that introduces a fresh nominal. Now we have to +-- take measures to ensure that the invariant for the box constraints +-- gets restored, if necessary. ++  | isDiamond f && not (isInvRel f)+     =+    let r = getRel f in +    [ node{accs = add (nom,r,n) (accs node),+           forms= nub (lcomponents n f ++ fs ++ [ At n g | (m,s,g) <- boxes node,  m == nom, s == r,  noAccTo (accs node) n r ])+          }     | n <- dom node ]+     ++ step node++  | isDiamond f && isInvRel f+     =+    let r = getRel f in +    [ node{accs = add (n,r,nom) (accs node),+           forms= nub (lcomponents n f ++ fs ++ [ At n g | (m,s,g) <- cboxes node, m == nom, s == r,noAccFrom (accs node) n r ])+          }     | n  <- dom node]+     ++ step node++  | otherwise = step node+ where (At nom f:fs) = forms node+++-- Cautious expansion of a tableau:+cautiousExpand :: Bool -> Tableau -> IO OpenFlag+cautiousExpand verbose []   = do when verbose $ putStrLn "Closed"+                                 return CLOSED+cautiousExpand verbose (node:nodes) =+ do when verbose $ putStrLn (show node)+    if complete node+     then return $ OPEN [node]+     else do let newnodes = cautiousStep node+             cautiousExpand verbose (nodes ++ newnodes)++{- Model Generation -}++extract :: Node -> String +extract node =+ unwords $+  show (reverse (dom node)) +   :  [ show n ++ show i ++ show m | (n,i,m) <- reverse (accs node)]+   ++ [ show i ++ ":"    ++ show p | (i,p)   <- reverse (pos node) ]+   ++ [ show i ++ ":-"   ++ show p | (i,p)   <- reverse (neg node) ]++{- Frame Properties -}++-- Here is a list of pure formulas (formulas without proposition letters) +-- that define frame properties. In fact, any pure formula defines +-- a frame condition, and characterizes a class of frames. ++trans, k4, intrans, refl, kt, irrefl, symm     :: Form+kb, asymm, s4, kt4, s5, serial, kd, euclid, k5 :: Form+kdb, kd4, kd5, k45, kd45, kb4, ktb, antisymm   :: Form+trans     = parse "begin down x1 . [][]<->x1 end"+k4        = trans+intrans   = parse "begin down x1 . [][][-]-x1 end"+refl      = parse "begin down x1 . <>x1 end"+kt        = refl+irrefl    = parse "begin down x1 . []-x1 end"+symm      = parse "begin down x1 . []<>x1 end"+kb        = symm+asymm     = parse "begin down x1 . [][]-x1 end"+s4        = parse "begin down x1 . (<>x1 & [][] <->x1) end"+kt4       = s4+s5        = parse "begin down x1 . ((<>x1) & ([]<>x1) & ([][]<->x1)) end"+serial    = parse "begin <>true end"+kd        = serial+euclid    = parse "begin down x1 . [] down x2 . @ x1 []<>x2 end"+k5        = euclid +kdb       = parse "begin (<>true & down x1 . []<->x1) end"+kd4       = parse "begin (<>true & down x1 . [][]<->x1) end"+kd5       = parse "begin (<>true & down x1 . [] down x2 . @ x1 []<>x2) end"+k45       = parse "begin down x1 . x1([][]<->1 & [] down x2 . @ x1 []<>x2) end"+kd45      = parse "begin down x1 . ((<>true) & ([][]<->x1) & ([] down x2 . @ x1 []<>x2)) end"+kb4       = parse "begin down x1 . ([]<>x1 & [][] <->x1) end"+ktb       = parse "begin down x1 . (<>x1 & []<>x1) end"+antisymm  = parse "begin down x1 . [] down x2 . [] (x1 -> x2) end"++add :: (Eq a) => a -> [a] -> [a]+add x xs = if x `elem` xs then xs else x:xs
+ src/Main.hs view
@@ -0,0 +1,216 @@+module Main++where ++import Form ( Form, parse )+import Hylotab++import System.IO           ( hPrint, stderr, hSetBuffering, stdin, BufferMode(LineBuffering)) +import System.Exit         ( exitWith, ExitCode(ExitFailure) )++import System.Console.GetOpt ( OptDescr(..), ArgDescr(..), ArgOrder(..),+                               getOpt, usageInfo )+import System.Environment    ( getArgs, getProgName )+import System.CPUTime( getCPUTime )+import System.Timeout ( timeout )++import Control.Monad.Error (MonadError(..))+import Control.Applicative ( (<$>) )+import Prelude hiding ( catch, log )+import Control.Exception   ( catch, SomeException )+import Control.Monad(unless)++main :: IO ()+main = do r <- runCmdLineVersion+                `catch` \e -> do+                    let msg = show (e::SomeException)+                    unless (msg == "ExitSuccess") $ hPrint stderr msg+                    exit r_RUNTIME_ERROR+          --+          case r of+            Nothing             -> exit r_DID_NOT_RUN+            Just Nothing        -> exit r_TIMEOUT+            Just (Just UNSAT)   -> exit r_UNSAT+            Just (Just (SAT _)) -> exit r_SAT+    --+    where r_SAT           = 1+          r_UNSAT         = 2+          r_TIMEOUT       = 3+          r_DID_NOT_RUN   = 10+          r_RUNTIME_ERROR = 13++exit :: Int -> IO a+exit = exitWith . ExitFailure++runCmdLineVersion :: IO (Maybe (Maybe SatFlag))+runCmdLineVersion =+    do p_clp <- getParams+       case p_clp of+         Left  err -> do putStrLn header+                         putStrLn err+                         progName <- getProgName+                         putStrLn $ "Try `" ++ progName ++ " --help' " +++                                     "for more information"+                         return Nothing+         --+         Right clp -> if showhelp clp+                        then do putStrLn header+                                progName <- getProgName+                                putStrLn $ usage (progName ++ " [OPTIONS]")+                                putStrLn gplTag+                                return Nothing+                        --+                        else Just <$> runWithParams clp++runWithParams :: Params -> IO (Maybe SatFlag)+runWithParams par =+ do  start <- getCPUTime+     --+     let myPutStrLn = if quietmode par then const (return ()) else putStrLn+     --+     let fromStdIn = do myPutStrLn $ "Reading from stdin (run again with" +++                                     "`--help' for usage options)"+                        hSetBuffering stdin LineBuffering+                        getContents++     f <- parse <$> maybe fromStdIn readFile (filename par)+     --+     f `seq` myPutStrLn $ "\nInput:\n{ " ++ show f ++" }\nEnd of input\n"+     --+     let fcs = frameconds par+     let md = expandmode par+     let verbose = log par+     --+     unless (null fcs) $ myPutStrLn $ "\nAxioms:\n{ " ++ show fcs ++ " }\n"+     --+     result <- if maxtimeout par == 0+                then Just <$> genSat verbose md fcs f+                else timeout (maxtimeout par * (10::Int)^(6::Int))+                             (genSat verbose md fcs f)+     --+     case result of+        Nothing           ->  myPutStrLn "TIMEOUT"+        Just UNSAT        ->  myPutStrLn "not satisfiable"+        Just (SAT nodes)  ->  myPutStrLn $ "satisfiable:\n" ++ extract (head nodes)+     -- +     end <- getCPUTime+     let elapsedTime = fromInteger (end - start) / 1000000000000.0+     myPutStrLn $ "Elapsed time: " ++ show (elapsedTime :: Double)+     --+     return result++{- Command line parameters handling -}++data Params = Params { expandmode :: Mode,+                       maxtimeout :: Int,+                         showhelp :: Bool,+                        quietmode :: Bool,+                       frameconds :: [Form],+                         filename :: Maybe FilePath,+                              log :: Bool}++defaultParams :: Params+defaultParams = Params { expandmode = Extend,+                         maxtimeout = 0,+                           showhelp = False,+                         frameconds = [],+                           filename = Nothing,+                          quietmode = False,+                                log = False }++type ParamsModifier   = Params -> Either ParsingErrMsg Params+type ParsingErrMsg = String++parseCmds :: [String] -> Params -> Either ParsingErrMsg Params+parseCmds argv par = case getOpt RequireOrder options argv of+                       (clpMods, [],  []) -> thread clpMods par+                       (      _,unk,  []) -> fail $ "Unknown option: " +++                                                   unwords unk+                       (     _,   _,errs) -> fail $ unlines errs+++thread :: Monad m => [a -> m a] -> a -> m a+thread = foldr (\f g -> \a -> f a >>= g) return++options :: [OptDescr ParamsModifier]+options =+  [Option ['h','?']+          ["help"]+          (NoArg $ \p -> return p{showhelp = True})+          "display this help and exit",+   Option ['f']+          ["input-file"]+          (ReqArg ((not . null) ?-> \s p -> return p{filename = Just s}) "file")+          "obtain input formulas from file instead of stdin",+   Option ['t']+          ["timeout"]+          (ReqArg ((not . null) ?-> \s p -> return p{maxtimeout = read s}) "T")+          "run for at most T seconds",+   Option ['q']+          ["quiet", "silent"]+          (NoArg $ \p -> return p{quietmode = True})+          "suppress all normal output",+   Option []+          ["min"]+          (NoArg $ \p -> return p{expandmode = Try})+          "search minimal model",+   Option ['v']+          ["verbose"]+          (NoArg $ \p -> return p{log = True})+          "log tableau calculus"+  ] ++  +  map genAxiomOptions+             [(["trans","k4"], trans, "transitivity (k4) axiom"),+              (["intrans"], intrans, "intransitivity axiom"),+              (["refl","kt"],refl, "reflexivity axiom"),+              (["irrefl"], irrefl, "irreflexivity axiom"),+              (["symm","kb"], symm, "symmetry axiom"),+              (["asymm"], asymm,  "asymmetry axiom"),+              (["s4","kt4"], s4, "s4 axiom"),+              (["s5"], s5, "s5 axiom"),+              (["serial","kd"], serial, "serial (kd) axiom"),+              (["euclid","k5"], euclid, "euclid (k5) axiom"),+              (["kdb"], kdb, "kdb axiom"),+              (["kd4"], kd4, "kd4 axiom"),+              (["kd5"], kd5, "kd5 axiom"),+              (["k45"], k45, "k45 axiom"),+              (["kd45"], kd45, "kd45 axiom"),+              (["kb4"], kb4, "kb4 axiom"),+              (["ktb"], ktb, "ktb axiom"),+              (["antisymm"], antisymm, "antisymmetry axiom")]++genAxiomOptions :: ([String],Form,String) -> OptDescr ParamsModifier+genAxiomOptions (flags, form, description)+  = Option []+           flags+           (NoArg $ \p -> return p{frameconds = form:frameconds p})+           description++(?->) :: (String -> Bool) -> (String -> ParamsModifier) -> String -> ParamsModifier+p ?-> m = \s -> if not (null s) && p s+                  then m s+                  else \_ -> throwError ("Invalid argument: '" ++ s ++ "'")++getParams :: IO (Either ParsingErrMsg Params)+getParams =+    do cmdline_args <- getArgs+       return $ parseCmds cmdline_args defaultParams++usage :: String -> String+usage hdr = usageInfo hdr options++showInfo :: IO ()+showInfo = putStrLn ("HyLoTab 1.2.0: no input file.\n" +++		     "Usage: `--help' option gives basic information.\n")++header :: String+header = unlines ["Hylotab 1.2.0",+                  "J. van Eijck, G. Hoffmann. (c) 2002-2010."]++gplTag :: String+gplTag = unlines [+    "This program is distributed in the hope that it will be useful,",+    "but WITHOUT ANY WARRANTY; without even the implied warranty of",+    "MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the",+    "GNU General Public License for more details."]+