{- |
Module      :  ./Common/SZSOntology.hs
Description :  The SZS ontology for TPTP prover results
Copyright   :  (c) Christian Maeder DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

see <http://www.cs.miami.edu/~tptp/> under Documents and SZSOntology
-}

module Common.SZSOntology where

import Data.Char

successes :: [(String, String)]
successes :: [(String, String)]
successes =
  [ ("Success", "SUC")
  -- The logical data has been processed successfully.

  , ("UnsatisfiabilityPreserving", "UNP")
  {- If there does not exist a model of Ax then there does not exist a model of
  C, i.e., if Ax is unsatisfiable then C is unsatisfiable. -}

  , ("SatisfiabilityPreserving", "SAP")
  {- If there exists a model of Ax then there exists a model of C, i.e., if Ax
  is satisfiable then C is satisfiable.
  - F is satisfiable. -}

  , ("EquiSatisfiable", "ESA")
  {- There exists a model of Ax iff there exists a model of C, i.e., Ax is
  (un)satisfiable iff C is (un)satisfiable. -}

  , ("Satisfiable", "SAT")
  {- Some interpretations are models of Ax, and
  some models of Ax are models of C.
  - F is satisfiable, and ~F is not valid.
  - Possible dataforms are Models of Ax | C. -}

  , ("FinitelySatisfiable", "FSA")
  {- Some finite interpretations are finite models of Ax, and
  some finite models of Ax are finite models of C.
  - F is satisfiable, and ~F is not valid.
  - Possible dataforms are FiniteModels of Ax | C. -}

  , ("Theorem", "THM")
  {- All models of Ax are models of C.
  - F is valid, and C is a theorem of Ax.
  - Possible dataforms are Proofs of C from Ax. -}

  , ("Equivalent", "EQV")
  {- Some interpretations are models of Ax,
  all models of Ax are models of C, and
  all models of C are models of Ax.
  - F is valid, C is a theorem of Ax, and Ax is a theorem of C.
  - Possible dataforms are Proofs of C from Ax and of Ax from C. -}

  , ("TautologousConclusion", "TAC")
  {- Some interpretations are models of Ax, and
  all interpretations are models of C.
  - F is valid, and C is a tautology.
  - Possible dataforms are Proofs of C. -}

  , ("WeakerConclusion", "WEC")
  {- Some interpretations are models of Ax,
  all models of Ax are models of C, and
  some models of C are not models of Ax.
  - See Theorem and Satisfiable. -}

  , ("EquivalentTheorem", "ETH")
  {- Some, but not all, interpretations are models of Ax,
  all models of Ax are models of C, and
  all models of C are models of Ax.
  - See Equivalent. -}

  , ("Tautology", "TAU")
  {- All interpretations are models of Ax, and
  all interpretations are models of C.
  - F is valid, ~F is unsatisfiable, and C is a tautology.
  - Possible dataforms are Proofs of Ax and of C. -}

  , ("WeakerTautologousConclusion", "WTC")
  {- Some, but not all, interpretations are models of Ax, and
  all interpretations are models of C.
  - F is valid, and C is a tautology.
  - See TautologousConclusion and WeakerConclusion. -}

  , ("WeakerTheorem", "WTH")
  {- Some interpretations are models of Ax,
  all models of Ax are models of C,
  some models of C are not models of Ax, and
  some interpretations are not models of C.
  - See Theorem and Satisfiable. -}

  , ("ContradictoryAxioms", "CAX")
  {- No interpretations are models of Ax.
  - F is valid, and anything is a theorem of Ax.
  - Possible dataforms are Refutations of Ax. -}

  , ("SatisfiableConclusionContradictoryAxioms", "SCA")
  {- No interpretations are models of Ax, and
  some interpretations are models of C.
  - See ContradictoryAxioms. -}

  , ("TautologousConclusionContradictoryAxioms", "TCA")
  {- No interpretations are models of Ax, and
  all interpretations are models of C.
  - See TautologousConclusion and SatisfiableConclusionContradictoryAxioms. -}

  , ("WeakerConclusionContradictoryAxioms", "WCA")
  {- No interpretations are models of Ax, and
  some, but not all, interpretations are models of C.
  - See SatisfiableConclusionContradictoryAxioms and
    SatisfiableCounterConclusionContradictoryAxioms. -}

  , ("CounterUnsatisfiabilityPreserving", "CUP")
  {- If there does not exist a model of Ax then there does not exist a model of
  ~C, i.e., if Ax is unsatisfiable then ~C is unsatisfiable. -}

  , ("CounterSatisfiabilityPreserving", "CSP")
  {- If there exists a model of Ax then there exists a model of ~C, i.e., if Ax
  is satisfiable then ~C is satisfiable. -}

  , ("EquiCounterSatisfiable", "ECS")
  {- There exists a model of Ax iff there exists a model of ~C, i.e., Ax is
  (un)satisfiable iff ~C is (un)satisfiable. -}

  , ("CounterSatisfiable", "CSA")
  {- Some interpretations are models of Ax, and
  some models of Ax are models of ~C.
  - F is not valid, ~F is satisfiable, and C is not a theorem of Ax.
  - Possible dataforms are Models of Ax | ~C. -}

  , ("CounterTheorem", "CTH")
  {- All models of Ax are models of ~C.
  - F is not valid, and ~C is a theorem of Ax.
  - Possible dataforms are Proofs of ~C from Ax. -}

  , ("CounterEquivalent", "CEQ")
  {- Some interpretations are models of Ax,
  all models of Ax are models of ~C, and
  all models of ~C are models of Ax
  (i.e., all interpretations are models of Ax xor of C).
  - F is not valid, and ~C is a theorem of Ax.
  - Possible dataforms are Proofs of ~C from Ax and of Ax from ~C. -}

  , ("UnsatisfiableConclusion", "UNC")
  {- Some interpretations are models of Ax, and
  all interpretations are models of ~C
  (i.e., no interpretations are models of C).
  - F is not valid, and ~C is a tautology.
  - Possible dataforms are Proofs of ~C. -}

  , ("WeakerCounterConclusion", "WCC")
  {- Some interpretations are models of Ax, and
  all models of Ax are models of ~C, and
  some models of ~C are not models of Ax.
  - See CounterTheorem and CounterSatisfiable. -}

  , ("EquivalentCounterTheorem", "ECT")
  {- Some, but not all, interpretations are models of Ax,
  all models of Ax are models of ~C, and
  all models of ~C are models of Ax.
  - See CounterEquivalent. -}

  , ("FinitelyUnsatisfiable", "FUN")
  {- All finite interpretations are finite models of Ax, and
  all finite interpretations are finite models of ~C
  (i.e., no finite interpretations are finite models of C). -}

  , ("Unsatisfiable", "UNS")
  {- All interpretations are models of Ax, and
  all interpretations are models of ~C.
  (i.e., no interpretations are models of C).
  - F is unsatisfiable, ~F is valid, and ~C is a tautology.
  - Possible dataforms are Proofs of Ax and of C, and Refutations of F. -}

  , ("WeakerUnsatisfiableConclusion", "WUC")
  {- Some, but not all, interpretations are models of Ax, and
  all interpretations are models of ~C.
  - See Unsatisfiable and WeakerCounterConclusion. -}

  , ("WeakerCounterTheorem", "WCT")
  {- Some interpretations are models of Ax,
  all models of Ax are models of ~C,
  some models of ~C are not models of Ax, and
  some interpretations are not models of ~C.
  - See CounterSatisfiable. -}

  , ("SatisfiableCounterConclusionContradictoryAxioms", "SCC")
  {- No interpretations are models of Ax, and
  some interpretations are models of ~C.
  - See ContradictoryAxioms. -}

  , ("UnsatisfiableConclusionContradictoryAxioms", "UCA")
  {- No interpretations are models of Ax, and
  all interpretations are models of ~C
  (i.e., no interpretations are models of C).
  - See UnsatisfiableConclusion and
  - SatisfiableCounterConclusionContradictoryAxioms. -}

  , ("NoConsequence", "NOC") ]
  {- Some interpretations are models of Ax,
  some models of Ax are models of C, and
  some models of Ax are models of ~C.
  - F is not valid, F is satisfiable, ~F is not valid, ~F is satisfiable, and
    C is not a theorem of Ax.
  - Possible dataforms are pairs of models, one Model of Ax | C and one Model
    of Ax | ~C. -}

