Logic_SoftFOL.hs revision a14767aeac3e78ed100f5b75e210ba563ee10dba
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{-# OPTIONS -cpp #-}
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederModule : $Header$
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederDescription : Instance of class Logic for SoftFOL.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Rene Wagner, Klaus Luettich, Uni Bremen 2005-2007
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : luecke@informatik.uni-bremen.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : non-portable (imports Logic)
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederInstance of class Logic for SoftFOL.
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder#ifdef UNI_PACKAGE
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder#ifndef NOMATHSERVER
8410667510a76409aca9bb24ff0eda0420088274Christian Maederinstance Pretty Sign where
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich pretty = pretty . signToSPLogicalPart
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder We use the DefaultMorphism for SPASS.
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maedertype SoftFOLMorphism = DefaultMorphism Sign
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder A dummy datatype for the LogicGraph and for identifying the right
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederdata SoftFOL = SoftFOL deriving (Show)
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maederinstance Language SoftFOL where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder description _ =
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder "SoftFOL - Softly typed First Order Logic for "++
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder "Automated Theorem Proving Systems\n\n" ++
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder "This logic corresponds to the logic of SPASS, \n"++
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder "but the generation of TPTP is also possible.\n" ++
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder "and http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html"
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maederinstance Logic.Logic.Syntax SoftFOL () () ()
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder -- default implementation is fine!
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maederinstance Sentences SoftFOL Sentence Sign
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder SoftFOLMorphism SFSymbol where
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder map_sen SoftFOL _ s = return s
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder sym_of SoftFOL = symOf
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder sym_name SoftFOL = symbolToId
2c9df69accd8924e7cef3bf8f686626958499c7aChristian Maeder print_named SoftFOL = printFormula
c2fcc35abb03cf0b4ca4b050efeb10827f38c322Christian Maeder -- other default implementations are fine
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maederinstance StaticAnalysis SoftFOL () Sentence
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder SoftFOLMorphism SFSymbol () where
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder empty_signature SoftFOL = emptySign
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder inclusion SoftFOL = defaultInclusion (const $ const True)
b9b331bded61b8860edacac91df16ee19e465b42Christian Maederinstance Logic SoftFOL () () Sentence () ()
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder SoftFOLMorphism SFSymbol () ProofTree where
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder stability _ = Testing
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich -- again default implementations are fine
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich -- the prover uses HTk and IO functions from uni
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich#ifdef UNI_PACKAGE
05a206508bc898f87fe6ab6e069814df3c29d303Dominik Luecke provers SoftFOL = [spassProver
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder#ifndef NOMATHSERVER
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder , mathServBroker,vampire
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder , darwinProver]
8a28707e9155465c6f2236a06eac6580a65c7025Christian Maeder cons_checkers SoftFOL = [darwinConsChecker]