{-# LANGUAGE CPP, MultiParamTypeClasses, TypeSynonymInstances
, FlexibleInstances #-}
module SoftFOL.Logic_SoftFOL where
import Data.Set (toList)
import Common.DefaultMorphism
import Common.DocUtils
import Common.ProofTree
import ATC.ProofTree ()
import Logic.Logic
import SoftFOL.ATC_SoftFOL ()
import SoftFOL.Sign
import SoftFOL.StatAna
import SoftFOL.Print
import SoftFOL.Conversions
import SoftFOL.Morphism
import SoftFOL.PrintTPTP ()
import SoftFOL.ProveSPASS
import SoftFOL.ProveHyperHyper
#ifndef NOHTTP
import SoftFOL.ProveMathServ
import SoftFOL.ProveVampire
#endif
import SoftFOL.ProveDarwin
import SoftFOL.ProveMetis
instance Pretty Sign where
pretty :: Sign -> Doc
pretty = SPLogicalPart -> Doc
forall a. Pretty a => a -> Doc
pretty (SPLogicalPart -> Doc) -> (Sign -> SPLogicalPart) -> Sign -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> SPLogicalPart
signToSPLogicalPart
data SoftFOL = SoftFOL deriving (Int -> SoftFOL -> ShowS
[SoftFOL] -> ShowS
SoftFOL -> String
(Int -> SoftFOL -> ShowS)
-> (SoftFOL -> String) -> ([SoftFOL] -> ShowS) -> Show SoftFOL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SoftFOL] -> ShowS
$cshowList :: [SoftFOL] -> ShowS
show :: SoftFOL -> String
$cshow :: SoftFOL -> String
showsPrec :: Int -> SoftFOL -> ShowS
$cshowsPrec :: Int -> SoftFOL -> ShowS
Show)
instance Language SoftFOL where
description :: SoftFOL -> String
description _ =
"SoftFOL - Softly typed First Order Logic for " String -> ShowS
forall a. [a] -> [a] -> [a]
++
"Automated Theorem Proving Systems\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
"This logic corresponds to the logic of SPASS, \n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
"but the generation of TPTP is also possible.\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
"See http://spass.mpi-sb.mpg.de/\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
"and http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html"
instance Logic.Logic.Syntax SoftFOL [TPTP] SFSymbol () ()
instance Sentences SoftFOL Sentence Sign
SoftFOLMorphism SFSymbol where
map_sen :: SoftFOL -> SoftFOLMorphism -> Sentence -> Result Sentence
map_sen SoftFOL _ = Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return
sym_of :: SoftFOL -> Sign -> [Set SFSymbol]
sym_of SoftFOL = Set SFSymbol -> [Set SFSymbol]
forall a. a -> [a]
singletonList (Set SFSymbol -> [Set SFSymbol])
-> (Sign -> Set SFSymbol) -> Sign -> [Set SFSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Set SFSymbol
symOf
symsOfSen :: SoftFOL -> Sign -> Sentence -> [SFSymbol]
symsOfSen SoftFOL sign :: Sign
sign = Set SFSymbol -> [SFSymbol]
forall a. Set a -> [a]
toList (Set SFSymbol -> [SFSymbol])
-> (Sentence -> Set SFSymbol) -> Sentence -> [SFSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sentence -> Set SFSymbol
symsOfTerm Sign
sign
sym_name :: SoftFOL -> SFSymbol -> Id
sym_name SoftFOL = SFSymbol -> Id
symbolToId
symKind :: SoftFOL -> SFSymbol -> String
symKind SoftFOL = SFSymbType -> String
sfSymbKind (SFSymbType -> String)
-> (SFSymbol -> SFSymbType) -> SFSymbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SFSymbol -> SFSymbType
sym_type
print_named :: SoftFOL -> Named Sentence -> Doc
print_named SoftFOL = Named Sentence -> Doc
printFormula
negation :: SoftFOL -> Sentence -> Maybe Sentence
negation _ = Sentence -> Maybe Sentence
negateSentence
instance StaticAnalysis SoftFOL [TPTP] Sentence
() ()
Sign
SoftFOLMorphism SFSymbol () where
empty_signature :: SoftFOL -> Sign
empty_signature SoftFOL = Sign
emptySign
is_subsig :: SoftFOL -> Sign -> Sign -> Bool
is_subsig SoftFOL _ _ = Bool
True
subsig_inclusion :: SoftFOL -> Sign -> Sign -> Result SoftFOLMorphism
subsig_inclusion SoftFOL = Sign -> Sign -> Result SoftFOLMorphism
forall (m :: * -> *) sign.
Monad m =>
sign -> sign -> m (DefaultMorphism sign)
defaultInclusion
basic_analysis :: SoftFOL
-> Maybe
(([TPTP], Sign, GlobalAnnos)
-> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence]))
basic_analysis SoftFOL = (([TPTP], Sign, GlobalAnnos)
-> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence]))
-> Maybe
(([TPTP], Sign, GlobalAnnos)
-> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence]))
forall a. a -> Maybe a
Just ([TPTP], Sign, GlobalAnnos)
-> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence])
basicAnalysis
instance Logic SoftFOL () [TPTP] Sentence () ()
Sign
SoftFOLMorphism SFSymbol () ProofTree where
stability :: SoftFOL -> Stability
stability _ = Stability
Stable
provers :: SoftFOL -> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
provers SoftFOL = [Prover Sign Sentence SoftFOLMorphism () ProofTree
spassProver]
#ifndef NOHTTP
[Prover Sign Sentence SoftFOLMorphism () ProofTree]
-> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
-> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
forall a. [a] -> [a] -> [a]
++ [Prover Sign Sentence SoftFOLMorphism () ProofTree
mathServBroker, Prover Sign Sentence SoftFOLMorphism () ProofTree
vampire]
#endif
[Prover Sign Sentence SoftFOLMorphism () ProofTree]
-> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
-> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
forall a. [a] -> [a] -> [a]
++ (ProverBinary -> Prover Sign Sentence SoftFOLMorphism () ProofTree)
-> [ProverBinary]
-> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
forall a b. (a -> b) -> [a] -> [b]
map ProverBinary -> Prover Sign Sentence SoftFOLMorphism () ProofTree
darwinProver [ProverBinary]
tptpProvers
[Prover Sign Sentence SoftFOLMorphism () ProofTree]
-> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
-> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
forall a. [a] -> [a] -> [a]
++ [Prover Sign Sentence SoftFOLMorphism () ProofTree
metisProver, Prover Sign Sentence SoftFOLMorphism () ProofTree
hyperProver]
cons_checkers :: SoftFOL -> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree]
cons_checkers SoftFOL = (ProverBinary
-> ConsChecker Sign Sentence () SoftFOLMorphism ProofTree)
-> [ProverBinary]
-> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree]
forall a b. (a -> b) -> [a] -> [b]
map ProverBinary
-> ConsChecker Sign Sentence () SoftFOLMorphism ProofTree
darwinConsChecker [ProverBinary]
tptpProvers
[ConsChecker Sign Sentence () SoftFOLMorphism ProofTree]
-> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree]
-> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree]
forall a. [a] -> [a] -> [a]
++ [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree
hyperConsChecker]