hylotab 1.2.0 → 1.2.1
raw patch · 3 files changed
+23/−16 lines, 3 filesdep ~hylolibdep ~mtl
Dependency ranges changed: hylolib, mtl
Files
- hylotab.cabal +5/−6
- src/Form.hs +6/−0
- src/Hylotab.hs +12/−10
hylotab.cabal view
@@ -1,12 +1,11 @@ Name: hylotab-Version: 1.2.0+Version: 1.2.1 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.+ It is no longer developped, but it is kept compatible+ with the syntax used in HyLoLib. License: GPL License-file: LICENSE Author: Jan van Eijck, Guillaume Hoffmann@@ -30,8 +29,8 @@ Main-is: Main.hs Other-modules: Form Hylotab Build-Depends: base >= 4, base < 5,- mtl >= 1, mtl < 2,- hylolib >= 1.3, hylolib < 1.4+ mtl >= 2, mtl < 3,+ hylolib == 1.4.* hs-source-dirs: src ghc-options: -Wall ghc-prof-options: -auto-all
src/Form.hs view
@@ -23,6 +23,8 @@ | E Form | Box RelSymbol Form | Dia RelSymbol Form+ | IBox RelSymbol Form+ | IDia RelSymbol Form | At NomSymbol Form | Down NomSymbol Form deriving (Eq,Ord)@@ -42,6 +44,8 @@ show (E f) = 'E' : show f show (Box name f) = "[" ++ show name ++ "]" ++ show f show (Dia name f) = "<" ++ show name ++ ">" ++ show f+ show (IBox name f) = "[-" ++ show name ++ "]" ++ show f+ show (IDia name f) = "<-" ++ show name ++ ">" ++ show f show (At nom f) = show nom ++ ":" ++ show f show (Down i f) = "down " ++ show i ++ "." ++ show f @@ -64,6 +68,8 @@ 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.IDiam r f) = IDia r (conv_ f)+conv_ (F.IBox r f) = IBox 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)
src/Hylotab.hs view
@@ -163,6 +163,8 @@ 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 (IBox r f) = IBox r (appF b f)+appF b (IDia r f) = IDia 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) @@ -230,14 +232,14 @@ 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 (Box _ _) = False+isInvRel (Dia _ _) = False+isInvRel (Neg (Box _ _)) = False+isInvRel (Neg (Dia _ _)) = False+isInvRel (IBox _ _) = True+isInvRel (IDia _ _) = True+isInvRel (Neg (IBox _ _)) = True+isInvRel (Neg (IDia _ _)) = True isInvRel f = error $ "error isInvRel: " ++ show f -- Function for converting a literal (a propositional atom or a negation@@ -273,9 +275,9 @@ getRel :: Form -> Rel getRel (Neg f) = getRel f getRel (Dia (RelSymbol rel) _) = rel-getRel (Dia (InvRelSymbol rel) _) = rel+getRel (IDia (RelSymbol rel) _) = rel getRel (Box (RelSymbol rel) _) = rel-getRel (Box (InvRelSymbol rel) _) = rel+getRel (IBox (RelSymbol rel) _) = rel getRel _ = error "error getRel" -- The components of a (non-literal) formula are given by: