diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. + + + Copyright (C) + + 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. + + , 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. diff --git a/NF.tex b/NF.tex new file mode 100644 --- /dev/null +++ b/NF.tex @@ -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 + + diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,4 @@ +#! /usr/bin/env runhaskell + +> import Distribution.Simple +> main = defaultMain diff --git a/cthl.tex b/cthl.tex new file mode 100644 --- /dev/null +++ b/cthl.tex @@ -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} + diff --git a/examples/runsat.sh b/examples/runsat.sh new file mode 100644 --- /dev/null +++ b/examples/runsat.sh @@ -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 + + diff --git a/examples/rununsat.sh b/examples/rununsat.sh new file mode 100644 --- /dev/null +++ b/examples/rununsat.sh @@ -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 + + diff --git a/examples/sat/form04.frm b/examples/sat/form04.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form04.frm @@ -0,0 +1,3 @@ +begin + <>(n1 & (<>n1) & ([]<>n1)) +end diff --git a/examples/sat/form05.frm b/examples/sat/form05.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form05.frm @@ -0,0 +1,5 @@ +begin + down x1 . [][] <->x1 ; { transitivity } + [] down x1 . <> true ; { irreflexivity } + <>true { initial successor } +end diff --git a/examples/sat/form06.frm b/examples/sat/form06.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form06.frm @@ -0,0 +1,5 @@ +begin + ([R1](p1 v p3)) <--> ([R3](p3 -> -p3)); + [R2](p1 -> (p1 <--> (p3 v p4 v -p5))); + [R1][R2][R3](p1 v -p3 v -p5) +end diff --git a/examples/sat/form08.frm b/examples/sat/form08.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form08.frm @@ -0,0 +1,12 @@ +begin + +@ N1 ( (<>true) + & ([][]<->N1) + & ([] ( (<>true) + & (down x1 . []-x1) + & (down x1 . [][]-x1) + & (down x1 . [][]<->x1) + ) + ) + ) +end diff --git a/examples/sat/form09.frm b/examples/sat/form09.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form09.frm @@ -0,0 +1,13 @@ +begin + +@ N1 ( (<>true) + & (<><>true) + & ([][]<->N1) + & ([] ( (<>true) + & (down x1 . []-x1) + & (down x1 . [][]-x1) + & (down x1 . [][]<->x1) + ) + ) + ) +end diff --git a/examples/sat/form11.frm b/examples/sat/form11.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form11.frm @@ -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 diff --git a/examples/sat/form12.frm b/examples/sat/form12.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form12.frm @@ -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 diff --git a/examples/sat/form13.frm b/examples/sat/form13.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form13.frm @@ -0,0 +1,6 @@ +begin +<>p1 ; +<><>-p1; +<><><>p1; +[](p1 & [](-p1 & [](p1 & []-p1))) +end diff --git a/examples/sat/form14.frm b/examples/sat/form14.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form14.frm @@ -0,0 +1,7 @@ +begin +<>p1; +<><>-p1; +<><><>p1; +<><><><>-p1; +[](p1 & [](-p1 & [](p1 & [](-p1 & []p1)))) +end diff --git a/examples/sat/form15.frm b/examples/sat/form15.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form15.frm @@ -0,0 +1,9 @@ +begin +<>p1; +<><>-p1; +<><><>p1; +<><><><>-p1; +<><><><><>p1; +<><><><><><>-p1; +[](p1 & [](-p1 & [](p1 & [](-p1 & [](p1 & []-p1))))) +end diff --git a/examples/sat/form16.frm b/examples/sat/form16.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form16.frm @@ -0,0 +1,5 @@ +begin + ([R1](p1 v p3) <--> [R3](p3 -> -p3)); + [R2](p1 -> (p1 <--> (p3 v p4 v -p5))); + [R1][R2][R3] (p1 v -p3 v -p5) +end diff --git a/examples/sat/form17.frm b/examples/sat/form17.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form17.frm @@ -0,0 +1,9 @@ +begin + +(@ n1 p1) v (@ n2 p2) v (@ n3 p3) v (@ n4 p4); +[]-p1; +[]-p2; +[]-p3; +[]-p4 + +end diff --git a/examples/sat/form18.frm b/examples/sat/form18.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form18.frm @@ -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 diff --git a/examples/sat/form23.frm b/examples/sat/form23.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form23.frm @@ -0,0 +1,6 @@ +begin + (- <> @ n1 n2) +v (- @ n1 (<>p2 -> p1)) +v (- @ n2 <>p2) +v (@ n1 p1) +end diff --git a/examples/sat/form27.frm b/examples/sat/form27.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form27.frm @@ -0,0 +1,3 @@ +begin + (@ n2 (p2 v p1) -> @n1 p3) +end diff --git a/examples/sat/form28.frm b/examples/sat/form28.frm new file mode 100644 --- /dev/null +++ b/examples/sat/form28.frm @@ -0,0 +1,5 @@ +begin + + -(@ n2 (p1 v p2) -> @n1 p3) + +end diff --git a/examples/unsat/form01.frm b/examples/unsat/form01.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/form01.frm @@ -0,0 +1,5 @@ +begin +<> (n1 & p2); +<>(n1 & p1); +[] (-p2 v -p1) +end diff --git a/examples/unsat/form02.frm b/examples/unsat/form02.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/form02.frm @@ -0,0 +1,4 @@ +begin + (@ n1 <>[-]-n1) + v (@ n1 <->[]-n1) +end diff --git a/examples/unsat/form03.frm b/examples/unsat/form03.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/form03.frm @@ -0,0 +1,6 @@ +begin + <>p1; + <>-p1; + [](p1 -> n1); + []p1 +end diff --git a/examples/unsat/form07.frm b/examples/unsat/form07.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/form07.frm @@ -0,0 +1,5 @@ +begin + +down x1 . []<>x1 & -(<>[]p1 -> p1) + +end diff --git a/examples/unsat/form10.frm b/examples/unsat/form10.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/form10.frm @@ -0,0 +1,5 @@ +begin + down x1 . [][]<->x1; { transitive } + down x1 . [][]-x1; { asymmetric } + down x1 . <>x1 { reflexive } +end diff --git a/examples/unsat/form19.frm b/examples/unsat/form19.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/form19.frm @@ -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 diff --git a/examples/unsat/form20.frm b/examples/unsat/form20.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/form20.frm @@ -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 diff --git a/examples/unsat/form21.frm b/examples/unsat/form21.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/form21.frm @@ -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 diff --git a/examples/unsat/form22.frm b/examples/unsat/form22.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/form22.frm @@ -0,0 +1,6 @@ +begin +<>(@n1 n2); +@ n1 ([]p1 -> p2); +@ n2 []p1; +- @ n1 p2 +end diff --git a/examples/unsat/form24.frm b/examples/unsat/form24.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/form24.frm @@ -0,0 +1,9 @@ +begin + +- ( + (@ n1 (n2 & (@ n1 (p2 v @ n2 p1) -> p3))) + -> + (@ n2 (p2 v @ n2 p1) -> @n1 p3) + ) + +end diff --git a/examples/unsat/form25.frm b/examples/unsat/form25.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/form25.frm @@ -0,0 +1,8 @@ +begin + ( + (@ n1 n2 & @ n1 ((p2 v @ n2 p1) -> p3)) + & + - (@ n2 (p2 v @ n2 p1) -> @n1 p3) + ) + +end diff --git a/examples/unsat/form26.frm b/examples/unsat/form26.frm new file mode 100644 --- /dev/null +++ b/examples/unsat/form26.frm @@ -0,0 +1,6 @@ +begin +<>@ n1 n2; +@ n1 (p2 -> @n2 p1); +@n1 p2; +- @ n2 p1 +end diff --git a/hylotab.bib b/hylotab.bib new file mode 100644 --- /dev/null +++ b/hylotab.bib @@ -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 = {} +} diff --git a/hylotab.cabal b/hylotab.cabal new file mode 100644 --- /dev/null +++ b/hylotab.cabal @@ -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 diff --git a/src/Form.hs b/src/Form.hs new file mode 100644 --- /dev/null +++ b/src/Form.hs @@ -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 diff --git a/src/Hylotab.hs b/src/Hylotab.hs new file mode 100644 --- /dev/null +++ b/src/Hylotab.hs @@ -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 nm 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 (nm) 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 (mn) 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' | km 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' | mk 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 (kn_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_ik) 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 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 diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 --- /dev/null +++ b/src/Main.hs @@ -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."] +