Hets - the Heterogeneous Tool Set

Copyright(c) Till Mossakowski Klaus Luettich Uni Bremen 2002-2005
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable (deriving Typeable)
Safe HaskellNone

Logic.Prover

Contents

Description

General datastructures for theorem prover interfaces

Synopsis

pack sentences with their proofs

type SenStatus a tStatus = SenAttr a (ThmStatus tStatus) Source #

instead of the sentence name (that will be the key into the order map) the theorem status will be stored as attribute. The theorem status will be a (wrapped) list of pairs (AnyComorphism, BasicProof) in G_theory, but a wrapped list of (ProofStatus proof_tree) in a logic specific Theory.

thmStatus :: SenStatus a tStatus -> [tStatus] Source #

data ThmStatus a Source #

the wrapped list of proof scripts or (AnyComorphism, BasicProof) pairs

Constructors

ThmStatus 

Fields

Instances

Eq a => Eq (ThmStatus a) Source # 

Methods

(==) :: ThmStatus a -> ThmStatus a -> Bool

(/=) :: ThmStatus a -> ThmStatus a -> Bool

Ord a => Ord (ThmStatus a) Source # 

Methods

compare :: ThmStatus a -> ThmStatus a -> Ordering

(<) :: ThmStatus a -> ThmStatus a -> Bool

(<=) :: ThmStatus a -> ThmStatus a -> Bool

(>) :: ThmStatus a -> ThmStatus a -> Bool

(>=) :: ThmStatus a -> ThmStatus a -> Bool

max :: ThmStatus a -> ThmStatus a -> ThmStatus a

min :: ThmStatus a -> ThmStatus a -> ThmStatus a

Show a => Show (ThmStatus a) Source # 

Methods

showsPrec :: Int -> ThmStatus a -> ShowS

show :: ThmStatus a -> String

showList :: [ThmStatus a] -> ShowS

ShATermLG a => ShATermLG (ThmStatus a) Source # 

Methods

toShATermLG :: ATermTable -> ThmStatus a -> IO (ATermTable, Int) Source #

fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, ThmStatus a) Source #

type ThSens a b = OMap String (SenStatus a b) Source #

the map from labels to the theorem plus status (and position)

mapThSensValueM :: Monad m => (a -> m b) -> ThSens a c -> m (ThSens b c) Source #

joinSensAux :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> (ThSens a b, [(String, String)]) Source #

join and disambiguate

  • separate Axioms from Theorems
  • don't merge sentences with same key but different contents?

joinSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b Source #

intersectSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b Source #

reduceSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b Source #

cmpSnd :: Ord a1 => (String, ElemWOrd (SenStatus a1 b)) -> (String, ElemWOrd (SenStatus a1 b)) -> Ordering Source #

cmpSenEle :: Ord a1 => ElemWOrd (SenStatus a1 b) -> ElemWOrd (SenStatus a1 b) -> Ordering Source #

mapValue :: (a -> b) -> SenStatus a c -> SenStatus b c Source #

markAsAxiom :: Ord a => Bool -> ThSens a b -> ThSens a b Source #

sets the field isAxiom according to the boolean value; if isAxiom is False for a sentence and set to True, the field wasTheorem is set to True.

markAsGoal :: Ord a => ThSens a b -> ThSens a b Source #

toNamed :: String -> SenStatus a b -> Named a Source #

toThSens :: Ord a => [Named a] -> ThSens a b Source #

putting Sentences from a list into a map

data Theory sign sen proof_tree Source #

theories with a signature and sentences with proof states

Constructors

Theory sign (ThSens sen (ProofStatus proof_tree)) 

data Reason Source #

failure reason

Constructors

Reason [String] 

Instances

Eq Reason Source # 

Methods

(==) :: Reason -> Reason -> Bool

(/=) :: Reason -> Reason -> Bool

Ord Reason Source # 

Methods

compare :: Reason -> Reason -> Ordering

(<) :: Reason -> Reason -> Bool

(<=) :: Reason -> Reason -> Bool

