Logic.Prover

Contents

• pack sentences with their proofs

Description

Synopsis

• type SenStatus a tStatus = SenAttr a (ThmStatus tStatus)
• thmStatus :: SenStatus a tStatus -> [tStatus]
• data ThmStatus a = ThmStatus {
  • getThmStatus :: [a]
  }
• emptySenStatus :: SenStatus a b
• printOMapElemWOrd :: (a -> Doc) -> ElemWOrd a -> Doc
• type ThSens a b = OMap String (SenStatus a b)
• noSens :: ThSens a b
• mapThSensValueM :: Monad m => (a -> m b) -> ThSens a c -> m (ThSens b c)
• joinSensAux :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> (ThSens a b, [(String, String)])
• joinSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b
• reduceSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b
• cmpSnd :: Ord a1 => (String, ElemWOrd (SenStatus a1 b)) -> (String, ElemWOrd (SenStatus a1 b)) -> Ordering
• cmpSenEle :: Ord a1 => ElemWOrd (SenStatus a1 b) -> ElemWOrd (SenStatus a1 b) -> Ordering
• mapValue :: (a -> b) -> SenStatus a c -> SenStatus b c
• markAsAxiom :: Ord a => Bool -> ThSens a b -> ThSens a b
• markAsGoal :: Ord a => ThSens a b -> ThSens a b
• toNamedList :: ThSens a b -> [Named a]
• toNamed :: String -> SenStatus a b -> Named a
• toThSens :: Ord a => [Named a] -> ThSens a b
• data Theory sign sen proof_tree = Theory sign (ThSens sen (ProofStatus proof_tree))
• data TacticScript = TacticScript String
• data Reason = Reason [String]
• data GoalStatus
  • = Open Reason
  • | Disproved
  • | Proved Bool
• isOpenGoal :: GoalStatus -> Bool
• openGoalStatus :: GoalStatus
• data ProofStatus proof_tree = ProofStatus {
  • goalName :: String
  • goalStatus :: GoalStatus
  • usedAxioms :: [String]
  • usedProver :: String
  • proofTree :: proof_tree
  • usedTime :: TimeOfDay
  • tacticScript :: TacticScript
  }
• openProofStatus :: Ord pt => String -> String -> pt -> ProofStatus pt
• isProvedStat :: ProofStatus proof_tree -> Bool
• isProvedGStat :: GoalStatus -> Bool
• data ProverKind
  • = ProveGUI
  • | ProveCMDLautomatic
• hasProverKind :: ProverKind -> ProverTemplate x s m y z -> Bool
• data FreeDefMorphism sentence morphism = FreeDefMorphism {
  • freeDefMorphism :: morphism
  • pathFromFreeDef :: morphism
  • freeTheory :: [Named sentence]
  • isCofree :: Bool
  }
• data ProverTemplate theory sentence morphism sublogics proof_tree = Prover {
  • proverName :: String
  • proverUsable :: IO (Maybe String)
  • proverSublogic :: sublogics
  • proveGUI :: Maybe (String -> theory -> [FreeDefMorphism sentence morphism] -> IO ([ProofStatus proof_tree], [(Named sentence, ProofStatus proof_tree)]))
  • proveCMDLautomaticBatch :: Maybe (Bool -> Bool -> MVar (Result [ProofStatus proof_tree]) -> String -> TacticScript -> theory -> [FreeDefMorphism sentence morphism] -> IO (ThreadId, MVar ()))
  }
• type Prover sign sentence morphism sublogics proof_tree = ProverTemplate (Theory sign sentence proof_tree) sentence morphism sublogics proof_tree
• mkProverTemplate :: String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO [ProofStatus proof_tree]) -> ProverTemplate theory sentence morphism sublogics proof_tree
• mkUsableProver :: String -> String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO [ProofStatus proof_tree]) -> ProverTemplate theory sentence morphism sublogics proof_tree
• mkAutomaticProver :: String -> String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO [ProofStatus proof_tree]) -> (Bool -> Bool -> MVar (Result [ProofStatus proof_tree]) -> String -> TacticScript -> theory -> [FreeDefMorphism sentence morphism] -> IO (ThreadId, MVar ())) -> ProverTemplate theory sentence morphism sublogics proof_tree
• data TheoryMorphism sign sen mor proof_tree = TheoryMorphism {
  • tSource :: Theory sign sen proof_tree
  • tTarget :: Theory sign sen proof_tree
  • tMorphism :: mor
  }
• data CCStatus proof_tree = CCStatus {
  • ccProofTree :: proof_tree
  • ccUsedTime :: TimeOfDay
  • ccResult :: Maybe Bool
  }
• data ConsChecker sign sentence sublogics morphism proof_tree = ConsChecker {
  • ccName :: String
  • ccUsable :: IO (Maybe String)
  • ccSublogic :: sublogics
  • ccBatch :: Bool
  • ccNeedsTimer :: Bool
  • ccAutomatic :: String -> TacticScript -> TheoryMorphism sign sentence morphism proof_tree -> [FreeDefMorphism sentence morphism] -> IO (CCStatus proof_tree)
  }
• mkConsChecker :: String -> sublogics -> (String -> TacticScript -> TheoryMorphism sign sentence morphism proof_tree -> [FreeDefMorphism sentence morphism] -> IO (CCStatus proof_tree)) -> ConsChecker sign sentence sublogics morphism proof_tree
• mkUsableConsChecker :: String -> String -> sublogics -> (String -> TacticScript -> TheoryMorphism sign sentence morphism proof_tree -> [FreeDefMorphism sentence morphism] -> IO (CCStatus proof_tree)) -> ConsChecker sign sentence sublogics morphism proof_tree

pack sentences with their proofs