Index

A

acc_diags() (hets.ProofState method) as_json() (hets.GMorphism method) (hets.Sentence method)

associativity_annotations() (hets.GlobalAnnotations method) automatic() (hets.Library method) automatic_hide_theorem_shift() (hets.Library method) axioms() (hets.Theory method)

B

BasicProof (class in hets)

best_proof() (hets.Sentence method)

C

check_conservativity() (hets.DevGraphEdge method) check_consistency() (hets.DevGraphNode method) codomain() (hets.GMorphism method) COFREE (hets.EdgeKind attribute) Comorphism (class in hets) comorphism() (hets.GMorphism method) composition_prove_edges() (hets.Library method) compute_colimit() (hets.Library method) CONJECTURED (hets.ProofKind attribute) CONSERVATIVE (hets.ConsistencyKind attribute)

conservativity() (hets.DefinitionDevGraphEdge method) (hets.DevGraphEdge method) (hets.Library method) (hets.TheoremDevGraphEdge method) conservativity_status() (hets.DevGraphEdge method) ConservativityChecker (class in hets) consistency_status() (hets.LocalDevGraphNode method) ConsistencyChecker (class in hets) ConsistencyKind (class in hets) ConsistencyStatus (class in hets)

D

DEFINITIONAL (hets.ConsistencyKind attribute) DefinitionDevGraphEdge (class in hets) dependencies() (hets.Library method) description (hets.Option attribute) description() (hets.GMorphism method) (hets.Logic method) details() (hets.BasicProof method)

development_graph() (hets.Library method) DevelopmentGraph (class in hets) DevGraphEdge (class in hets) DevGraphNode (class in hets) display_annos() (hets.GlobalAnnotations method) DISPROVEN (hets.ProofKind attribute) domain() (hets.GMorphism method)

E

EdgeKind (class in hets) edges() (hets.DevelopmentGraph method)

environment() (hets.Library method) ERROR (hets.ConsistencyKind attribute)

F

FREE (hets.EdgeKind attribute)

freeness() (hets.Library method)

G

get_available_comorphisms() (hets.Theory method) get_conservativity_checker_by_name() (hets.DevGraphEdge method) get_consistency_checker_by_name() (hets.Theory method) get_prover_by_name() (hets.Theory method) get_refinement_tree() (hets.Library method) get_sublogic() (hets.Theory method) get_usable() (hets.ConservativityChecker method) get_usable_conservativity_checkers() (hets.DevGraphEdge method) get_usable_consistency_checkers() (hets.Theory method) get_usable_consistency_checkers_and_comorphisms() (hets.Theory method) get_usable_consistency_checkers_with_comorphisms() (hets.Theory method) get_usable_provers() (hets.Theory method)

get_usable_provers_and_comorphisms() (hets.Theory method) get_usable_provers_with_comorphisms() (hets.Theory method) GLOBAL (hets.EdgeKind attribute) global_annotations() (hets.DevelopmentGraph method) global_decomposition() (hets.Library method) global_subsume() (hets.Library method) global_theory() (hets.DevGraphNode method) GlobalAnnotations (class in hets) GMorphism (class in hets) goal_name() (hets.ProofDetails method) goal_status() (hets.ProofDetails method) goals() (hets.Theory method) GUESSED (hets.ProofKind attribute)

H

HANDWRITTEN (hets.ProofKind attribute)

HIDING (hets.EdgeKind attribute) hs_update_result() (hets.Library method)

I

id() (hets.DevGraphEdge method) (hets.DevGraphNode method) included_axioms() (hets.ProofState method) included_theorems() (hets.ProofState method) INCONSISTENT (hets.ConsistencyKind attribute) info() (hets.DevGraphEdge method) (hets.DevGraphNode method) is_axiom() (hets.Sentence method) is_conjectured() (hets.BasicProof method) is_conservativ() (hets.TheoremDevGraphEdge method) is_consistency_proven() (hets.DevGraphNode method) is_defined() (hets.Sentence method)

is_guessed() (hets.BasicProof method) is_handwritten() (hets.BasicProof method) is_homogeneous() (hets.DevGraphEdge method) is_inclusion() (hets.DevGraphEdge method) (hets.GMorphism method) is_internal() (hets.DevGraphNode method) is_pending() (hets.TheoremDevGraphEdge method) is_proven() (hets.Sentence method) (hets.TheoremDevGraphEdge method) is_proven_link() (hets.ConsistencyStatus method) is_proven_node() (hets.DevGraphNode method) is_reference_node() (hets.DevGraphNode method)