(>) :: Reason -> Reason -> Bool

(>=) :: Reason -> Reason -> Bool

max :: Reason -> Reason -> Reason

min :: Reason -> Reason -> Reason

data GoalStatus Source #

enumeration type representing the status of a goal

Constructors

Open Reason

failure reason

Disproved 
Proved Bool

True means consistent; False inconsistent

Instances

Eq GoalStatus Source # 

Methods

(==) :: GoalStatus -> GoalStatus -> Bool

(/=) :: GoalStatus -> GoalStatus -> Bool

Ord GoalStatus Source # 
Show GoalStatus Source # 

Methods

showsPrec :: Int -> GoalStatus -> ShowS

show :: GoalStatus -> String

showList :: [GoalStatus] -> ShowS

data ProofStatus proof_tree Source #

data type representing the proof status for a goal

Constructors

ProofStatus 

Fields

Instances

Eq proof_tree => Eq (ProofStatus proof_tree) Source # 

Methods

(==) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool

(/=) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool

Ord proof_tree => Ord (ProofStatus proof_tree) Source # 

Methods

compare :: ProofStatus proof_tree -> ProofStatus proof_tree -> Ordering

(<) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool

(<=) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool

(>) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool

(>=) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool

max :: ProofStatus proof_tree -> ProofStatus proof_tree -> ProofStatus proof_tree

min :: ProofStatus proof_tree -> ProofStatus proof_tree -> ProofStatus proof_tree

Show proof_tree => Show (ProofStatus proof_tree) Source # 

Methods

showsPrec :: Int -> ProofStatus proof_tree -> ShowS

show :: ProofStatus proof_tree -> String

showList :: [ProofStatus proof_tree] -> ShowS

openProofStatus Source #

Arguments

:: Ord pt 
=> String

name of the goal

-> String

name of the prover

-> pt 
-> ProofStatus pt 

constructs an open proof status with basic information filled in; make sure to set proofTree to a useful value before you access it.

isProvedStat :: ProofStatus proof_tree -> Bool Source #

data ProverKind Source #

different kinds of prover interfaces

hasProverKind :: ProverKind -> ProverTemplate x s m y z -> Bool Source #

determine if a prover kind is implemented

data FreeDefMorphism sentence morphism Source #

Constructors

FreeDefMorphism 

Fields

Instances

(Eq sentence, Eq morphism) => Eq (FreeDefMorphism sentence morphism) Source # 

Methods

(==) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool

(/=) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool

(Ord sentence, Ord morphism) => Ord (FreeDefMorphism sentence morphism) Source # 

Methods

compare :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Ordering

(<) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool

(<=) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool

(>) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool

(>=) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool

max :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism

min :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism

(Show sentence, Show morphism) => Show (FreeDefMorphism sentence morphism) Source # 

Methods

showsPrec :: Int -> FreeDefMorphism sentence morphism -> ShowS

show :: FreeDefMorphism sentence morphism -> String

showList :: [FreeDefMorphism sentence morphism] -> ShowS

data ProverTemplate theory sentence morphism sublogics proof_tree Source #

prover or consistency checker

Constructors

Prover 

Fields

type Prover sign sentence morphism sublogics proof_tree = ProverTemplate (Theory sign sentence proof_tree) sentence morphism sublogics proof_tree Source #

mkProverTemplate :: String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO [ProofStatus proof_tree]) -> ProverTemplate theory sentence morphism sublogics proof_tree Source #

mkUsableProver :: String -> String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO [ProofStatus proof_tree]) -> ProverTemplate theory sentence morphism sublogics proof_tree Source #

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 Source #

data TheoryMorphism sign sen mor proof_tree Source #

theory morphisms between two theories

Constructors

TheoryMorphism 

Fields

data CCStatus proof_tree Source #

Constructors

CCStatus 

Fields

data ConsChecker sign sentence sublogics morphism proof_tree Source #

Constructors

ConsChecker 

Fields

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 Source #

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 Source #

Orphan instances