Logic_SoftFOL.hs revision 2665d7759e63acff0bcd4135678f2cc6f2041d46
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder{-# LANGUAGE CPP #-}
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian MaederModule : $Header$
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederDescription : Instance of class Logic for SoftFOL.
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederCopyright : (c) Rene Wagner, Klaus Luettich, Uni Bremen 2005-2007
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederMaintainer : luecke@informatik.uni-bremen.de
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederStability : provisional
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : non-portable (imports Logic)
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederInstance of class Logic for SoftFOL.
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder#ifdef UNI_PACKAGE
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder#ifndef NOMATHSERVER
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maederinstance Pretty Sign where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder pretty = pretty . signToSPLogicalPart
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder A dummy datatype for the LogicGraph and for identifying the right
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederdata SoftFOL = SoftFOL deriving (Show)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Language SoftFOL where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder description _ =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "SoftFOL - Softly typed First Order Logic for "++
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "Automated Theorem Proving Systems\n\n" ++
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder "This logic corresponds to the logic of SPASS, \n"++
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder "but the generation of TPTP is also possible.\n" ++
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "and http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Logic.Logic.Syntax SoftFOL () () ()
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- default implementation is fine!
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Sentences SoftFOL Sentence Sign
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder SoftFOLMorphism SFSymbol where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder map_sen SoftFOL _ s = return s
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder sym_of SoftFOL = symOf
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder sym_name SoftFOL = symbolToId
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder print_named SoftFOL = printFormula
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- other default implementations are fine
a9e804dbec424ec36e34bab955cbe90edac5baa6Christian Maederinstance StaticAnalysis SoftFOL () Sentence
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder SoftFOLMorphism SFSymbol () where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder empty_signature SoftFOL = emptySign
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder is_subsig SoftFOL _ _ = True
fdac680252d7347858bd67b4c2a2aaa52e623815Christian Maeder subsig_inclusion SoftFOL = defaultInclusion
a9e804dbec424ec36e34bab955cbe90edac5baa6Christian Maederinstance Logic SoftFOL () () Sentence () ()
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich SoftFOLMorphism SFSymbol () ProofTree where
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich stability _ = Testing
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich -- again default implementations are fine
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich -- the prover uses HTk and IO functions from uni
2353f65833a3da763392f771223250cd50b8d873Christian Maeder#ifdef UNI_PACKAGE
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder provers SoftFOL = (unsafeProverCheck "SPASS" "PATH" spassProver)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder#ifndef NOMATHSERVER
2353f65833a3da763392f771223250cd50b8d873Christian Maeder ++ [mathServBroker, vampire]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ (unsafeProverCheck "darwin" "PATH" darwinProver)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder cons_checkers SoftFOL = (unsafeProverCheck "darwin" "PATH"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder darwinConsChecker)