nosuccess :: [(String, String)]
nosuccess :: [(String, String)]
nosuccess =
  [ ("NoSuccess", "NOS")
  -- The logical data has not been processed successfully (yet).

  , ("Open", "OPN")
  -- A success value has never been established.

  , ("Unknown", "UNK")
  -- Success value unknown, and no assumption has been made.

  , ("Assumed", "ASS(U,S)")
  {- The success ontology value S has been assumed because the actual value is
  unknown for the no-success ontology reason U. U is taken from the
  subontology starting at Unknown in the no-success ontology. -}

  , ("Stopped", "STP")
  {- Software attempted to process the data, and stopped without a success
  status. -}

  , ("Error", "ERR")
  -- Software stopped due to an error.

  , ("OSError", "OSE")
  -- Software stopped due to an operating system error.

  , ("InputError", "INE")
  -- Software stopped due to an input error.

  , ("SyntaxError", "SYE")
  -- Software stopped due to an input syntax error.

  , ("SemanticError", "SEE")
  -- Software stopped due to an input semantic error.

  , ("TypeError", "TYE")
  -- Software stopped due to an input type error (for typed logical data).

  , ("Forced", "FOR")
  -- Software was forced to stop by an external force.

  , ("User", "USR")
  -- Software was forced to stop by the user.

  , ("ResourceOut", "RSO")
  -- Software stopped because some resource ran out.

  , ("Timeout", "TMO")
  -- Software stopped because the CPU time limit ran out.

  , ("MemoryOut", "MMO")
  -- Software stopped because the memory limit ran out.

  , ("GaveUp", "GUP")
  -- Software gave up of its own accord.

  , ("Incomplete", "INC")
  -- Software gave up because it's incomplete.

  , ("Inappropriate", "IAP")
  -- Software gave up because it cannot process this type of data.

  , ("InProgress", "INP")
  -- Software is still running.

  , ("NotTried", "NTT")
  -- Software has not tried to process the data.

  , ("NotTriedYet", "NTY") ]
  -- Software has not tried to process the data yet, but might in the future.

szsCheck :: [(String, String)] -> [String] -> String -> Bool
szsCheck :: [(String, String)] -> [String] -> String -> Bool
szsCheck pl :: [(String, String)]
pl l :: [String]
l = Bool -> (String -> Bool) -> Maybe String -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
l)
   (Maybe String -> Bool)
-> (String -> Maybe String) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` ((String, String) -> (String, String))
-> [(String, String)] -> [(String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (t :: String
t, r :: String
r) -> ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
t, String
r)) [(String, String)]
pl) (String -> Maybe String)
-> (String -> String) -> String -> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower

szsProved :: String -> Bool
szsProved :: String -> Bool
szsProved = [(String, String)] -> [String] -> String -> Bool
szsCheck [(String, String)]
successes ["SAT", "THM"]

szsDisproved :: String -> Bool
szsDisproved :: String -> Bool
szsDisproved = [(String, String)] -> [String] -> String -> Bool
szsCheck [(String, String)]
successes ["CSA", "UNS"]

szsTimeout :: String -> Bool
szsTimeout :: String -> Bool
szsTimeout = [(String, String)] -> [String] -> String -> Bool
szsCheck [(String, String)]
nosuccess ["TMO", "RSO"]

szsMemoryOut :: String -> Bool
szsMemoryOut :: String -> Bool
szsMemoryOut = [(String, String)] -> [String] -> String -> Bool
szsCheck [(String, String)]
nosuccess ["MMO"]

szsStopped :: String -> Bool
szsStopped :: String -> Bool
szsStopped = [(String, String)] -> [String] -> String -> Bool
szsCheck [(String, String)]
nosuccess ["STP"]