Hets - the Heterogeneous Tool Set

Copyright(c) Rene Wagner Klaus Luettich Uni Bremen 2005-2007
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerluecke@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable (imports Logic)
Safe HaskellNone

SoftFOL.Logic_SoftFOL

Contents

Description

Instance of class Logic for SoftFOL.

Synopsis

Documentation

data SoftFOL Source #

A dummy datatype for the LogicGraph and for identifying the right instances

Constructors

SoftFOL 

Instances

Show SoftFOL Source # 

Methods

showsPrec :: Int -> SoftFOL -> ShowS

show :: SoftFOL -> String

showList :: [SoftFOL] -> ShowS

Language SoftFOL Source # 

Methods

language_name :: SoftFOL -> String Source #

description :: SoftFOL -> String Source #

Sentences SoftFOL Sentence Sign SoftFOLMorphism SFSymbol Source # 
Comorphism SoftFOL2CommonLogic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree Source # 

Methods

parse_basic_sen :: SoftFOL -> Maybe ([TPTP] -> AParser st Sentence) Source #

stability :: SoftFOL -> Stability Source #

data_logic :: SoftFOL -> Maybe AnyLogic Source #

top_sublogic :: SoftFOL -> () Source #

all_sublogics :: SoftFOL -> [()] Source #

bottomSublogic :: SoftFOL -> Maybe () Source #

sublogicDimensions :: SoftFOL -> [[()]] Source #

parseSublogic :: SoftFOL -> String -> Maybe () Source #

proj_sublogic_epsilon :: SoftFOL -> () -> Sign -> SoftFOLMorphism Source #

provers :: SoftFOL -> [Prover Sign Sentence SoftFOLMorphism () ProofTree] Source #

default_prover :: SoftFOL -> String Source #

cons_checkers :: SoftFOL -> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree] Source #

conservativityCheck :: SoftFOL -> [ConservativityChecker Sign Sentence SoftFOLMorphism] Source #

empty_proof_tree :: SoftFOL -> ProofTree Source #

syntaxTable :: SoftFOL -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: SoftFOL -> Maybe OMCD Source #

export_symToOmdoc :: SoftFOL -> NameMap SFSymbol -> SFSymbol -> String -> Result TCElement Source #

export_senToOmdoc :: SoftFOL -> NameMap SFSymbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: SoftFOL -> SigMap SFSymbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result SFSymbol Source #

omdocToSen :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

Syntax SoftFOL [TPTP] SFSymbol () () Source # 
StaticAnalysis SoftFOL [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () Source # 

Methods

basic_analysis :: SoftFOL -> Maybe (([TPTP], Sign, GlobalAnnos) -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence])) Source #

sen_analysis :: SoftFOL -> Maybe (([TPTP], Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: SoftFOL -> IRI -> LibName -> [TPTP] -> Sign -> GlobalAnnos -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence]) Source #

stat_symb_map_items :: SoftFOL -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: SoftFOL -> Sign -> [()] -> Result [()] Source #

convertTheory :: SoftFOL -> Maybe ((Sign, [Named Sentence]) -> [TPTP]) Source #

ensures_amalgamability :: SoftFOL -> ([CASLAmalgOpt], Gr Sign (Int, SoftFOLMorphism), [(Int, SoftFOLMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: SoftFOL -> SoftFOLMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: SoftFOL -> Gr Sign (Int, SoftFOLMorphism) -> Result (Sign, Map Int SoftFOLMorphism) Source #

qualify :: SoftFOL -> SIMPLE_ID -> LibName -> SoftFOLMorphism -> Sign -> Result (SoftFOLMorphism, [Named Sentence]) Source #

symbol_to_raw :: SoftFOL -> SFSymbol -> () Source #

id_to_raw :: SoftFOL -> Id -> () Source #

matches :: SoftFOL -> SFSymbol -> () -> Bool Source #

empty_signature :: SoftFOL -> Sign Source #

add_symb_to_sign :: SoftFOL -> Sign -> SFSymbol -> Result Sign Source #

signature_union :: SoftFOL -> Sign -> Sign -> Result Sign Source #

signatureDiff :: SoftFOL -> Sign -> Sign -> Result Sign Source #

intersection :: SoftFOL -> Sign -> Sign -> Result Sign Source #

final_union :: SoftFOL -> Sign -> Sign -> Result Sign Source #

morphism_union :: SoftFOL -> SoftFOLMorphism -> SoftFOLMorphism -> Result SoftFOLMorphism Source #

is_subsig :: SoftFOL -> Sign -> Sign -> Bool Source #

subsig_inclusion :: SoftFOL -> Sign -> Sign -> Result SoftFOLMorphism Source #

generated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source #

cogenerated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source #

induced_from_morphism :: SoftFOL -> EndoMap () -> Sign -> Result SoftFOLMorphism Source #

induced_from_to_morphism :: SoftFOL -> EndoMap () -> ExtSign Sign SFSymbol -> ExtSign Sign SFSymbol -> Result SoftFOLMorphism Source #

is_transportable :: SoftFOL -> SoftFOLMorphism -> Bool Source #

is_injective :: SoftFOL -> SoftFOLMorphism -> Bool Source #

theory_to_taxonomy :: SoftFOL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: SoftFOL -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap SFSymbol -> EndoMap SFSymbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap SFSymbol, EndoMap SFSymbol) Source #

equiv2cospan :: SoftFOL -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap SFSymbol, EndoMap SFSymbol) Source #

extract_module :: SoftFOL -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

Orphan instances