Logic_THF.hs revision 51ba9f663d9287750036b875cb278d7cdf9db91f
57dc8a87418e235e3d0621fb90728054044a9ef9Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
57dc8a87418e235e3d0621fb90728054044a9ef9Christian MaederModule : $Header$
57dc8a87418e235e3d0621fb90728054044a9ef9Christian MaederDescription : Instance of class Logic for THF.
57dc8a87418e235e3d0621fb90728054044a9ef9Christian MaederCopyright : (c) A. Tsogias, DFKI Bremen 2011
57dc8a87418e235e3d0621fb90728054044a9ef9Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
57dc8a87418e235e3d0621fb90728054044a9ef9Christian MaederMaintainer : Alexis.Tsogias@dfki.de
57dc8a87418e235e3d0621fb90728054044a9ef9Christian MaederStability : provisional
57dc8a87418e235e3d0621fb90728054044a9ef9Christian MaederPortability : non-portable (imports Logic)
89026e63176e6e40c7be1bbc542326f0d29d8108Christian MaederInstance of class Logic for THF.
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder-- TODO implement more instance methods
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maederdata THF = THF deriving Show
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maederinstance Language THF where
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder description _ =
89026e63176e6e40c7be1bbc542326f0d29d8108Christian Maeder "THF is a language for Higher Order Logic from the TPTP standard.\n" ++
89026e63176e6e40c7be1bbc542326f0d29d8108Christian Maeder "For further information please refer to" ++
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder "http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html"
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maederinstance Monoid BasicSpecTHF where
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder mempty = BasicSpecTHF BSTHF0 []
89026e63176e6e40c7be1bbc542326f0d29d8108Christian Maeder mappend (BasicSpecTHF t1 l1) (BasicSpecTHF t2 l2) =
89026e63176e6e40c7be1bbc542326f0d29d8108Christian Maeder BasicSpecTHF (max t1 t2) $ l1 ++ l2
89026e63176e6e40c7be1bbc542326f0d29d8108Christian Maederinstance Logic.Logic.Syntax THF BasicSpecTHF () () where
89026e63176e6e40c7be1bbc542326f0d29d8108Christian Maeder parse_basic_spec THF = Just (basicSpec BSTHF0)
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder -- remaining default implementations are fine!
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maederinstance Sentences THF SentenceTHF SignTHF MorphismTHF SymbolTHF where
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder map_sen THF _ = return
89026e63176e6e40c7be1bbc542326f0d29d8108Christian Maeder print_named THF = printNamedSentenceTHF
89026e63176e6e40c7be1bbc542326f0d29d8108Christian Maeder {- sym_name THF =
89026e63176e6e40c7be1bbc542326f0d29d8108Christian Maeder negation THF _ =
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder other default implementations are fine -}
89026e63176e6e40c7be1bbc542326f0d29d8108Christian Maederinstance StaticAnalysis THF BasicSpecTHF SentenceTHF () ()
89026e63176e6e40c7be1bbc542326f0d29d8108Christian Maeder SignTHF MorphismTHF SymbolTHF () where
79e28be65fd0bc65adf266d5ae4f6deb92546bf7Christian Maeder basic_analysis THF = Just basicAnalysis
89026e63176e6e40c7be1bbc542326f0d29d8108Christian Maeder empty_signature THF = emptySign
89026e63176e6e40c7be1bbc542326f0d29d8108Christian Maeder signature_union THF = sigUnion
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder signatureDiff THF = sigDiff
89026e63176e6e40c7be1bbc542326f0d29d8108Christian Maeder intersection THF = sigIntersect
89026e63176e6e40c7be1bbc542326f0d29d8108Christian Maeder -- is_subsig THF _ _ = True
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder{- In order to find the LeoII prover there must be an entry in the
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian MaederPATH environment variable leading to the leo executable
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder(The executable leo.opt is not supported. In this case there should be a link
57dc8a87418e235e3d0621fb90728054044a9ef9Christian Maedercalled leo, or something like that.) -}
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maederinstance Logic THF () BasicSpecTHF SentenceTHF () ()
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder SignTHF MorphismTHF SymbolTHF () ProofTree where
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder stability THF = Testing
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder provers THF = [] ++ unsafeProverCheck "leo" "PATH" leoIIProver
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder ++ unsafeProverCheck "isabelle" "PATH" isaProver
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder ++ unsafeProverCheck "isabelle" "PATH" nitpickProver
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder ++ unsafeProverCheck "isabelle" "PATH" refuteProver
5b55761e0df088c5b41183fb83106bfd02a61fa2Christian Maeder ++ unsafeProverCheck "isabelle" "PATH" sledgehammerProver