K

kind() (hets.BasicProof method) (hets.DevGraphEdge method) (hets.ProofDetails method)

L

lib_flat_d_unions() (hets.Library method) lib_flat_heterogen() (hets.Library method) lib_flat_hiding() (hets.Library method) lib_flat_imports() (hets.Library method) lib_flat_renamings() (hets.Library method) Library (class in hets) literal_annos() (hets.GlobalAnnotations method)

load_library (class in hets) LOCAL (hets.EdgeKind attribute) local_decomposition() (hets.Library method) local_inference() (hets.Library method) LocalDevGraphNode (class in hets) Logic (class in hets) logic() (hets.Theory method)

M

MONOMORPHIC (hets.ConsistencyKind attribute)

morphism() (hets.DevGraphEdge method)

N

name (hets.Option attribute) name() (hets.Comorphism method) (hets.ConservativityChecker method) (hets.ConsistencyChecker method) (hets.DevGraphEdge method) (hets.DevGraphNode method) (hets.GMorphism method) (hets.Library method) (hets.Logic method) (hets.Prover method) (hets.Sentence method)

node_by_id() (hets.DevelopmentGraph method) nodes() (hets.DevelopmentGraph method) non_imported_symbols() (hets.Signature method) NONE (hets.ConsistencyKind attribute) normal_form() (hets.Library method)

O

OPEN (hets.ProofKind attribute) Option (class in hets)

Options (class in hets) origin() (hets.DevGraphEdge method)

P

patch() (hets.Options method) path_length() (hets.Comorphism method) plain() (hets.Signature method) precedence_annotations() (hets.GlobalAnnotations method) prefix_map() (hets.GlobalAnnotations method) priority() (hets.Sentence method) proof_lines() (hets.ProofDetails method) PROOF_THEORETICALLY_CONSERVATIVE (hets.ConsistencyKind attribute) proof_tree() (hets.ProofDetails method)

ProofDetails (class in hets) ProofKind (class in hets) ProofState (class in hets) prove() (hets.DevGraphNode method) PROVEN (hets.ProofKind attribute) proven() (hets.ConsistencyStatus method) PROVEN_BY_INCONSISTENCY (hets.ProofKind attribute) proven_goals() (hets.Theory method) Prover (class in hets)

Q

qualify_lib_env() (hets.Library method)

R

recompute() (hets.DevGraphNode method) referenced_libname() (hets.ReferenceDevGraphNode method)

referenced_library() (hets.Library method) ReferenceDevGraphNode (class in hets) required() (hets.ConsistencyStatus method)

S

selected_cons_checker_name() (hets.ProofState method) selected_goals() (hets.ProofState method) selected_prover_name() (hets.ProofState method) Sentence (class in hets) sentence_by_name() (hets.Theory method) sentences() (hets.Theory method)

short_name() (hets.ConsistencyKind method) Signature (class in hets) signature() (hets.GMorphism method) (hets.Theory method) source() (hets.Comorphism method) specifications() (hets.Library method) symbol_map() (hets.GMorphism method)

T

tactic_script() (hets.ProofDetails method) target() (hets.Comorphism method) (hets.DevGraphEdge method) theorem_hide_shift() (hets.Library method) theorem_status() (hets.Sentence method) TheoremDevGraphEdge (class in hets) Theory (class in hets) theory() (hets.DevGraphNode method)

TIMED_OUT (hets.ConsistencyKind attribute) (hets.ProofKind attribute) title() (hets.DevGraphEdge method) to_dict() (hets.Options method) to_str() (hets.ConsistencyKind method) (hets.ProofKind method) translate() (hets.Theory method) triangle_cons() (hets.Library method) typ (hets.Option attribute)

U

UNKNOWN (hets.ConsistencyKind attribute) (hets.EdgeKind attribute) (hets.ProofKind attribute)

unproven_goals() (hets.Theory method) used_axioms() (hets.ProofDetails method) used_prover() (hets.ProofDetails method) used_time() (hets.ProofDetails method)

W

was_theorem() (hets.Sentence method)

with_selection() (hets.Theory method)