Logic_SoftFOL.hs revision a7be28e157e9ceeec73a8fd0e642c36ea29d4218
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{-# OPTIONS -cpp #-}
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblett{- |
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettModule : $Header$
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyDescription : Instance of class Logic for SoftFOL.
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyCopyright : (c) Rene Wagner, Klaus Luettich, Uni Bremen 2005-2007
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettMaintainer : luecke@informatik.uni-bremen.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : non-portable (imports Logic)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettInstance of class Logic for SoftFOL.
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-}
78718c37b1a50086a27e0f031db4cf82bea934aeChristian Maeder
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachmodule SoftFOL.Logic_SoftFOL where
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.DefaultMorphism
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.DocUtils
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.ProofTree
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettimport ATC.ProofTree ()
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettimport Logic.Logic
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport SoftFOL.ATC_SoftFOL ()
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport SoftFOL.Sign
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblettimport SoftFOL.Print
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport SoftFOL.Conversions
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport SoftFOL.Morphism
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maederimport Common.ProverTools
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach#ifdef UNI_PACKAGE
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maederimport SoftFOL.ProveSPASS
0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblett#ifndef NOMATHSERVER
04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblettimport SoftFOL.ProveMathServ
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettimport SoftFOL.ProveVampire
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly#endif
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblettimport SoftFOL.ProveDarwin
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett#endif
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder
842ae753ab848a8508c4832ab64296b929167a97Christian Maederinstance Pretty Sign where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly pretty = pretty . signToSPLogicalPart
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder{- |
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder A dummy datatype for the LogicGraph and for identifying the right
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder instances
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-}
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblettdata SoftFOL = SoftFOL deriving (Show)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyinstance Language SoftFOL where
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly description _ =
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly "SoftFOL - Softly typed First Order Logic for "++
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly "Automated Theorem Proving Systems\n\n" ++
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett "This logic corresponds to the logic of SPASS, \n"++
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder "but the generation of TPTP is also possible.\n" ++
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "See http://spass.mpi-sb.mpg.de/\n"++
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly "and http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html"
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maederinstance Logic.Logic.Syntax SoftFOL () () ()
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder -- default implementation is fine!
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maederinstance Sentences SoftFOL Sentence Sign
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly SoftFOLMorphism SFSymbol where
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly map_sen SoftFOL _ s = return s
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sym_of SoftFOL = symOf
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sym_name SoftFOL = symbolToId
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly print_named SoftFOL = printFormula
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- other default implementations are fine
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maederinstance StaticAnalysis SoftFOL () Sentence
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder () ()
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder Sign
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder SoftFOLMorphism SFSymbol () where
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder empty_signature SoftFOL = emptySign
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett is_subsig SoftFOL _ _ = True
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett subsig_inclusion SoftFOL = defaultInclusion
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblettinstance Logic SoftFOL () () Sentence () ()
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett Sign
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett SoftFOLMorphism SFSymbol () ProofTree where
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett stability _ = Testing
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -- again default implementations are fine
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -- the prover uses HTk and IO functions from uni
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett#ifdef UNI_PACKAGE
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett provers SoftFOL = (unsafeProverCheck "SPASS" "PATH" spassProver)
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett#ifndef NOMATHSERVER
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett ++ [mathServBroker, vampire]
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett#endif
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ++ (unsafeProverCheck "darwin" "PATH" darwinProver)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly cons_checkers SoftFOL = (unsafeProverCheck "darwin" "PATH"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly darwinConsChecker)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly#endif
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett