Generated by tools/assurance-inventory.sh. Every row is derived from the F* source, the extracted OCaml, formal/fstar/build-ocaml.sh, .github/test-suites/*.yaml and the committed suite logs. No row on this page is hand-written, and nothing here can drift out of step with the tree without the regenerator noticing.
Tree: 53ec4268b. Modules analysed: 225, from 237 .fst/.fsti files.
Machine-readable copy: assurance-inventory.json · scrollable full table: assurance-inventory.html
Three materially different claims are easy to blur together:
A module with nothing in the last two columns of the full inventory below has no correctness proof, whatever the prose around it says.
The oracle is extraction, not naming.
formal/fstar/ocaml-output/<Module>.ml. It is the code that runs. Extracted types do not count: a lemma mentioning rdf_graph says nothing about an algorithm..ml) whose return type is prop, Type0 or logical. That is formalised specification, not code..ml at all — verified on every extract run, contributing zero executable code.| Lemma class | Requires |
|---|---|
| W3C-refinement theorem | names a shipping function and a declarative relation from a different pure formalisation module — the specification is stated independently of both the code and the proof |
| internal-refinement theorem | names a shipping function and a declarative relation, but the relation lives beside the code it constrains (an invariant, not an independent formalisation) |
| algorithm-correctness theorem | relates two or more shipping functions, with no declarative relation |
| local refinement lemma | everything else stated in the module |
merely Tot |
the module has shipping functions and no lemma anywhere in the corpus mentions them |
Name resolution is limited to the host module plus the modules it opens or aliases; an ambiguous identifier is dropped rather than counted, and a module whose extracted .ml is missing is reported as unclassified rather than assumed either way. The classifier therefore fails downward — a module can be under-credited here, never over-credited.
Pure formalisation modules in this tree: OWL.RL.Refinement, OWL.RL.Spec, OWL.Semantics, OWL.Semantics.MemLemmas, OWL.Semantics.Soundness, RDF.Entailment.RDF.Spec, RDF.Entailment.RDFS.ModelTheory, RDF.Entailment.RDFS.Refinement, RDF.Entailment.RDFS.SepFree, RDF.Entailment.RDFS.Spec, RDF.Entailment.Simple.ModelTheory, RDF.Entailment.Simple.Refinement, RDF.Entailment.Simple.Spec, RDF.Indexed.KeyInjectivity, RDF.Semantics.HypothesisWitness, SPARQL11.Algebra.Refinement, SPARQL11.Algebra.Spec.
| Bucket | Modules |
|---|---|
| W3C-refinement theorem | 11 |
| internal-refinement theorem | 13 |
| algorithm-correctness theorem | 29 |
| specification / proof module | 17 |
| local lemmas only | 13 |
| merely Tot | 123 |
| specification only (erased) | 0 |
| unclassified (oracle unavailable) | 19 |
Theorem counts across the whole corpus: 322 W3C-refinement, 163 internal-refinement and 364 algorithm-correctness theorems, out of 1767 lemmas in total (3 lemmas the tool could not classify).
| Measure | Count |
|---|---|
--lax / --admit_smt_queries / --admit_except pragma regions |
0 |
Active admissions (admit (), admitP, magic (), admit_smt_query), outside comments |
0 |
Active assume val declarations |
81 |
The assume val count is not a defect count: under iron rule #3 each is either an acknowledged gap with an open issue or an allowed realisation (pure I/O, a host-engine call-out, or a vendored crypto primitive).
| Module | Theorem | Proved in | Shipping function | Declarative relation | Unconditional |
|---|---|---|---|---|---|
OWL.Closure |
theorem_sameAs_symmetry_licensed |
OWL.RL.Refinement |
owl_rule_sameAs_symmetry |
eq_sym_derives |
no (has requires) |
OWL.Closure |
theorem_sameAs_reflexivity_licensed |
OWL.RL.Refinement |
owl_rule_sameAs_reflexivity |
eq_ref_derives |
no (has requires) |
OWL.Closure |
theorem_symmetric_property_licensed |
OWL.RL.Refinement |
owl_rule_symmetric_property |
prp_symp_derives |
no (has requires) |
OWL.Closure |
theorem_equivalent_class_licensed |
OWL.RL.Refinement |
owl_rule_equivalent_class |
scm_eqc1_derives |
no (has requires) |
OWL.Closure |
theorem_equivalent_property_licensed |
OWL.RL.Refinement |
owl_rule_equivalent_property |
scm_eqp1_derives |
no (has requires) |
OWL.Closure |
theorem_inverse_of_licensed |
OWL.RL.Refinement |
owl_rule_inverse_of |
prp_inv1_derives, prp_inv2_derives |
no (has requires) |
OWL.Closure |
owl_rule_sameAs_transitivity_licensed |
OWL.RL.Refinement |
owl_rule_sameAs_transitivity |
eq_trans_licensed, ig_wf_sp |
no (has requires) |
OWL.Closure |
theorem_sameAs_transitivity_licensed |
OWL.RL.Refinement |
owl_rule_sameAs_transitivity |
eq_trans_derives, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_transitive_property_licensed |
OWL.RL.Refinement |
owl_rule_transitive_property |
ig_wf_sp, prp_trp_licensed |
no (has requires) |
OWL.Closure |
theorem_transitive_property_licensed |
OWL.RL.Refinement |
owl_rule_transitive_property |
ig_wf_sp, prp_trp_derives |
no (has requires) |
OWL.Closure |
lemma_scm_eqc2_emission_licensed |
OWL.RL.Refinement |
find_objects_indexed, owl_equivalentClass, rdfs_subClassOf, term_is_iri |
ig_wf_sp, scm_eqc2_derives |
no (has requires) |
OWL.Closure |
owl_rule_scm_eqc2_licensed |
OWL.RL.Refinement |
owl_rule_scm_eqc2 |
ig_wf_sp, scm_eqc2_licensed |
no (has requires) |
OWL.Closure |
theorem_scm_eqc2_licensed |
OWL.RL.Refinement |
owl_rule_scm_eqc2 |
ig_wf_sp, scm_eqc2_derives |
no (has requires) |
OWL.Closure |
owl_rule_sameAs_replace_subject_licensed |
OWL.RL.Refinement |
owl_rule_sameAs_replace_subject |
eq_rep_s_licensed, ig_wf_subj |
no (has requires) |
OWL.Closure |
theorem_sameAs_replace_subject_licensed |
OWL.RL.Refinement |
owl_rule_sameAs_replace_subject |
eq_rep_s_derives, ig_wf_subj |
no (has requires) |
OWL.Closure |
owl_rule_sameAs_replace_object_licensed |
OWL.RL.Refinement |
owl_rule_sameAs_replace_object |
eq_rep_o_licensed, ig_wf_obj |
no (has requires) |
OWL.Closure |
theorem_sameAs_replace_object_licensed |
OWL.RL.Refinement |
owl_rule_sameAs_replace_object |
eq_rep_o_derives, ig_wf_obj |
no (has requires) |
OWL.Closure |
owl_rule_sameAs_replace_predicate_licensed |
OWL.RL.Refinement |
owl_rule_sameAs_replace_predicate |
eq_rep_p_licensed, ig_wf_pred |
no (has requires) |
OWL.Closure |
theorem_sameAs_replace_predicate_licensed |
OWL.RL.Refinement |
owl_rule_sameAs_replace_predicate |
eq_rep_p_derives, ig_wf_pred |
no (has requires) |
OWL.Closure |
lemma_scm_eqp2_emission_licensed |
OWL.RL.Refinement |
find_objects_indexed, owl_equivalentProperty, rdfs_subPropertyOf, term_is_iri |
ig_wf_sp, scm_eqp2_derives |
no (has requires) |
OWL.Closure |
owl_rule_scm_eqp2_licensed |
OWL.RL.Refinement |
owl_rule_scm_eqp2 |
ig_wf_sp, scm_eqp2_licensed |
no (has requires) |
OWL.Closure |
theorem_scm_eqp2_licensed |
OWL.RL.Refinement |
owl_rule_scm_eqp2 |
ig_wf_sp, scm_eqp2_derives |
no (has requires) |
OWL.Closure |
owl_rule_scm_dom2_licensed |
OWL.RL.Refinement |
owl_rule_scm_dom2 |
ig_wf_sp, scm_dom1_licensed |
no (has requires) |
OWL.Closure |
theorem_scm_dom2_licensed |
OWL.RL.Refinement |
owl_rule_scm_dom2 |
ig_wf_sp, scm_dom1_derives |
no (has requires) |
OWL.Closure |
owl_rule_scm_rng2_licensed |
OWL.RL.Refinement |
owl_rule_scm_rng2 |
ig_wf_sp, scm_rng1_licensed |
no (has requires) |
OWL.Closure |
theorem_scm_rng2_licensed |
OWL.RL.Refinement |
owl_rule_scm_rng2 |
ig_wf_sp, scm_rng1_derives |
no (has requires) |
OWL.Closure |
owl_rule_subprop_domain_range_licensed |
OWL.RL.Refinement |
owl_rule_subprop_domain_range |
ig_wf_sp, subprop_domain_range_licensed |
no (has requires) |
OWL.Closure |
theorem_subprop_domain_range_licensed |
OWL.RL.Refinement |
owl_rule_subprop_domain_range |
ig_wf_sp, scm_dom2_derives, scm_rng2_derives |
no (has requires) |
OWL.Closure |
lemma_decode_iri_list_licensed |
OWL.RL.Refinement |
decode_iri_list |
ig_wf_sp, owl_list_denotes |
no (has requires) |
OWL.Closure |
owl_rule_cls_oneof_licensed |
OWL.RL.Refinement |
owl_rule_cls_oneof |
cls_oo_licensed, ig_wf_sp |
no (has requires) |
OWL.Closure |
theorem_cls_oneof_licensed |
OWL.RL.Refinement |
owl_rule_cls_oneof |
cls_oo_derives, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_cls_int1_licensed |
OWL.RL.Refinement |
owl_rule_cls_int1 |
cls_int2_licensed, ig_wf_po_spec, ig_wf_sp |
no (has requires) |
OWL.Closure |
theorem_cls_int1_licensed |
OWL.RL.Refinement |
owl_rule_cls_int1 |
cls_int2_derives, ig_wf_po_spec, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_cls_uni_licensed |
OWL.RL.Refinement |
owl_rule_cls_uni |
cls_uni_licensed, ig_wf_sp |
no (has requires) |
OWL.Closure |
theorem_cls_uni_licensed |
OWL.RL.Refinement |
owl_rule_cls_uni |
cls_disjoint_union_ext_derives, ig_wf_sp, scm_uni_derives |
no (has requires) |
OWL.Closure |
lemma_all_keys_match_shares_approx |
OWL.RL.Refinement |
all_keys_match |
ig_wf_sp, shares_key_values_approx |
no (has requires) |
OWL.Closure |
owl_rule_prp_key_licensed |
OWL.RL.Refinement |
owl_rule_prp_key |
ig_wf_sp, prp_key_licensed |
no (has requires) |
OWL.Closure |
theorem_prp_key_licensed |
OWL.RL.Refinement |
owl_rule_prp_key |
ig_wf_sp, prp_key_derives_approx |
no (has requires) |
OWL.Closure |
lemma_prp_fp_derives_intro |
OWL.RL.Refinement |
owl_sameAs |
fp_from_decl, prp_fp_derives |
no (has requires) |
OWL.Closure |
owl_rule_functional_licensed |
OWL.RL.Refinement |
owl_rule_functional |
ig_wf_sp, prp_fp_licensed |
no (has requires) |
OWL.Closure |
theorem_functional_licensed |
OWL.RL.Refinement |
owl_rule_functional |
ig_wf_sp, prp_fp_derives |
no (has requires) |
OWL.Closure |
lemma_prp_ifp_derives_intro |
OWL.RL.Refinement |
owl_sameAs |
ifp_from_decl, prp_ifp_derives |
no (has requires) |
OWL.Closure |
owl_rule_inverse_functional_licensed |
OWL.RL.Refinement |
owl_rule_inverse_functional |
graph_literal_match_exact, ig_wf_po, ig_wf_pred, prp_ifp_licensed |
no (has requires) |
OWL.Closure |
theorem_inverse_functional_licensed |
OWL.RL.Refinement |
owl_rule_inverse_functional |
graph_literal_match_exact, ig_wf_po, ig_wf_pred, prp_ifp_derives |
no (has requires) |
OWL.Closure |
lemma_cls_hv1_row_intro |
OWL.RL.Refinement |
find_subjects_indexed, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cls_hv1_derives, ig_wf_po |
no (has requires) |
OWL.Closure |
lemma_cls_hv1_members_fold |
OWL.RL.Refinement |
find_subjects_indexed, owl_cls_hv1_emit, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cls_hv1_licensed, ig_wf_po |
no (has requires) |
OWL.Closure |
lemma_cls_hv1_mid_step |
OWL.RL.Refinement |
find_objects_indexed, owl_cls_hv1_mid, owl_hasValue_iri, owl_onProperty_iri |
cls_hv1_licensed, ig_wf_po, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_cls_hv1_licensed |
OWL.RL.Refinement |
owl_rule_cls_hv1 |
cls_hv1_licensed, ig_wf_po, ig_wf_sp |
no (has requires) |
OWL.Closure |
theorem_cls_hv1_licensed |
OWL.RL.Refinement |
owl_rule_cls_hv1 |
cls_hv1_derives, ig_wf_po, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_cls_hv2_licensed |
OWL.RL.Refinement |
owl_rule_cls_hv2 |
cls_hv2_licensed, ig_wf_po, ig_wf_pred, ig_wf_sp |
no (has requires) |
OWL.Closure |
theorem_cls_hv2_licensed |
OWL.RL.Refinement |
owl_rule_cls_hv2 |
cls_hv2_derives_approx, ig_wf_po, ig_wf_pred, ig_wf_sp |
no (has requires) |
OWL.Closure |
lemma_decode_chain_pair_licensed |
OWL.RL.Refinement |
decode_chain_pair |
ig_wf_sp, owl_list_denotes |
no (has requires) |
OWL.Closure |
lemma_prp_spo2_row_intro |
OWL.RL.Refinement |
find_objects_indexed, owl_propertyChainAxiom |
ig_wf_sp, owl_list_denotes, prp_spo2_derives |
no (has requires) |
OWL.Closure |
lemma_prp_spo2_mid_step |
OWL.RL.Refinement |
owl_chain2_mid, owl_propertyChainAxiom |
ig_wf_sp, owl_list_denotes, prp_spo2_licensed |
no (has requires) |
OWL.Closure |
owl_rule_property_chain_2_licensed |
OWL.RL.Refinement |
owl_rule_property_chain_2 |
ig_wf_sp, prp_spo2_licensed |
no (has requires) |
OWL.Closure |
theorem_property_chain_2_licensed |
OWL.RL.Refinement |
owl_rule_property_chain_2 |
ig_wf_sp, prp_spo2_derives |
no (has requires) |
OWL.Closure |
lemma_cls_avf_row_intro |
OWL.RL.Refinement |
find_objects_indexed, find_subjects_indexed, owl_allValuesFrom_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cls_avf_derives, ig_wf_po, ig_wf_sp |
no (has requires) |
OWL.Closure |
lemma_cls_avf_member_step |
OWL.RL.Refinement |
find_subjects_indexed, owl_allValuesFrom_iri, owl_cls_avf1_member, owl_onProperty_iri, rdf_type, subject_to_term |
cls_avf_licensed, ig_wf_po, ig_wf_sp |
no (has requires) |
OWL.Closure |
lemma_cls_avf_prop_step |
OWL.RL.Refinement |
find_objects_indexed, owl_allValuesFrom_iri, owl_cls_avf1_prop, owl_onProperty_iri |
cls_avf_licensed, ig_wf_po, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_cls_avf1_licensed |
OWL.RL.Refinement |
owl_rule_cls_avf1 |
cls_avf_licensed, ig_wf_po, ig_wf_sp |
no (has requires) |
OWL.Closure |
theorem_cls_avf1_licensed |
OWL.RL.Refinement |
owl_rule_cls_avf1 |
cls_avf_derives, ig_wf_po, ig_wf_sp |
no (has requires) |
OWL.Closure |
theorem_cax_adc_cax_dw_detection_sound |
OWL.RL.Refinement |
owl_has_disjoint_class_clash |
rdf_type_objects_resource, table6_clashes |
no (has requires) |
OWL.Closure |
owl_rule_symmetric_property_sound |
OWL.Semantics.Soundness |
owl_rule_symmetric_property |
cond_symmetric, holds_all |
no (has requires) |
OWL.Closure |
lemma_sameas_pairs_hold |
OWL.Semantics.Soundness |
sameas_pairs |
holds_all, sameas_pairs_hold |
no (has requires) |
OWL.Closure |
owl_rule_sameAs_symmetry_sound |
OWL.Semantics.Soundness |
owl_rule_sameAs_symmetry |
cond_sameas_identity, holds_all |
no (has requires) |
OWL.Closure |
decode_iri_list_sound |
OWL.Semantics.Soundness |
decode_iri_list |
holds_all, ig_wf_sp, seq_is |
no (has requires) |
OWL.Closure |
owl_rule_cls_oneof_sound |
OWL.Semantics.Soundness |
owl_rule_cls_oneof |
cond_oneof, holds_all, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_equivalent_class_sound |
OWL.Semantics.Soundness |
owl_rule_equivalent_class |
cond_equivalent_class, holds_all |
no (has requires) |
OWL.Closure |
owl_rule_equivalent_property_sound |
OWL.Semantics.Soundness |
owl_rule_equivalent_property |
cond_equivalent_property, holds_all |
no (has requires) |
OWL.Closure |
owl_rule_sameAs_reflexivity_sound |
OWL.Semantics.Soundness |
owl_rule_sameAs_reflexivity |
cond_sameas_reflexive, holds_all |
no (has requires) |
OWL.Closure |
owl_rule_differentFrom_symmetry_sound |
OWL.Semantics.Soundness |
owl_rule_differentFrom_symmetry |
cond_differentfrom_symmetric, holds_all |
no (has requires) |
OWL.Closure |
owl_rule_disjoint_with_propagation_sound |
OWL.Semantics.Soundness |
owl_rule_disjoint_with_propagation |
cond_complementof_disjoint, cond_disjointwith_symmetric, holds_all |
no (has requires) |
OWL.Closure |
owl_rule_symmetric_metapredicates_sound |
OWL.Semantics.Soundness |
owl_rule_symmetric_metapredicates |
cond_complementof_symmetric, cond_disjointwith_symmetric, cond_equivalentclass_symmetric, cond_equivalentproperty_symmetric, cond_inverseof_symmetric, cond_propertydisjointwith_symmetric, holds_all |
no (has requires) |
OWL.Closure |
decode_chain_pair_sound |
OWL.Semantics.Soundness |
decode_chain_pair |
holds_all, ig_wf_sp, seq_is |
no (has requires) |
OWL.Closure |
owl_rule_chain_to_transitive_sound |
OWL.Semantics.Soundness |
owl_rule_chain_to_transitive |
cond_chain2_transitive, holds_all, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_scm_cls_restriction_sound |
OWL.Semantics.Soundness |
owl_rule_scm_cls_restriction |
cond_restriction_subclass_of_class, holds_all |
no (has requires) |
OWL.Closure |
owl_rule_scm_eqc2_sound |
OWL.Semantics.Soundness |
owl_rule_scm_eqc2 |
cond_mutual_subclass_equivalent, holds_all, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_sameAs_replace_subject_sound |
OWL.Semantics.Soundness |
owl_rule_sameAs_replace_subject |
cond_sameas_identity, holds_all, ig_wf_subj |
no (has requires) |
OWL.Closure |
owl_rule_sameAs_replace_object_sound |
OWL.Semantics.Soundness |
owl_rule_sameAs_replace_object |
cond_sameas_identity, holds_all, ig_wf_obj |
no (has requires) |
OWL.Closure |
owl_rule_sameAs_replace_predicate_sound |
OWL.Semantics.Soundness |
owl_rule_sameAs_replace_predicate |
cond_sameas_identity, holds_all, ig_wf_pred |
no (has requires) |
OWL.Closure |
owl_rule_scm_eqp2_sound |
OWL.Semantics.Soundness |
owl_rule_scm_eqp2 |
cond_mutual_subproperty_equivalent, holds_all, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_sameAs_transitivity_sound |
OWL.Semantics.Soundness |
owl_rule_sameAs_transitivity |
cond_sameas_identity, holds_all, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_transitive_property_sound |
OWL.Semantics.Soundness |
owl_rule_transitive_property |
cond_transitive, holds_all, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_functional_sound |
OWL.Semantics.Soundness |
owl_rule_functional |
cond_functional, cond_sameas_identity, holds_all, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_inverse_functional_sound |
OWL.Semantics.Soundness |
owl_rule_inverse_functional |
cond_inverse_functional, cond_sameas_identity, graph_literal_match_exact, holds_all, ig_wf_po, ig_wf_pred |
no (has requires) |
OWL.Closure |
owl_rule_inverse_of_sound |
OWL.Semantics.Soundness |
owl_rule_inverse_of |
cond_inverse_of, holds_all |
no (has requires) |
OWL.Closure |
owl_rule_prp_key_sound |
OWL.Semantics.Soundness |
owl_rule_prp_key |
cond_haskey, cond_literal_term_eq_respecting, cond_sameas_identity, holds_all, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_scm_dom2_sound |
OWL.Semantics.Soundness |
owl_rule_scm_dom2 |
cond_domain_subclass, holds_all, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_scm_rng2_sound |
OWL.Semantics.Soundness |
owl_rule_scm_rng2 |
cond_range_subclass, holds_all, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_subprop_domain_range_sound |
OWL.Semantics.Soundness |
owl_rule_subprop_domain_range |
cond_domain_subprop, cond_range_subprop, holds_all, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_cls_int1_sound |
OWL.Semantics.Soundness |
owl_rule_cls_int1 |
cond_intersection_of, holds_all, ig_wf_po_spec, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_cls_uni_sound |
OWL.Semantics.Soundness |
owl_rule_cls_uni |
cond_union_of, holds_all, ig_wf_sp, no_disjoint_union |
no (has requires) |
OWL.Closure |
lemma_cls_hv1_witness_holds |
OWL.Semantics.Soundness |
find_subjects_indexed, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cond_hasvalue, holds_all, ig_wf_po, triple_holds |
no (has requires) |
OWL.Closure |
lemma_cls_hv1_members_fold_sound |
OWL.Semantics.Soundness |
find_subjects_indexed, owl_cls_hv1_emit, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cond_hasvalue, holds_all, ig_wf_po |
no (has requires) |
OWL.Closure |
lemma_cls_hv1_mid_step_sound |
OWL.Semantics.Soundness |
find_objects_indexed, owl_cls_hv1_mid, owl_hasValue_iri, owl_onProperty_iri |
cond_hasvalue, holds_all, ig_wf_po, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_cls_hv1_sound |
OWL.Semantics.Soundness |
owl_rule_cls_hv1 |
cond_hasvalue, holds_all, ig_wf_po, ig_wf_sp |
no (has requires) |
OWL.Closure |
lemma_cls_hv2_witness_holds |
OWL.Semantics.Soundness |
find_subjects_indexed, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cond_hasvalue, cond_literal_term_eq_respecting, holds_all, ig_wf_po, ig_wf_pred, triple_holds |
no (has requires) |
OWL.Closure |
owl_rule_cls_hv2_sound |
OWL.Semantics.Soundness |
owl_rule_cls_hv2 |
cond_hasvalue, cond_literal_term_eq_respecting, holds_all, ig_wf_po, ig_wf_pred, ig_wf_sp |
no (has requires) |
OWL.Closure |
lemma_cls_avf_witness_holds |
OWL.Semantics.Soundness |
find_objects_indexed, find_subjects_indexed, owl_allValuesFrom_iri, owl_onProperty_iri, rdf_type, subject_to_term, term_to_subject |
cond_allvaluesfrom, holds_all, ig_wf_po, ig_wf_sp, triple_holds |
no (has requires) |
OWL.Closure |
lemma_cls_avf_member_fold_sound |
OWL.Semantics.Soundness |
find_objects_indexed, find_subjects_indexed, owl_allValuesFrom_iri, owl_cls_avf1_emit, owl_onProperty_iri, rdf_type, subject_to_term |
cond_allvaluesfrom, holds_all, ig_wf_po, ig_wf_sp |
no (has requires) |
OWL.Closure |
lemma_cls_avf_prop_step_sound |
OWL.Semantics.Soundness |
find_objects_indexed, owl_allValuesFrom_iri, owl_cls_avf1_prop, owl_onProperty_iri |
cond_allvaluesfrom, holds_all, ig_wf_po, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_cls_avf1_sound |
OWL.Semantics.Soundness |
owl_rule_cls_avf1 |
cond_allvaluesfrom, holds_all, ig_wf_po, ig_wf_sp |
no (has requires) |
OWL.Closure |
lemma_prp_spo2_witness_holds |
OWL.Semantics.Soundness |
find_objects_indexed, owl_propertyChainAxiom, term_to_subject |
cond_chain2_compose, holds_all, ig_wf_sp, seq_is, triple_holds |
no (has requires) |
OWL.Closure |
lemma_prp_spo2_mid_step_sound |
OWL.Semantics.Soundness |
owl_chain2_mid, owl_propertyChainAxiom, term_to_subject |
cond_chain2_compose, holds_all, ig_wf_sp, seq_is |
no (has requires) |
OWL.Closure |
owl_rule_property_chain_2_sound |
OWL.Semantics.Soundness |
owl_rule_property_chain_2 |
cond_chain2_compose, holds_all, ig_wf_sp |
no (has requires) |
OWL.Closure |
owl_rule_symmetric_property_entailed |
OWL.Semantics.Soundness |
owl_rule_symmetric_property |
pilot_entails |
yes |
OWL.Closure |
owl_rule_sameAs_symmetry_entailed |
OWL.Semantics.Soundness |
build_indexed, owl_rule_sameAs_symmetry |
pilot_entails |
yes |
OWL.Closure |
owl_rule_cls_oneof_entailed |
OWL.Semantics.Soundness |
build_indexed, owl_rule_cls_oneof |
ig_wf_sp, pilot_entails |
no (has requires) |
Parser.NTriples |
entails_ntriples_boundary |
RDF.Entailment.Simple.Boundary |
parse_ntriples_strict |
graph_exact, simple_entailment_spec |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_rho_df_pre_dedup_clean |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure_step_pre_dedup |
graph_clean |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_rho_df_pre_dedup_no_dup_keys |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure_step_pre_dedup |
graph_clean, no_dup_keys |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_rho_df_step_clean |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure_step |
graph_clean |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_rho_df_closure_iter_clean |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure_iter |
graph_clean |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_rho_df_closure_extensive_aux |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure |
is_subgraph |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure_extensive |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure |
graph_clean, is_subgraph |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure_extensive_chain |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure |
is_subgraph |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_rho_df_step_sound |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rho_df_closure_step |
holds_all, ig_wf_sp, rho_df_conditions |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_rho_df_closure_sound_aux |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure |
holds_all, rho_df_conditions |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_f1_bad_triple_derived |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, f1_bad_triple, f1_witness, i_rdfs_subPropertyOf, rdfs_rule_subPropertyOf |
ig_wf_sp |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_frag_preservation_fails |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, f1_bad_triple, f1_witness, i_rdfs_subPropertyOf, rdfs_rule_subPropertyOf |
ig_wf_sp, rho_df_frag_graph, rho_df_frag_triple |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_rho_df_closed_row_domain |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rho_df_closure_step_pre_dedup |
ig_wf_sp, no_dup_keys, rdfs2_derives, rho_df_frag_graph |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_rho_df_closed_row_range |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rho_df_closure_step_pre_dedup |
ig_wf_sp, no_dup_keys, rdfs3_derives, rho_df_frag_graph |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_rho_df_closed_row_subPropertyOf |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rho_df_closure_step_pre_dedup |
ig_wf_sp, no_dup_keys, rdfs7_derives, rho_df_frag_graph |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_rho_df_closed_row_subClassOf_trans |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rho_df_closure_step_pre_dedup |
ig_wf_sp, no_dup_keys, rdfs11_derives, rho_df_frag_graph |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_rho_df_closed_row_subPropertyOf_trans |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rho_df_closure_step_pre_dedup |
ig_wf_sp, no_dup_keys, rdfs5_derives, rho_df_frag_graph |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_rho_df_closed_row_subClassOf |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rho_df_closure_step_pre_dedup |
ig_wf_sp, no_dup_keys, rdfs9_derives, rho_df_frag_graph |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure_closed |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, graph_len, rho_df_closure, rho_df_closure_step, rho_df_closure_step_pre_dedup |
ig_wf_sp, no_dup_keys, rho_df_closed, rho_df_frag_graph |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure_decides |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, graph_len, rho_df_closure, rho_df_closure_step, rho_df_closure_step_pre_dedup |
graph_tt_free, ig_wf_sp, no_dup_keys, rho_df_entails, rho_df_frag_graph, simple_entailment_spec |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_decides_hyps_suffices |
SPARQL11.EntailmentRegime.RDFS |
rho_df_closure |
graph_tt_free, rho_df_decides_hyps, rho_df_entails, simple_entailment_spec |
no (has requires) |
RDF.Entailment.Simple |
simple_entails_rename_invariant |
RDF.Entailment.Simple.Boundary |
simple_entails |
graph_exact |
no (has requires) |
RDF.Entailment.Simple |
simple_entails_iff_model_theory |
RDF.Entailment.Simple.ModelTheory |
simple_entails |
graph_exact, graph_tt_free, simple_entails_mt |
no (has requires) |
RDF.Entailment.Simple |
lemma_match_subj_complete |
RDF.Entailment.Simple.Refinement |
match_subj |
binding_compat, subj_inst |
no (has requires) |
RDF.Entailment.Simple |
lemma_match_term_complete |
RDF.Entailment.Simple.Refinement |
match_term |
binding_compat, bnd_total, leq_reflexive, term_inst |
no (has requires) |
RDF.Entailment.Simple |
lemma_match_triple_complete |
RDF.Entailment.Simple.Refinement |
match_triple |
binding_compat, bnd_total, leq_reflexive, triple_inst |
no (has requires) |
RDF.Entailment.Simple |
lemma_try_alts_complete |
RDF.Entailment.Simple.Refinement |
try_alts |
all_matched, binding_compat, bnd_total, leq_reflexive, triple_inst |
no (has requires) |
RDF.Entailment.Simple |
simple_entails_complete |
RDF.Entailment.Simple.Refinement |
simple_entails |
simple_entailment_spec |
no (has requires) |
RDF.Entailment.Simple |
lemma_match_subj_sound |
RDF.Entailment.Simple.Refinement |
match_subj |
binding_exact, binding_extends, subj_inst |
no (has requires) |
RDF.Entailment.Simple |
lemma_match_term_sound |
RDF.Entailment.Simple.Refinement |
match_term |
binding_exact, binding_extends, leq_exact_identity, term_exact, term_inst |
no (has requires) |
RDF.Entailment.Simple |
lemma_match_triple_sound |
RDF.Entailment.Simple.Refinement |
match_triple |
binding_exact, binding_extends, leq_exact_identity, triple_exact, triple_inst |
no (has requires) |
RDF.Entailment.Simple |
lemma_try_match_sound |
RDF.Entailment.Simple.Refinement |
try_match |
binding_exact, graph_exact, leq_exact_identity, search_witness |
no (has requires) |
RDF.Entailment.Simple |
lemma_try_alts_sound |
RDF.Entailment.Simple.Refinement |
try_alts |
binding_exact, graph_exact, is_subgraph, leq_exact_identity, search_witness, triple_exact |
no (has requires) |
RDF.Entailment.Simple |
simple_entails_sound |
RDF.Entailment.Simple.Refinement |
simple_entails |
graph_exact, simple_entailment_spec |
no (has requires) |
RDF.Entailment.Simple |
entails_with_complete |
RDF.Entailment.Simple.Refinement |
entails_with |
bnd_total, leq_reflexive, simple_entailment_spec |
no (has requires) |
RDF.Entailment.Simple |
entails_with_sound |
RDF.Entailment.Simple.Refinement |
entails_with |
graph_exact, leq_exact_identity, simple_entailment_spec |
no (has requires) |
RDF.Entailment.Simple |
simple_entails_iff_spec |
RDF.Entailment.Simple.Refinement |
simple_entails |
graph_exact, simple_entailment_spec |
no (has requires) |
RDF.Entailment.Simple |
simple_entails_se1_regression |
RDF.Entailment.Simple.Refinement |
simple_entails |
simple_entailment_spec |
no (has requires) |
RDF.Entailment.Simple |
simple_entails_se1_positive_regression |
RDF.Entailment.Simple.Refinement |
simple_entails |
simple_entailment_spec |
yes |
RDF.Entailment.Simple |
lemma_try_match_ground_sound |
RDF.Entailment.Simple.Refinement |
try_match |
graph_ground, is_subgraph, leq_always_identity |
no (has requires) |
RDF.Entailment.Simple |
lemma_try_alts_ground_sound |
RDF.Entailment.Simple.Refinement |
try_alts |
graph_ground, is_subgraph, leq_always_identity |
no (has requires) |
RDF.Entailment.Simple |
simple_entails_sound_ground |
RDF.Entailment.Simple.Refinement |
simple_entails |
graph_ground, simple_entailment_spec |
no (has requires) |
RDF.Graph |
lemma_single_add_licensed |
OWL.RL.Refinement |
add_triple_unchecked |
cls_disjoint_union_ext_derives, cls_uni_licensed, scm_uni_derives |
no (has requires) |
RDF.Graph |
lemma_find_subjects_indexed_wf_subj |
OWL.RL.Refinement |
find_subjects_indexed, subject_to_term |
ig_wf_po |
no (has requires) |
RDF.Graph |
lemma_cls_hv1_row_intro |
OWL.RL.Refinement |
find_subjects_indexed, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cls_hv1_derives, ig_wf_po |
no (has requires) |
RDF.Graph |
lemma_cls_hv1_members_fold |
OWL.RL.Refinement |
find_subjects_indexed, owl_cls_hv1_emit, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cls_hv1_licensed, ig_wf_po |
no (has requires) |
RDF.Graph |
lemma_cls_avf_row_intro |
OWL.RL.Refinement |
find_objects_indexed, find_subjects_indexed, owl_allValuesFrom_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cls_avf_derives, ig_wf_po, ig_wf_sp |
no (has requires) |
RDF.Graph |
lemma_cls_avf_member_step |
OWL.RL.Refinement |
find_subjects_indexed, owl_allValuesFrom_iri, owl_cls_avf1_member, owl_onProperty_iri, rdf_type, subject_to_term |
cls_avf_licensed, ig_wf_po, ig_wf_sp |
no (has requires) |
RDF.Graph |
lemma_cls_hv1_witness_holds |
OWL.Semantics.Soundness |
find_subjects_indexed, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cond_hasvalue, holds_all, ig_wf_po, triple_holds |
no (has requires) |
RDF.Graph |
lemma_cls_hv1_members_fold_sound |
OWL.Semantics.Soundness |
find_subjects_indexed, owl_cls_hv1_emit, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cond_hasvalue, holds_all, ig_wf_po |
no (has requires) |
RDF.Graph |
lemma_cls_hv2_witness_holds |
OWL.Semantics.Soundness |
find_subjects_indexed, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cond_hasvalue, cond_literal_term_eq_respecting, holds_all, ig_wf_po, ig_wf_pred, triple_holds |
no (has requires) |
RDF.Graph |
lemma_cls_avf_witness_holds |
OWL.Semantics.Soundness |
find_objects_indexed, find_subjects_indexed, owl_allValuesFrom_iri, owl_onProperty_iri, rdf_type, subject_to_term, term_to_subject |
cond_allvaluesfrom, holds_all, ig_wf_po, ig_wf_sp, triple_holds |
no (has requires) |
RDF.Graph |
lemma_cls_avf_member_fold_sound |
OWL.Semantics.Soundness |
find_objects_indexed, find_subjects_indexed, owl_allValuesFrom_iri, owl_cls_avf1_emit, owl_onProperty_iri, rdf_type, subject_to_term |
cond_allvaluesfrom, holds_all, ig_wf_po, ig_wf_sp |
no (has requires) |
RDF.Graph |
lemma_prp_spo2_witness_holds |
OWL.Semantics.Soundness |
find_objects_indexed, owl_propertyChainAxiom, term_to_subject |
cond_chain2_compose, holds_all, ig_wf_sp, seq_is, triple_holds |
no (has requires) |
RDF.Graph |
lemma_prp_spo2_mid_step_sound |
OWL.Semantics.Soundness |
owl_chain2_mid, owl_propertyChainAxiom, term_to_subject |
cond_chain2_compose, holds_all, ig_wf_sp, seq_is |
no (has requires) |
RDF.Graph |
lemma_len_eq_saturated_sep_free |
RDF.Entailment.RDFS.FixedPoint |
graph_len, rdfs_closure_step |
graph_obj_not_tt, graph_sep_free, step_saturated |
no (has requires) |
RDF.Graph |
lemma_add_triples_if_new_holds |
RDF.Entailment.RDFS.ModelTheory |
add_triples_if_new |
holds_all |
no (has requires) |
RDF.Graph |
rs2_rows_complete_at_build_indexed |
RDF.Entailment.RDFS.Refinement |
build_indexed, is_typed_as, rdf_type, rdfs_Class, rdfs_Datatype, rdfs_Literal, rdfs_Resource, rdfs_rule_class_subclass_resource, rdfs_rule_datatype_subclass_literal, rdfs_rule_recognized_datatypes, rdfs_rule_resource_object, rdfs_rule_resource_subject, rdfs_subClassOf, recognized_datatypes, term_to_subject |
ig_wf_sp |
no (has requires) |
RDF.Graph |
rho_df_closure_closed |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, graph_len, rho_df_closure, rho_df_closure_step, rho_df_closure_step_pre_dedup |
ig_wf_sp, no_dup_keys, rho_df_closed, rho_df_frag_graph |
no (has requires) |
RDF.Graph |
rho_df_closure_decides |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, graph_len, rho_df_closure, rho_df_closure_step, rho_df_closure_step_pre_dedup |
graph_tt_free, ig_wf_sp, no_dup_keys, rho_df_entails, rho_df_frag_graph, simple_entailment_spec |
no (has requires) |
RDF.Indexed |
lemma_find_objects_indexed_sp_elim |
OWL.RL.Refinement |
find_objects_indexed |
ig_wf_sp |
no (has requires) |
RDF.Indexed |
lemma_scm_eqc2_emission_licensed |
OWL.RL.Refinement |
find_objects_indexed, owl_equivalentClass, rdfs_subClassOf, term_is_iri |
ig_wf_sp, scm_eqc2_derives |
no (has requires) |
RDF.Indexed |
lemma_scm_eqp2_emission_licensed |
OWL.RL.Refinement |
find_objects_indexed, owl_equivalentProperty, rdfs_subPropertyOf, term_is_iri |
ig_wf_sp, scm_eqp2_derives |
no (has requires) |
RDF.Indexed |
lemma_find_subjects_indexed_wf |
OWL.RL.Refinement |
find_subjects_indexed |
graph_literal_match_exact, ig_wf_po, ig_wf_pred |
no (has requires) |
RDF.Indexed |
lemma_find_subjects_indexed_wf_subj |
OWL.RL.Refinement |
find_subjects_indexed, subject_to_term |
ig_wf_po |
no (has requires) |
RDF.Indexed |
lemma_cls_hv1_row_intro |
OWL.RL.Refinement |
find_subjects_indexed, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cls_hv1_derives, ig_wf_po |
no (has requires) |
RDF.Indexed |
lemma_cls_hv1_members_fold |
OWL.RL.Refinement |
find_subjects_indexed, owl_cls_hv1_emit, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cls_hv1_licensed, ig_wf_po |
no (has requires) |
RDF.Indexed |
lemma_cls_hv1_mid_step |
OWL.RL.Refinement |
find_objects_indexed, owl_cls_hv1_mid, owl_hasValue_iri, owl_onProperty_iri |
cls_hv1_licensed, ig_wf_po, ig_wf_sp |
no (has requires) |
RDF.Indexed |
lemma_find_subjects_indexed_wf_approx |
OWL.RL.Refinement |
find_subjects_indexed, rdf_term_eq |
ig_wf_po, ig_wf_pred |
no (has requires) |
RDF.Indexed |
lemma_prp_spo2_row_intro |
OWL.RL.Refinement |
find_objects_indexed, owl_propertyChainAxiom |
ig_wf_sp, owl_list_denotes, prp_spo2_derives |
no (has requires) |
RDF.Indexed |
lemma_cls_avf_row_intro |
OWL.RL.Refinement |
find_objects_indexed, find_subjects_indexed, owl_allValuesFrom_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cls_avf_derives, ig_wf_po, ig_wf_sp |
no (has requires) |
RDF.Indexed |
lemma_cls_avf_member_step |
OWL.RL.Refinement |
find_subjects_indexed, owl_allValuesFrom_iri, owl_cls_avf1_member, owl_onProperty_iri, rdf_type, subject_to_term |
cls_avf_licensed, ig_wf_po, ig_wf_sp |
no (has requires) |
RDF.Indexed |
lemma_cls_avf_prop_step |
OWL.RL.Refinement |
find_objects_indexed, owl_allValuesFrom_iri, owl_cls_avf1_prop, owl_onProperty_iri |
cls_avf_licensed, ig_wf_po, ig_wf_sp |
no (has requires) |
RDF.Indexed |
lemma_cls_hv1_witness_holds |
OWL.Semantics.Soundness |
find_subjects_indexed, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cond_hasvalue, holds_all, ig_wf_po, triple_holds |
no (has requires) |
RDF.Indexed |
lemma_cls_hv1_members_fold_sound |
OWL.Semantics.Soundness |
find_subjects_indexed, owl_cls_hv1_emit, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cond_hasvalue, holds_all, ig_wf_po |
no (has requires) |
RDF.Indexed |
lemma_cls_hv1_mid_step_sound |
OWL.Semantics.Soundness |
find_objects_indexed, owl_cls_hv1_mid, owl_hasValue_iri, owl_onProperty_iri |
cond_hasvalue, holds_all, ig_wf_po, ig_wf_sp |
no (has requires) |
RDF.Indexed |
lemma_cls_hv2_witness_holds |
OWL.Semantics.Soundness |
find_subjects_indexed, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cond_hasvalue, cond_literal_term_eq_respecting, holds_all, ig_wf_po, ig_wf_pred, triple_holds |
no (has requires) |
RDF.Indexed |
lemma_cls_avf_witness_holds |
OWL.Semantics.Soundness |
find_objects_indexed, find_subjects_indexed, owl_allValuesFrom_iri, owl_onProperty_iri, rdf_type, subject_to_term, term_to_subject |
cond_allvaluesfrom, holds_all, ig_wf_po, ig_wf_sp, triple_holds |
no (has requires) |
RDF.Indexed |
lemma_cls_avf_member_fold_sound |
OWL.Semantics.Soundness |
find_objects_indexed, find_subjects_indexed, owl_allValuesFrom_iri, owl_cls_avf1_emit, owl_onProperty_iri, rdf_type, subject_to_term |
cond_allvaluesfrom, holds_all, ig_wf_po, ig_wf_sp |
no (has requires) |
RDF.Indexed |
lemma_cls_avf_prop_step_sound |
OWL.Semantics.Soundness |
find_objects_indexed, owl_allValuesFrom_iri, owl_cls_avf1_prop, owl_onProperty_iri |
cond_allvaluesfrom, holds_all, ig_wf_po, ig_wf_sp |
no (has requires) |
RDF.Indexed |
lemma_prp_spo2_witness_holds |
OWL.Semantics.Soundness |
find_objects_indexed, owl_propertyChainAxiom, term_to_subject |
cond_chain2_compose, holds_all, ig_wf_sp, seq_is, triple_holds |
no (has requires) |
RDF.Indexed |
rdfs_rule_domain_entailed |
OWL.Semantics.Soundness |
build_indexed, rdfs_rule_domain |
pilot_entails |
yes |
RDF.Indexed |
rdfs_rule_range_entailed |
OWL.Semantics.Soundness |
build_indexed, rdfs_rule_range |
pilot_entails |
yes |
RDF.Indexed |
owl_rule_sameAs_symmetry_entailed |
OWL.Semantics.Soundness |
build_indexed, owl_rule_sameAs_symmetry |
pilot_entails |
yes |
RDF.Indexed |
owl_rule_cls_oneof_entailed |
OWL.Semantics.Soundness |
build_indexed, owl_rule_cls_oneof |
ig_wf_sp, pilot_entails |
no (has requires) |
RDF.Indexed |
lemma_closure_chain_wf_step |
RDF.Entailment.RDFS.ChainWf |
build_indexed |
graph_sep_free, ig_wf_sp |
no (has requires) |
RDF.Indexed |
lemma_rdfs_rule_subPropertyOf_clean |
RDF.Entailment.RDFS.FixedPoint |
build_indexed, rdfs_rule_subPropertyOf |
graph_clean |
no (has requires) |
RDF.Indexed |
lemma_rdfs_rule_domain_clean |
RDF.Entailment.RDFS.FixedPoint |
build_indexed, rdfs_rule_domain |
graph_clean |
no (has requires) |
RDF.Indexed |
lemma_rdfs_rule_range_clean |
RDF.Entailment.RDFS.FixedPoint |
build_indexed, rdfs_rule_range |
graph_clean |
no (has requires) |
RDF.Indexed |
lemma_rdfs_rule_subClassOf_clean |
RDF.Entailment.RDFS.FixedPoint |
build_indexed, rdfs_rule_subClassOf |
graph_clean |
no (has requires) |
RDF.Indexed |
lemma_rdfs_rule_subClassOf_trans_clean |
RDF.Entailment.RDFS.FixedPoint |
build_indexed, rdfs_rule_subClassOf_trans |
graph_clean |
no (has requires) |
RDF.Indexed |
lemma_rdfs_rule_subPropertyOf_trans_clean |
RDF.Entailment.RDFS.FixedPoint |
build_indexed, rdfs_rule_subPropertyOf_trans |
graph_clean |
no (has requires) |
RDF.Indexed |
rdfs_closure_step_sound |
RDF.Entailment.RDFS.ModelTheory |
build_indexed, rdfs_closure_step |
holds_all, ig_wf_sp, rdfs_conditions |
no (has requires) |
RDF.Indexed |
lemma_find_objects_elim |
RDF.Entailment.RDFS.Refinement |
find_objects_indexed |
ig_wf_sp |
no (has requires) |
RDF.Indexed |
rs2_rows_complete_at_build_indexed |
RDF.Entailment.RDFS.Refinement |
build_indexed, is_typed_as, rdf_type, rdfs_Class, rdfs_Datatype, rdfs_Literal, rdfs_Resource, rdfs_rule_class_subclass_resource, rdfs_rule_datatype_subclass_literal, rdfs_rule_recognized_datatypes, rdfs_rule_resource_object, rdfs_rule_resource_subject, rdfs_subClassOf, recognized_datatypes, term_to_subject |
ig_wf_sp |
no (has requires) |
RDF.Indexed |
lemma_rho_df_step_sound |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rho_df_closure_step |
holds_all, ig_wf_sp, rho_df_conditions |
no (has requires) |
RDF.Indexed |
rdfs_rule_domain_reaches2 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_domain |
ig_wf_sp, is_subgraph, rdfs2_derives, rho_df_frag_graph |
no (has requires) |
RDF.Indexed |
rdfs_rule_domain_reaches |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_domain |
ig_wf_sp, rdfs2_derives, rho_df_frag_graph |
no (has requires) |
RDF.Indexed |
rdfs_rule_range_reaches2 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_range |
ig_wf_sp, is_subgraph, rdfs3_derives, rho_df_frag_graph |
no (has requires) |
RDF.Indexed |
rdfs_rule_range_reaches |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_range |
ig_wf_sp, rdfs3_derives, rho_df_frag_graph |
no (has requires) |
RDF.Indexed |
rdfs_rule_subPropertyOf_reaches2 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_subPropertyOf |
ig_wf_sp, is_subgraph, rdfs7_derives, rho_df_frag_graph |
no (has requires) |
RDF.Indexed |
rdfs_rule_subPropertyOf_reaches |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_subPropertyOf |
ig_wf_sp, rdfs7_derives, rho_df_frag_graph |
no (has requires) |
RDF.Indexed |
rdfs_rule_subClassOf_trans_reaches2 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_subClassOf_trans |
ig_wf_sp, is_subgraph, rdfs11_derives |
no (has requires) |
RDF.Indexed |
rdfs_rule_subClassOf_trans_reaches |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_subClassOf_trans |
ig_wf_sp, rdfs11_derives |
no (has requires) |
RDF.Indexed |
rdfs_rule_subPropertyOf_trans_reaches2 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_subPropertyOf_trans |
ig_wf_sp, is_subgraph, rdfs5_derives |
no (has requires) |
RDF.Indexed |
rdfs_rule_subPropertyOf_trans_reaches |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_subPropertyOf_trans |
ig_wf_sp, rdfs5_derives |
no (has requires) |
RDF.Indexed |
rdfs_rule_subClassOf_reaches_iri2 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, i_rdf_type, i_rdfs_subClassOf, rdfs_rule_subClassOf |
ig_wf_sp, is_subgraph, rho_df_frag_graph |
no (has requires) |
RDF.Indexed |
rdfs_rule_subClassOf_reaches_iri |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, i_rdf_type, i_rdfs_subClassOf, rdfs_rule_subClassOf |
ig_wf_sp, rho_df_frag_graph |
no (has requires) |
RDF.Indexed |
lemma_f1_bad_triple_derived |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, f1_bad_triple, f1_witness, i_rdfs_subPropertyOf, rdfs_rule_subPropertyOf |
ig_wf_sp |
no (has requires) |
RDF.Indexed |
rho_df_frag_preservation_fails |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, f1_bad_triple, f1_witness, i_rdfs_subPropertyOf, rdfs_rule_subPropertyOf |
ig_wf_sp, rho_df_frag_graph, rho_df_frag_triple |
no (has requires) |
RDF.Indexed |
lemma_c_in_g1 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_subPropertyOf |
is_subgraph |
no (has requires) |
RDF.Indexed |
lemma_c_in_g2 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_domain, rdfs_rule_subPropertyOf |
is_subgraph |
no (has requires) |
RDF.Indexed |
lemma_c_in_g3 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_domain, rdfs_rule_range, rdfs_rule_subPropertyOf |
is_subgraph |
no (has requires) |
RDF.Indexed |
lemma_c_in_g4 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_domain, rdfs_rule_range, rdfs_rule_subClassOf, rdfs_rule_subPropertyOf |
is_subgraph |
no (has requires) |
RDF.Indexed |
lemma_c_in_g5 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_domain, rdfs_rule_range, rdfs_rule_subClassOf, rdfs_rule_subClassOf_trans, rdfs_rule_subPropertyOf |
is_subgraph |
no (has requires) |
RDF.Indexed |
lemma_rho_df_closed_row_domain |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rho_df_closure_step_pre_dedup |
ig_wf_sp, no_dup_keys, rdfs2_derives, rho_df_frag_graph |
no (has requires) |
RDF.Indexed |
lemma_rho_df_closed_row_range |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rho_df_closure_step_pre_dedup |
ig_wf_sp, no_dup_keys, rdfs3_derives, rho_df_frag_graph |
no (has requires) |
RDF.Indexed |
lemma_rho_df_closed_row_subPropertyOf |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rho_df_closure_step_pre_dedup |
ig_wf_sp, no_dup_keys, rdfs7_derives, rho_df_frag_graph |
no (has requires) |
RDF.Indexed |
lemma_rho_df_closed_row_subClassOf_trans |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rho_df_closure_step_pre_dedup |
ig_wf_sp, no_dup_keys, rdfs11_derives, rho_df_frag_graph |
no (has requires) |
RDF.Indexed |
lemma_rho_df_closed_row_subPropertyOf_trans |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rho_df_closure_step_pre_dedup |
ig_wf_sp, no_dup_keys, rdfs5_derives, rho_df_frag_graph |
no (has requires) |
RDF.Indexed |
lemma_rho_df_closed_row_subClassOf |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rho_df_closure_step_pre_dedup |
ig_wf_sp, no_dup_keys, rdfs9_derives, rho_df_frag_graph |
no (has requires) |
RDF.Indexed |
rho_df_closure_closed |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, graph_len, rho_df_closure, rho_df_closure_step, rho_df_closure_step_pre_dedup |
ig_wf_sp, no_dup_keys, rho_df_closed, rho_df_frag_graph |
no (has requires) |
RDF.Indexed |
rho_df_closure_decides |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, graph_len, rho_df_closure, rho_df_closure_step, rho_df_closure_step_pre_dedup |
graph_tt_free, ig_wf_sp, no_dup_keys, rho_df_entails, rho_df_frag_graph, simple_entailment_spec |
no (has requires) |
RDF.Indexed |
lemma_build_indexed_wf_sp |
RDF.Indexed.KeyInjectivity |
build_indexed |
graph_sp_sep_free, ig_wf_sp |
no (has requires) |
RDF.Indexed |
theorem_wf_sp_nonempty_instance |
RDF.Indexed.KeyInjectivity |
build_indexed |
ig_wf_sp |
yes |
RDF.Indexed |
lemma_build_indexed_wf_subj |
RDF.Indexed.KeyInjectivity |
build_indexed |
ig_wf_subj |
yes |
RDF.Indexed |
lemma_build_indexed_wf_obj |
RDF.Indexed.KeyInjectivity |
build_indexed |
ig_wf_obj |
yes |
RDF.Indexed |
lemma_build_indexed_wf_po |
RDF.Indexed.KeyInjectivity |
build_indexed |
graph_po_sep_free, ig_wf_po |
no (has requires) |
RDF.Indexed |
theorem_ig_wf_pred_witness |
RDF.Semantics.HypothesisWitness |
bucket_lookup |
ig_wf_pred |
yes |
RDF.Indexed |
theorem_ig_wf_sp_satisfiable_degenerately |
RDF.Semantics.HypothesisWitness |
bucket_lookup, sp_key |
ig_wf_sp |
yes |
RDF.Indexed |
lemma_ig_wf_sp_of_empty |
RDF.Semantics.HypothesisWitness |
build_indexed |
ig_wf_sp |
yes |
RDF.Indexed |
theorem_closure_chain_wf_n0_of_empty |
RDF.Semantics.HypothesisWitness |
build_indexed |
ig_wf_sp |
yes |
RDF.List.Helpers |
lemma_assoc_tr_congr |
SPARQL11.Algebra.Refinement |
assoc_tr |
smap_eq |
no (has requires) |
RDF.Term |
lemma_find_subjects_indexed_wf_approx |
OWL.RL.Refinement |
find_subjects_indexed, rdf_term_eq |
ig_wf_po, ig_wf_pred |
no (has requires) |
RDF.Term |
lemma_literal_eq_exact |
RDF.Entailment.Simple.Refinement |
literal_eq |
lit_exact |
no (has requires) |
RDF.Term |
lemma_rdf_term_eq_exact_identity |
RDF.Entailment.Simple.Refinement |
rdf_term_eq |
term_exact |
no (has requires) |
RDF.Vocabulary.Axioms |
lemma_selfloop_not_in_herbrand |
RDF.Entailment.RDFS.Completeness |
i_rdfs_subClassOf |
herb_iext |
no (has requires) |
RDF.Vocabulary.Axioms |
lemma_graph_clean_satisfiable |
RDF.Entailment.RDFS.RhoDFClosure |
i_rdf_type, i_rdfs_Class, i_rdfs_Resource |
graph_clean |
yes |
RDF.Vocabulary.Axioms |
rdfs_rule_subClassOf_reaches_iri2 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, i_rdf_type, i_rdfs_subClassOf, rdfs_rule_subClassOf |
ig_wf_sp, is_subgraph, rho_df_frag_graph |
no (has requires) |
RDF.Vocabulary.Axioms |
rdfs_rule_subClassOf_reaches_iri |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, i_rdf_type, i_rdfs_subClassOf, rdfs_rule_subClassOf |
ig_wf_sp, rho_df_frag_graph |
no (has requires) |
RDF.Vocabulary.Axioms |
lemma_f1_bad_triple_derived |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, f1_bad_triple, f1_witness, i_rdfs_subPropertyOf, rdfs_rule_subPropertyOf |
ig_wf_sp |
no (has requires) |
RDF.Vocabulary.Axioms |
rho_df_frag_preservation_fails |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, f1_bad_triple, f1_witness, i_rdfs_subPropertyOf, rdfs_rule_subPropertyOf |
ig_wf_sp, rho_df_frag_graph, rho_df_frag_triple |
no (has requires) |
RDF.Vocabulary.Axioms |
lemma_vocab_sep_free |
RDF.Entailment.RDFS.SepFree |
i_rdf_Property, i_rdf_type, i_rdfs_Class, i_rdfs_ContainerMembershipProperty, i_rdfs_Datatype, i_rdfs_Literal, i_rdfs_Resource, i_rdfs_domain, i_rdfs_member, i_rdfs_range, i_rdfs_subClassOf, i_rdfs_subPropertyOf |
str_sep_free |
yes |
RDF.Vocabulary.Axioms |
lemma_axiomatic_tables_sep_free |
RDF.Entailment.RDFS.SepFree |
container_membership_properties, rdf_axiomatic_triples, rdfs_axiomatic_triples |
str_sep_free, triple_sep_free |
yes |
RDFS.Closure |
lemma_scm_eqc2_emission_licensed |
OWL.RL.Refinement |
find_objects_indexed, owl_equivalentClass, rdfs_subClassOf, term_is_iri |
ig_wf_sp, scm_eqc2_derives |
no (has requires) |
RDFS.Closure |
lemma_scm_eqp2_emission_licensed |
OWL.RL.Refinement |
find_objects_indexed, owl_equivalentProperty, rdfs_subPropertyOf, term_is_iri |
ig_wf_sp, scm_eqp2_derives |
no (has requires) |
RDFS.Closure |
lemma_cls_hv1_row_intro |
OWL.RL.Refinement |
find_subjects_indexed, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cls_hv1_derives, ig_wf_po |
no (has requires) |
RDFS.Closure |
lemma_cls_hv1_members_fold |
OWL.RL.Refinement |
find_subjects_indexed, owl_cls_hv1_emit, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cls_hv1_licensed, ig_wf_po |
no (has requires) |
RDFS.Closure |
lemma_cls_avf_row_intro |
OWL.RL.Refinement |
find_objects_indexed, find_subjects_indexed, owl_allValuesFrom_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cls_avf_derives, ig_wf_po, ig_wf_sp |
no (has requires) |
RDFS.Closure |
lemma_cls_avf_member_step |
OWL.RL.Refinement |
find_subjects_indexed, owl_allValuesFrom_iri, owl_cls_avf1_member, owl_onProperty_iri, rdf_type, subject_to_term |
cls_avf_licensed, ig_wf_po, ig_wf_sp |
no (has requires) |
RDFS.Closure |
rdfs_rule_domain_sound |
OWL.Semantics.Soundness |
rdfs_rule_domain |
cond_domain, holds_all, ig_wf_pred |
no (has requires) |
RDFS.Closure |
rdfs_rule_range_sound |
OWL.Semantics.Soundness |
rdfs_rule_range |
cond_range, holds_all, ig_wf_pred |
no (has requires) |
RDFS.Closure |
lemma_cls_hv1_witness_holds |
OWL.Semantics.Soundness |
find_subjects_indexed, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cond_hasvalue, holds_all, ig_wf_po, triple_holds |
no (has requires) |
RDFS.Closure |
lemma_cls_hv1_members_fold_sound |
OWL.Semantics.Soundness |
find_subjects_indexed, owl_cls_hv1_emit, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cond_hasvalue, holds_all, ig_wf_po |
no (has requires) |
RDFS.Closure |
lemma_cls_hv2_witness_holds |
OWL.Semantics.Soundness |
find_subjects_indexed, owl_hasValue_iri, owl_onProperty_iri, rdf_type, subject_to_term |
cond_hasvalue, cond_literal_term_eq_respecting, holds_all, ig_wf_po, ig_wf_pred, triple_holds |
no (has requires) |
RDFS.Closure |
lemma_cls_avf_witness_holds |
OWL.Semantics.Soundness |
find_objects_indexed, find_subjects_indexed, owl_allValuesFrom_iri, owl_onProperty_iri, rdf_type, subject_to_term, term_to_subject |
cond_allvaluesfrom, holds_all, ig_wf_po, ig_wf_sp, triple_holds |
no (has requires) |
RDFS.Closure |
lemma_cls_avf_member_fold_sound |
OWL.Semantics.Soundness |
find_objects_indexed, find_subjects_indexed, owl_allValuesFrom_iri, owl_cls_avf1_emit, owl_onProperty_iri, rdf_type, subject_to_term |
cond_allvaluesfrom, holds_all, ig_wf_po, ig_wf_sp |
no (has requires) |
RDFS.Closure |
rdfs_rule_domain_entailed |
OWL.Semantics.Soundness |
build_indexed, rdfs_rule_domain |
pilot_entails |
yes |
RDFS.Closure |
rdfs_rule_range_entailed |
OWL.Semantics.Soundness |
build_indexed, rdfs_rule_range |
pilot_entails |
yes |
RDFS.Closure |
rdfs_rule_subPropertyOf_preserves_sep |
RDF.Entailment.RDFS.ChainWf |
rdfs_rule_subPropertyOf |
graph_sep_free, ig_wf_pred |
no (has requires) |
RDFS.Closure |
rdfs_rule_domain_preserves_sep |
RDF.Entailment.RDFS.ChainWf |
rdfs_rule_domain |
graph_sep_free, ig_wf_pred |
no (has requires) |
RDFS.Closure |
rdfs_rule_range_preserves_sep |
RDF.Entailment.RDFS.ChainWf |
rdfs_rule_range |
graph_sep_free, ig_wf_pred |
no (has requires) |
RDFS.Closure |
rdfs_rule_subClassOf_preserves_sep |
RDF.Entailment.RDFS.ChainWf |
rdfs_rule_subClassOf |
graph_sep_free, ig_wf_sp |
no (has requires) |
RDFS.Closure |
rdfs_rule_container_membership_preserves_sep |
RDF.Entailment.RDFS.ChainWf |
rdfs_rule_container_membership |
graph_sep_free |
no (has requires) |
RDFS.Closure |
rdfs_rule_subClassOf_trans_preserves_sep |
RDF.Entailment.RDFS.ChainWf |
rdfs_rule_subClassOf_trans |
graph_sep_free, ig_wf_sp |
no (has requires) |
RDFS.Closure |
rdfs_rule_subPropertyOf_trans_preserves_sep |
RDF.Entailment.RDFS.ChainWf |
rdfs_rule_subPropertyOf_trans |
graph_sep_free, ig_wf_sp |
no (has requires) |
RDFS.Closure |
rdfs_rule_recognized_datatypes_preserves_sep |
RDF.Entailment.RDFS.ChainWf |
rdfs_rule_recognized_datatypes |
graph_sep_free |
no (has requires) |
RDFS.Closure |
rdfs_rule_class_subclass_resource_preserves_sep |
RDF.Entailment.RDFS.ChainWf |
rdfs_rule_class_subclass_resource |
graph_sep_free |
no (has requires) |
RDFS.Closure |
rdfs_rule_datatype_subclass_literal_preserves_sep |
RDF.Entailment.RDFS.ChainWf |
rdfs_rule_datatype_subclass_literal |
graph_sep_free |
no (has requires) |
RDFS.Closure |
rdfs_rule_resource_subject_preserves_sep |
RDF.Entailment.RDFS.ChainWf |
rdfs_rule_resource_subject |
graph_sep_free |
no (has requires) |
RDFS.Closure |
rdfs_rule_resource_object_preserves_sep |
RDF.Entailment.RDFS.ChainWf |
rdfs_rule_resource_object |
graph_sep_free |
no (has requires) |
RDFS.Closure |
step_preserves_sep_free |
RDF.Entailment.RDFS.ChainWf |
rdfs_closure_step |
graph_sep_free |
no (has requires) |
RDFS.Closure |
step_domain |
RDF.Entailment.RDFS.Completeness |
rdf_type, rdfs_domain |
herb_iext, rho_df_closed |
no (has requires) |
RDFS.Closure |
step_range |
RDF.Entailment.RDFS.Completeness |
rdf_type, rdfs_range |
herb_iext, rho_df_closed, rho_df_frag_graph |
no (has requires) |
RDFS.Closure |
step_sub_property |
RDF.Entailment.RDFS.Completeness |
rdfs_subPropertyOf |
herb_iext, rho_df_closed, rho_df_frag_graph |
no (has requires) |
RDFS.Closure |
step_sub_property_trans |
RDF.Entailment.RDFS.Completeness |
rdfs_subPropertyOf |
herb_iext, rho_df_closed |
no (has requires) |
RDFS.Closure |
step_sub_class |
RDF.Entailment.RDFS.Completeness |
rdf_type, rdfs_subClassOf |
herb_iext, rho_df_closed |
no (has requires) |
RDFS.Closure |
step_sub_class_trans |
RDF.Entailment.RDFS.Completeness |
rdfs_subClassOf |
herb_iext, rho_df_closed |
no (has requires) |
RDFS.Closure |
rdfs_closure_rho_df_complete |
RDF.Entailment.RDFS.Completeness |
rdfs_closure |
graph_tt_free, is_subgraph, rho_df_closed, rho_df_entails, rho_df_frag_graph, simple_entailment_spec |
no (has requires) |
RDFS.Closure |
lemma_rdfs_rule_subPropertyOf_clean |
RDF.Entailment.RDFS.FixedPoint |
build_indexed, rdfs_rule_subPropertyOf |
graph_clean |
no (has requires) |
RDFS.Closure |
lemma_rdfs_rule_domain_clean |
RDF.Entailment.RDFS.FixedPoint |
build_indexed, rdfs_rule_domain |
graph_clean |
no (has requires) |
RDFS.Closure |
lemma_rdfs_rule_range_clean |
RDF.Entailment.RDFS.FixedPoint |
build_indexed, rdfs_rule_range |
graph_clean |
no (has requires) |
RDFS.Closure |
lemma_rdfs_rule_subClassOf_clean |
RDF.Entailment.RDFS.FixedPoint |
build_indexed, rdfs_rule_subClassOf |
graph_clean |
no (has requires) |
RDFS.Closure |
lemma_rdfs_rule_container_membership_clean |
RDF.Entailment.RDFS.FixedPoint |
rdfs_rule_container_membership |
graph_clean |
no (has requires) |
RDFS.Closure |
lemma_rdfs_rule_subClassOf_trans_clean |
RDF.Entailment.RDFS.FixedPoint |
build_indexed, rdfs_rule_subClassOf_trans |
graph_clean |
no (has requires) |
RDFS.Closure |
lemma_rdfs_rule_subPropertyOf_trans_clean |
RDF.Entailment.RDFS.FixedPoint |
build_indexed, rdfs_rule_subPropertyOf_trans |
graph_clean |
no (has requires) |
RDFS.Closure |
lemma_rdfs_rule_recognized_datatypes_clean |
RDF.Entailment.RDFS.FixedPoint |
rdfs_rule_recognized_datatypes |
graph_clean |
no (has requires) |
RDFS.Closure |
lemma_rdfs_rule_class_subclass_resource_clean |
RDF.Entailment.RDFS.FixedPoint |
rdfs_rule_class_subclass_resource |
graph_clean |
no (has requires) |
RDFS.Closure |
lemma_rdfs_rule_datatype_subclass_literal_clean |
RDF.Entailment.RDFS.FixedPoint |
rdfs_rule_datatype_subclass_literal |
graph_clean |
no (has requires) |
RDFS.Closure |
lemma_rdfs_rule_resource_subject_clean |
RDF.Entailment.RDFS.FixedPoint |
rdfs_rule_resource_subject |
graph_clean |
no (has requires) |
RDFS.Closure |
lemma_rdfs_rule_resource_object_clean |
RDF.Entailment.RDFS.FixedPoint |
rdfs_rule_resource_object |
graph_clean |
no (has requires) |
RDFS.Closure |
lemma_len_eq_saturated_sep_free |
RDF.Entailment.RDFS.FixedPoint |
graph_len, rdfs_closure_step |
graph_obj_not_tt, graph_sep_free, step_saturated |
no (has requires) |
RDFS.Closure |
rdfs_rule_subPropertyOf_preserves |
RDF.Entailment.RDFS.ModelTheory |
rdfs_rule_subPropertyOf |
cond_subPropertyOf, holds_all, ig_wf_pred |
no (has requires) |
RDFS.Closure |
rdfs_rule_domain_preserves |
RDF.Entailment.RDFS.ModelTheory |
rdfs_rule_domain |
cond_domain, holds_all, ig_wf_pred |
no (has requires) |
RDFS.Closure |
rdfs_rule_range_preserves |
RDF.Entailment.RDFS.ModelTheory |
rdfs_rule_range |
cond_range, holds_all, ig_wf_pred |
no (has requires) |
RDFS.Closure |
rdfs_rule_subClassOf_preserves |
RDF.Entailment.RDFS.ModelTheory |
rdfs_rule_subClassOf |
cond_subClassOf, holds_all, ig_wf_sp |
no (has requires) |
RDFS.Closure |
rdfs_rule_subClassOf_trans_preserves |
RDF.Entailment.RDFS.ModelTheory |
rdfs_rule_subClassOf_trans |
cond_subClassOf_trans, holds_all, ig_wf_sp |
no (has requires) |
RDFS.Closure |
rdfs_rule_subPropertyOf_trans_preserves |
RDF.Entailment.RDFS.ModelTheory |
rdfs_rule_subPropertyOf_trans |
cond_subPropertyOf_trans, holds_all, ig_wf_sp |
no (has requires) |
RDFS.Closure |
rdfs_rule_container_membership_preserves |
RDF.Entailment.RDFS.ModelTheory |
rdfs_rule_container_membership |
cond_cmp_member, cond_rdfs_axioms, holds_all |
no (has requires) |
RDFS.Closure |
rdfs_rule_recognized_datatypes_preserves |
RDF.Entailment.RDFS.ModelTheory |
rdfs_rule_recognized_datatypes |
cond_datatypes_minimal, holds_all |
no (has requires) |
RDFS.Closure |
rdfs_rule_resource_subject_preserves |
RDF.Entailment.RDFS.ModelTheory |
rdfs_rule_resource_subject |
cond_resource, holds_all |
no (has requires) |
RDFS.Closure |
rdfs_rule_resource_object_preserves |
RDF.Entailment.RDFS.ModelTheory |
rdfs_rule_resource_object |
cond_resource, holds_all |
no (has requires) |
RDFS.Closure |
rdfs_rule_class_subclass_resource_preserves |
RDF.Entailment.RDFS.ModelTheory |
rdfs_rule_class_subclass_resource |
cond_class_subclass_resource, holds_all |
no (has requires) |
RDFS.Closure |
rdfs_rule_datatype_subclass_literal_preserves |
RDF.Entailment.RDFS.ModelTheory |
rdfs_rule_datatype_subclass_literal |
cond_datatype_subclass_literal, holds_all |
no (has requires) |
RDFS.Closure |
rdfs_closure_step_sound |
RDF.Entailment.RDFS.ModelTheory |
build_indexed, rdfs_closure_step |
holds_all, ig_wf_sp, rdfs_conditions |
no (has requires) |
RDFS.Closure |
rdfs_closure_sound |
RDF.Entailment.RDFS.ModelTheory |
rdfs_closure |
closure_chain_wf, holds_all, rdfs_conditions |
no (has requires) |
RDFS.Closure |
rdfs_reflexivity_axioms_preserves |
RDF.Entailment.RDFS.ModelTheory |
rdfs_reflexivity_axioms |
holds_all, rdfs_conditions |
no (has requires) |
RDFS.Closure |
rdfs_closure_with_reflexivity_sound |
RDF.Entailment.RDFS.ModelTheory |
rdfs_closure_with_reflexivity |
closure_chain_wf, holds_all, rdfs_conditions |
no (has requires) |
RDFS.Closure |
reflexivity_needs_rdfs_Class |
RDF.Entailment.RDFS.ModelTheory |
rdfs_Class, rdfs_subClassOf |
cond_subClassOf_refl, icext |
no (has requires) |
RDFS.Closure |
rdf_property_axiom_closure_licensed |
RDF.Entailment.RDFS.Refinement |
rdf_property_axiom_closure |
rdfD2_derives |
yes |
RDFS.Closure |
rdfs_rule_domain_licensed |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_domain |
ig_wf_pred, licensed_by2, rdfs2_derives |
no (has requires) |
RDFS.Closure |
rdfs_rule_range_licensed |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_range |
ig_wf_pred, licensed_by2, rdfs3_derives |
no (has requires) |
RDFS.Closure |
rdfs_rule_subPropertyOf_licensed |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_subPropertyOf |
ig_wf_pred, licensed_by2, rdfs7_derives |
no (has requires) |
RDFS.Closure |
rdfs_rule_subClassOf_licensed |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_subClassOf |
ig_wf_sp, licensed_by2, rdfs9_derives2 |
no (has requires) |
RDFS.Closure |
rdfs_rule_subClassOf_trans_licensed |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_subClassOf_trans |
ig_wf_sp, licensed_by2, rdfs11_derives2 |
no (has requires) |
RDFS.Closure |
rdfs_rule_subPropertyOf_trans_licensed |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_subPropertyOf_trans |
ig_wf_sp, licensed_by2, rdfs5_derives2 |
no (has requires) |
RDFS.Closure |
lemma_rdf_member_iris |
RDF.Entailment.RDFS.Refinement |
rdf_1, rdf_2, rdf_3, rdf_4, rdf_5 |
is_rdf_member_iri |
yes |
RDFS.Closure |
rdfs_rule_container_membership_licensed |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_container_membership |
rdfs_axiomatic, rdfs_member_subproperty |
yes |
RDFS.Closure |
rdfs_rule_recognized_datatypes_licensed |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_recognized_datatypes |
rdfs1_derives |
yes |
RDFS.Closure |
rdfs_rule_resource_subject_licensed |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_resource_subject |
licensed_by, rdfs4a_derives |
yes |
RDFS.Closure |
rdfs_rule_resource_object_licensed |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_resource_object |
licensed_by, rdfs4b_derives |
yes |
RDFS.Closure |
rdfs_rule_class_subclass_resource_licensed |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_class_subclass_resource |
licensed_by, rdfs8_derives |
yes |
RDFS.Closure |
rdfs_rule_datatype_subclass_literal_licensed |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_datatype_subclass_literal |
licensed_by, rdfs13_derives |
yes |
RDFS.Closure |
lemma_snapshot_carries_elim |
RDF.Entailment.RDFS.Refinement |
snapshot_carries |
ig_wf_sp |
no (has requires) |
RDFS.Closure |
lemma_emit_once |
RDF.Entailment.RDFS.Refinement |
emit_once |
ig_wf_sp, snapshot_subset |
no (has requires) |
RDFS.Closure |
lemma_emit_once_all |
RDF.Entailment.RDFS.Refinement |
emit_once |
ig_wf_sp, snapshot_subset |
no (has requires) |
RDFS.Closure |
rdfs_rule_recognized_datatypes_complete |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_recognized_datatypes, recognized_datatypes |
ig_wf_sp, snapshot_subset |
no (has requires) |
RDFS.Closure |
rdfs_rule_resource_subject_complete |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_resource_subject |
ig_wf_sp, snapshot_subset |
no (has requires) |
RDFS.Closure |
rdfs_rule_resource_object_complete |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_resource_object |
ig_wf_sp, snapshot_subset |
no (has requires) |
RDFS.Closure |
rdfs_rule_class_subclass_resource_complete |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_class_subclass_resource |
ig_wf_sp, snapshot_subset |
no (has requires) |
RDFS.Closure |
rdfs_rule_datatype_subclass_literal_complete |
RDF.Entailment.RDFS.Refinement |
rdfs_rule_datatype_subclass_literal |
ig_wf_sp, snapshot_subset |
no (has requires) |
RDFS.Closure |
rs2_rows_complete_at_build_indexed |
RDF.Entailment.RDFS.Refinement |
build_indexed, is_typed_as, rdf_type, rdfs_Class, rdfs_Datatype, rdfs_Literal, rdfs_Resource, rdfs_rule_class_subclass_resource, rdfs_rule_datatype_subclass_literal, rdfs_rule_recognized_datatypes, rdfs_rule_resource_object, rdfs_rule_resource_subject, rdfs_subClassOf, recognized_datatypes, term_to_subject |
ig_wf_sp |
no (has requires) |
RDFS.Closure |
lemma_class_refl_licensed |
RDF.Entailment.RDFS.Refinement |
is_class_type_object_rdfs, rdfs_subClassOf |
harvest_source, rdfs_licensed |
no (has requires) |
RDFS.Closure |
lemma_property_refl_licensed |
RDF.Entailment.RDFS.Refinement |
is_property_type_object_rdfs, rdfs_subPropertyOf |
harvest_source, rdfs_licensed |
no (has requires) |
RDFS.Closure |
rdfs_reflexivity_axioms_licensed |
RDF.Entailment.RDFS.Refinement |
rdfs_reflexivity_axioms |
rdfs_licensed |
yes |
RDFS.Closure |
owl_reflexivity_axioms_not_rdfs_sound |
RDF.Entailment.RDFS.Refinement |
owl_reflexivity_axioms |
rdfs_licensed |
yes |
RDFS.Closure |
lemma_emit_once_term_reaches |
RDF.Entailment.RDFS.RhoDFClosure |
emit_once_term |
ig_wf_sp, rho_df_frag_graph, rho_df_object_ok, snapshot_subset |
no (has requires) |
RDFS.Closure |
rdfs_rule_domain_reaches2 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_domain |
ig_wf_sp, is_subgraph, rdfs2_derives, rho_df_frag_graph |
no (has requires) |
RDFS.Closure |
rdfs_rule_domain_reaches |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_domain |
ig_wf_sp, rdfs2_derives, rho_df_frag_graph |
no (has requires) |
RDFS.Closure |
rdfs_rule_range_reaches2 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_range |
ig_wf_sp, is_subgraph, rdfs3_derives, rho_df_frag_graph |
no (has requires) |
RDFS.Closure |
rdfs_rule_range_reaches |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_range |
ig_wf_sp, rdfs3_derives, rho_df_frag_graph |
no (has requires) |
RDFS.Closure |
rdfs_rule_subPropertyOf_reaches2 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_subPropertyOf |
ig_wf_sp, is_subgraph, rdfs7_derives, rho_df_frag_graph |
no (has requires) |
RDFS.Closure |
rdfs_rule_subPropertyOf_reaches |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_subPropertyOf |
ig_wf_sp, rdfs7_derives, rho_df_frag_graph |
no (has requires) |
RDFS.Closure |
rdfs_rule_subClassOf_trans_reaches2 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_subClassOf_trans |
ig_wf_sp, is_subgraph, rdfs11_derives |
no (has requires) |
RDFS.Closure |
rdfs_rule_subClassOf_trans_reaches |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_subClassOf_trans |
ig_wf_sp, rdfs11_derives |
no (has requires) |
RDFS.Closure |
rdfs_rule_subPropertyOf_trans_reaches2 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_subPropertyOf_trans |
ig_wf_sp, is_subgraph, rdfs5_derives |
no (has requires) |
RDFS.Closure |
rdfs_rule_subPropertyOf_trans_reaches |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_subPropertyOf_trans |
ig_wf_sp, rdfs5_derives |
no (has requires) |
RDFS.Closure |
rdfs_rule_subClassOf_reaches_iri2 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, i_rdf_type, i_rdfs_subClassOf, rdfs_rule_subClassOf |
ig_wf_sp, is_subgraph, rho_df_frag_graph |
no (has requires) |
RDFS.Closure |
rdfs_rule_subClassOf_reaches_iri |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, i_rdf_type, i_rdfs_subClassOf, rdfs_rule_subClassOf |
ig_wf_sp, rho_df_frag_graph |
no (has requires) |
RDFS.Closure |
lemma_f1_bad_triple_derived |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, f1_bad_triple, f1_witness, i_rdfs_subPropertyOf, rdfs_rule_subPropertyOf |
ig_wf_sp |
no (has requires) |
RDFS.Closure |
rho_df_frag_preservation_fails |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, f1_bad_triple, f1_witness, i_rdfs_subPropertyOf, rdfs_rule_subPropertyOf |
ig_wf_sp, rho_df_frag_graph, rho_df_frag_triple |
no (has requires) |
RDFS.Closure |
lemma_c_in_g1 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_subPropertyOf |
is_subgraph |
no (has requires) |
RDFS.Closure |
lemma_c_in_g2 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_domain, rdfs_rule_subPropertyOf |
is_subgraph |
no (has requires) |
RDFS.Closure |
lemma_c_in_g3 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_domain, rdfs_rule_range, rdfs_rule_subPropertyOf |
is_subgraph |
no (has requires) |
RDFS.Closure |
lemma_c_in_g4 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_domain, rdfs_rule_range, rdfs_rule_subClassOf, rdfs_rule_subPropertyOf |
is_subgraph |
no (has requires) |
RDFS.Closure |
lemma_c_in_g5 |
RDF.Entailment.RDFS.RhoDFClosure |
build_indexed, rdfs_rule_domain, rdfs_rule_range, rdfs_rule_subClassOf, rdfs_rule_subClassOf_trans, rdfs_rule_subPropertyOf |
is_subgraph |
no (has requires) |
RDFS.Closure |
lemma_axiomatic_tables_sep_free |
RDF.Entailment.RDFS.SepFree |
container_membership_properties, rdf_axiomatic_triples, rdfs_axiomatic_triples |
str_sep_free, triple_sep_free |
yes |
SPARQL11.Algebra |
theorem_tp_match_instantiates_ext |
SPARQL11.Algebra.BGPRefinement |
instantiate_tp, tp_match |
binding_extends, ptrm_exact, smap_exact, term_exact |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_sound_fuel |
SPARQL11.Algebra.BGPRefinement |
eval_bgp_store_from_mu_fuel, graph_to_store |
bgp_frag, bgp_subgraph_clause, binding_extends, graph_frag, smap_exact |
no (has requires) |
SPARQL11.Algebra |
lemma_bgp_sol_spec_from_subgraph_clause |
SPARQL11.Algebra.BGPRefinement |
instantiate_tp |
bgp_sol_spec, bgp_subgraph_clause |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_store_sound_fuel |
SPARQL11.Algebra.BGPRefinement |
eval_bgp_store_from_mu_fuel |
bgp_frag, bgp_subgraph_clause, binding_extends, graph_frag, smap_exact, store_search_sound |
no (has requires) |
SPARQL11.Algebra |
lemma_term_exact_subject |
SPARQL11.Algebra.BGPRefinement |
subject_to_term |
term_exact |
yes |
SPARQL11.Algebra |
lemma_bound_subject_mono |
SPARQL11.Algebra.BGPRefinement |
bound_subject_of_pattern |
binding_extends |
no (has requires) |
SPARQL11.Algebra |
lemma_bound_predicate_mono |
SPARQL11.Algebra.BGPRefinement |
bound_predicate_of_pattern |
binding_extends |
no (has requires) |
SPARQL11.Algebra |
lemma_bound_object_mono |
SPARQL11.Algebra.BGPRefinement |
bound_object_of_pattern |
binding_extends |
no (has requires) |
SPARQL11.Algebra |
lemma_bound_object_exact |
SPARQL11.Algebra.BGPRefinement |
bound_object_of_pattern |
ptrm_exact, smap_exact, term_exact |
no (has requires) |
SPARQL11.Algebra |
lemma_sm_bind_extends |
SPARQL11.Algebra.BGPRefinement |
sm_bind |
binding_extends |
no (has requires) |
SPARQL11.Algebra |
lemma_sm_bind_under |
SPARQL11.Algebra.BGPRefinement |
sm_bind |
binding_extends |
no (has requires) |
SPARQL11.Algebra |
lemma_try_bind_subject_complete |
SPARQL11.Algebra.BGPRefinement |
bound_subject_of_pattern, try_bind_subject |
binding_extends, smap_exact |
no (has requires) |
SPARQL11.Algebra |
lemma_try_bind_term_complete |
SPARQL11.Algebra.BGPRefinement |
bound_object_of_pattern, try_bind_term |
binding_extends, smap_exact, term_exact |
no (has requires) |
SPARQL11.Algebra |
lemma_tp_match_complete |
SPARQL11.Algebra.BGPRefinement |
instantiate_tp, tp_match |
binding_extends, smap_exact, term_exact |
no (has requires) |
SPARQL11.Algebra |
lemma_bound_holds_of_instantiate |
SPARQL11.Algebra.BGPRefinement |
instantiate_tp |
binding_extends |
no (has requires) |
SPARQL11.Algebra |
lemma_eval_single_tp_complete_at |
SPARQL11.Algebra.BGPRefinement |
instantiate_tp |
binding_extends, graph_frag, single_tp_goal, smap_exact, store_search_complete, tp_frag |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_store_complete |
SPARQL11.Algebra.BGPRefinement |
eval_bgp_store |
bgp_frag, bgp_subgraph_clause, binding_extends, graph_frag, smap_exact, store_search_complete |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_complete |
SPARQL11.Algebra.BGPRefinement |
eval_bgp |
bgp_frag, bgp_subgraph_clause, binding_extends, graph_frag, smap_exact |
no (has requires) |
SPARQL11.Algebra |
lemma_instantiate_tp_mono |
SPARQL11.Algebra.BGPRefinement |
instantiate_tp |
binding_extends |
no (has requires) |
SPARQL11.Algebra |
lemma_instantiate_bgp_agree |
SPARQL11.Algebra.BGPRefinement |
instantiate_bgp, instantiate_tp |
binding_extends |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_full_spec |
SPARQL11.Algebra.BGPRefinement |
eval_bgp, instantiate_tp, tp_vars |
bgp_frag, bgp_sol_spec, graph_frag |
no (has requires) |
SPARQL11.Algebra |
theorem_sm_compatible_sound |
SPARQL11.Algebra.Refinement |
sm_compatible |
compatible_spec, smap_exact |
no (has requires) |
SPARQL11.Algebra |
theorem_sm_compatible_complete |
SPARQL11.Algebra.Refinement |
sm_compatible |
compatible_spec |
no (has requires) |
SPARQL11.Algebra |
theorem_sm_merge_is_merge |
SPARQL11.Algebra.Refinement |
sm_merge |
is_merge |
yes |
SPARQL11.Algebra |
theorem_domains_disjoint_sound |
SPARQL11.Algebra.Refinement |
domains_disjoint |
dom_disjoint_spec |
no (has requires) |
SPARQL11.Algebra |
theorem_domains_disjoint_complete |
SPARQL11.Algebra.Refinement |
domains_disjoint |
dom_disjoint_spec |
no (has requires) |
SPARQL11.Algebra |
theorem_union_card |
SPARQL11.Algebra.Refinement |
union |
union_card_spec |
yes |
SPARQL11.Algebra |
theorem_union_sound |
SPARQL11.Algebra.Refinement |
union |
in_union_spec |
no (has requires) |
SPARQL11.Algebra |
lemma_sm_lookup_congr |
SPARQL11.Algebra.Refinement |
sm_lookup |
smap_eq |
no (has requires) |
SPARQL11.Algebra |
lemma_fx_ctx_get_congr |
SPARQL11.Algebra.Refinement |
fx_ctx_get |
smap_eq |
no (has requires) |
SPARQL11.Algebra |
lemma_eval_expr_congr |
SPARQL11.Algebra.Refinement |
eval_expr_with_base |
smap_eq |
no (has requires) |
SPARQL11.Algebra |
lemma_eval_coalesce_congr |
SPARQL11.Algebra.Refinement |
eval_coalesce_with_base |
smap_eq |
no (has requires) |
SPARQL11.Algebra |
lemma_eval_geof_args_congr |
SPARQL11.Algebra.Refinement |
eval_geof_args_with_base |
smap_eq |
no (has requires) |
SPARQL11.Algebra |
lemma_eval_in_congr |
SPARQL11.Algebra.Refinement |
eval_in_with_base |
smap_eq |
no (has requires) |
SPARQL11.Algebra |
lemma_eval_concat_congr |
SPARQL11.Algebra.Refinement |
eval_concat_with_base |
smap_eq |
no (has requires) |
SPARQL11.Algebra |
lemma_eval_expr_opt_congr |
SPARQL11.Algebra.Refinement |
eval_expr_with_base |
smap_eq |
no (has requires) |
SPARQL11.Algebra |
theorem_sr1_witness_now_card_conformant |
SPARQL11.Algebra.Refinement |
distinct_solutions |
distinct_card_spec |
yes |
SPARQL11.Algebra |
theorem_sm_equal_matches_smap_eq_on_witness |
SPARQL11.Algebra.Refinement |
sm_equal |
smap_eq |
yes |
SPARQL11.Algebra |
theorem_join_nested_loop_sound |
SPARQL11.Algebra.Refinement |
join_nested_loop |
in_join_spec, seq_exact |
no (has requires) |
SPARQL11.Algebra |
theorem_join_nested_loop_complete |
SPARQL11.Algebra.Refinement |
join_nested_loop |
compatible_spec, is_merge |
no (has requires) |
SPARQL11.Algebra |
theorem_project_is_proj |
SPARQL11.Algebra.Refinement |
project |
is_proj |
yes |
SPARQL11.Algebra |
theorem_project_solutions_sound |
SPARQL11.Algebra.Refinement |
project_solutions |
in_project_spec |
no (has requires) |
SPARQL11.Algebra |
theorem_project_card |
SPARQL11.Algebra.Refinement |
project_solutions |
project_card_spec |
yes |
SPARQL11.Algebra |
lemma_not_compatible_of_engine |
SPARQL11.Algebra.Refinement |
sm_compatible |
compatible_spec |
no (has requires) |
SPARQL11.Algebra |
theorem_minus_sound |
SPARQL11.Algebra.Refinement |
minus |
in_minus_spec |
no (has requires) |
SPARQL11.Algebra |
theorem_minus_complete |
SPARQL11.Algebra.Refinement |
minus |
compatible_spec, dom_disjoint_spec, smap_exact |
no (has requires) |
SPARQL11.Algebra |
theorem_left_join_empty_right |
SPARQL11.Algebra.Refinement |
eval_expr_ebv, left_join |
in_leftjoin_spec |
no (has requires) |
SPARQL11.Algebra |
theorem_sm_bind_is_extend |
SPARQL11.Algebra.Refinement |
sm_bind |
is_extend_at |
no (has requires) |
SPARQL11.Algebra |
theorem_sr3_distinct_card_spec_false |
SPARQL11.Algebra.Refinement |
distinct_solutions |
distinct_card_spec |
yes |
| Module | Theorem | Proved in | Shipping functions | Declarative relation | Unconditional |
|---|---|---|---|---|---|
OWL.Closure |
lemma_sameas_pairs_provenance |
OWL.RL.Refinement |
sameas_pairs |
pairs_licensed |
yes |
OWL.Closure |
owl_rule_sameAs_symmetry_licensed |
OWL.RL.Refinement |
owl_rule_sameAs_symmetry |
eq_sym_licensed |
yes |
OWL.Closure |
lemma_collect_nodes_provenance |
OWL.RL.Refinement |
collect_iri_or_bnode_terms |
nodes_licensed |
yes |
OWL.Closure |
owl_rule_sameAs_reflexivity_licensed |
OWL.RL.Refinement |
owl_rule_sameAs_reflexivity |
eq_ref_licensed |
yes |
OWL.Closure |
owl_rule_symmetric_property_licensed |
OWL.RL.Refinement |
owl_rule_symmetric_property |
prp_symp_licensed |
yes |
OWL.Closure |
owl_rule_equivalent_class_licensed |
OWL.RL.Refinement |
owl_rule_equivalent_class |
scm_eqc1_licensed |
yes |
OWL.Closure |
owl_rule_equivalent_property_licensed |
OWL.RL.Refinement |
owl_rule_equivalent_property |
scm_eqp1_licensed |
yes |
OWL.Closure |
owl_rule_inverse_of_licensed |
OWL.RL.Refinement |
owl_rule_inverse_of |
inv_licensed |
yes |
OWL.Closure |
lemma_no_disjoint_union_elim |
OWL.RL.Refinement |
owl_disjointUnionOf_iri |
no_disjoint_union |
no (has requires) |
OWL.Closure |
lemma_collect_haskey_axioms_licensed |
OWL.RL.Refinement |
collect_haskey_axioms |
haskey_axioms_licensed |
yes |
OWL.Closure |
lemma_members_of_class_licensed |
OWL.RL.Refinement |
members_of_class |
class_members_licensed |
yes |
Parser.FastString |
lemma_parse_nquads_acc_blank_step_shift |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
blank_line_wf |
no (has requires) |
Parser.FastString |
lemma_parse_nquads_acc_skip_blanks |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
blank_chain_wf |
no (has requires) |
Parser.FastString |
lemma_parse_nquads_acc_comment_step_shift |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
comment_line_wf |
no (has requires) |
Parser.FastString |
lemma_parse_nquads_acc_quad_fail_step_shift |
RDF.NQuads.Streaming |
fs_byte_at, fs_byte_length, parse_nquad, parse_nquads_acc |
quad_fail_line_wf |
no (has requires) |
Parser.FastString |
lemma_parse_nquads_acc_quad_ok_step_shift |
RDF.NQuads.Streaming |
dataset_add_quad, fs_byte_length, parse_iri, parse_nquad, parse_nquads_acc, parse_object, parse_opt_graph_label, parse_subject |
quad_ok_line_wf |
no (has requires) |
Parser.FastString |
lemma_parse_nquads_acc_line_step_shift |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
lw_wf |
no (has requires) |
Parser.FastString |
lemma_parse_nquads_acc_restart |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
chain_wf |
no (has requires) |
Parser.FastString |
lemma_parse_nquads_acc_full_via_chain |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
chain_wf |
no (has requires) |
Parser.FastString |
lemma_parse_nquads_acc_concat_line_general |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
chain_wf |
no (has requires) |
Parser.FastString |
theorem_stream_eq_batch_single_chunk_general |
RDF.NQuads.Streaming |
fs_byte_length |
chain_wf |
no (has requires) |
Parser.FastString |
stream_fold_eq_batch |
RDF.NQuads.Streaming |
dataset_finalise, fs_byte_length, parse_nquads_acc |
stream_fold_wf |
no (has requires) |
Parser.FastString |
lw_wf_shift_left_blank |
RDF.NQuads.Streaming |
fs_byte_length |
lw_wf |
no (has requires) |
Parser.FastString |
lw_wf_shift_left_comment |
RDF.NQuads.Streaming |
fs_byte_length |
lw_wf |
no (has requires) |
Parser.FastString |
lw_wf_shift_left_quadfail |
RDF.NQuads.Streaming |
fs_byte_length |
lw_wf |
no (has requires) |
Parser.FastString |
lw_wf_shift_left_quadok |
RDF.NQuads.Streaming |
fs_byte_length |
lw_wf |
no (has requires) |
Parser.FastString |
lw_wf_shift_left |
RDF.NQuads.Streaming |
fs_byte_length |
lw_wf |
no (has requires) |
Parser.FastString |
lw_ds_step_shift |
RDF.NQuads.Streaming |
fs_byte_length |
lw_wf |
no (has requires) |
Parser.FastString |
chain_wf_shift_left |
RDF.NQuads.Streaming |
fs_byte_length |
chain_wf |
no (has requires) |
Parser.FastString |
chain_ds_fold_shift |
RDF.NQuads.Streaming |
fs_byte_length |
chain_wf |
no (has requires) |
Parser.FastString |
chain_append |
RDF.NQuads.Streaming |
fs_byte_length |
chain_wf |
no (has requires) |
Parser.FastString |
stream_consume_dataset_fold_eq_batch |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
stream_fold_wf |
no (has requires) |
Parser.FastString |
stream_consume_dataset_eq_batch_raw |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
stream_fold_wf |
no (has requires) |
Parser.FastString |
lemma_fold_nquads_acc_blank_step_shift |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length |
blank_line_wf |
no (has requires) |
Parser.FastString |
lemma_fold_nquads_acc_comment_step_shift |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length |
comment_line_wf |
no (has requires) |
Parser.FastString |
lemma_fold_nquads_acc_quad_fail_step_shift |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_at, fs_byte_length, parse_nquad |
quad_fail_line_wf |
no (has requires) |
Parser.FastString |
lemma_fold_nquads_acc_quad_ok_step_shift |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length, parse_iri, parse_nquad, parse_object, parse_opt_graph_label, parse_subject |
quad_ok_line_wf |
no (has requires) |
Parser.FastString |
lemma_fold_nquads_acc_line_step_shift |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length |
lw_wf |
no (has requires) |
Parser.FastString |
lemma_fold_nquads_acc_restart |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length |
chain_wf |
no (has requires) |
Parser.FastString |
lemma_fold_nquads_acc_full_via_chain |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length |
chain_wf |
no (has requires) |
Parser.FastString |
fold_nquads_acc_concat_line_general |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length |
chain_wf |
no (has requires) |
Parser.FastString |
stream_consume_generic_fold_eq_batch |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length |
stream_fold_wf |
no (has requires) |
Parser.NQuads |
lemma_parse_nquads_acc_blank_step_shift |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
blank_line_wf |
no (has requires) |
Parser.NQuads |
lemma_parse_nquads_acc_skip_blanks |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
blank_chain_wf |
no (has requires) |
Parser.NQuads |
lemma_parse_nquads_acc_comment_step_shift |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
comment_line_wf |
no (has requires) |
Parser.NQuads |
lemma_parse_nquads_acc_quad_fail_step_shift |
RDF.NQuads.Streaming |
fs_byte_at, fs_byte_length, parse_nquad, parse_nquads_acc |
quad_fail_line_wf |
no (has requires) |
Parser.NQuads |
lemma_parse_nquads_acc_quad_ok_step_shift |
RDF.NQuads.Streaming |
dataset_add_quad, fs_byte_length, parse_iri, parse_nquad, parse_nquads_acc, parse_object, parse_opt_graph_label, parse_subject |
quad_ok_line_wf |
no (has requires) |
Parser.NQuads |
lemma_parse_nquads_acc_line_step_shift |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
lw_wf |
no (has requires) |
Parser.NQuads |
lemma_parse_nquads_acc_restart |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
chain_wf |
no (has requires) |
Parser.NQuads |
lemma_parse_nquads_acc_full_via_chain |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
chain_wf |
no (has requires) |
Parser.NQuads |
lemma_parse_nquads_acc_concat_line_general |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
chain_wf |
no (has requires) |
Parser.NQuads |
stream_fold_eq_batch |
RDF.NQuads.Streaming |
dataset_finalise, fs_byte_length, parse_nquads_acc |
stream_fold_wf |
no (has requires) |
Parser.NQuads |
stream_consume_dataset_fold_eq_batch |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
stream_fold_wf |
no (has requires) |
Parser.NQuads |
stream_consume_dataset_eq_batch_raw |
RDF.NQuads.Streaming |
fs_byte_length, parse_nquads_acc |
stream_fold_wf |
no (has requires) |
Parser.NQuads |
lemma_fold_nquads_acc_blank_step_shift |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length |
blank_line_wf |
no (has requires) |
Parser.NQuads |
lemma_fold_nquads_acc_comment_step_shift |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length |
comment_line_wf |
no (has requires) |
Parser.NQuads |
lemma_fold_nquads_acc_quad_fail_step_shift |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_at, fs_byte_length, parse_nquad |
quad_fail_line_wf |
no (has requires) |
Parser.NQuads |
lemma_fold_nquads_acc_quad_ok_step_shift |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length, parse_iri, parse_nquad, parse_object, parse_opt_graph_label, parse_subject |
quad_ok_line_wf |
no (has requires) |
Parser.NQuads |
lemma_fold_nquads_acc_line_step_shift |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length |
lw_wf |
no (has requires) |
Parser.NQuads |
lemma_fold_nquads_acc_restart |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length |
chain_wf |
no (has requires) |
Parser.NQuads |
lemma_fold_nquads_acc_full_via_chain |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length |
chain_wf |
no (has requires) |
Parser.NQuads |
fold_nquads_acc_concat_line_general |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length |
chain_wf |
no (has requires) |
Parser.NQuads |
stream_consume_generic_fold_eq_batch |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length |
stream_fold_wf |
no (has requires) |
Parser.NTriples |
lemma_parse_nquads_acc_quad_ok_step_shift |
RDF.NQuads.Streaming |
dataset_add_quad, fs_byte_length, parse_iri, parse_nquad, parse_nquads_acc, parse_object, parse_opt_graph_label, parse_subject |
quad_ok_line_wf |
no (has requires) |
Parser.NTriples |
lemma_fold_nquads_acc_quad_ok_step_shift |
RDF.NQuads.Streaming |
fold_nquads_acc, fs_byte_length, parse_iri, parse_nquad, parse_object, parse_opt_graph_label, parse_subject |
quad_ok_line_wf |
no (has requires) |
RDF.Canonical |
lemma_issue_fresh_label_shape |
RDF.Canonical |
issue_fresh |
is_issuer_label |
yes |
RDF.Canonical |
lemma_issue_identifier_fresh_label_shape |
RDF.Canonical |
issue_identifier, lookup_issued |
is_issuer_label |
no (has requires) |
RDF.CottasStore |
tables_of_handle_agree |
RDF.CottasStore |
tables_of_handle |
token_tables_agree_with |
yes |
RDF.CottasStore |
graph_bound_to_raw_token_agrees |
RDF.CottasStore |
graph_bound_to_raw_token_with, tables_of_handle |
token_tables_agree_with |
no (has requires) |
RDF.CottasStore |
build_qp_row_agrees |
RDF.CottasStore |
build_qp_row_with, tables_of_handle |
token_tables_agree_with |
no (has requires) |
RDF.CottasStore.CompoundPresenceBitmap |
rg_could_contain_pair_sound |
RDF.CottasStore.CompoundPresenceBitmap |
rg_could_contain_pair |
compound_built_correctly |
no (has requires) |
RDF.CottasStore.PresenceBitmap |
rg_contains_token_sound |
RDF.CottasStore.PresenceBitmap |
rg_contains_token |
bitmap_built_correctly |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_rho_df_step_extensive |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure_step, rho_df_closure_step_pre_dedup |
no_dup_keys |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure_sound |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure |
rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_f1_witness_frag |
RDF.Entailment.RDFS.RhoDFClosure |
f1_witness, i_rdfs_subPropertyOf |
rho_df_frag_graph |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_f1_bad_triple_not_frag |
RDF.Entailment.RDFS.RhoDFClosure |
f1_bad_triple |
rho_df_frag_triple |
yes |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_len_eq_saturated |
RDF.Entailment.RDFS.RhoDFClosure |
graph_len, rho_df_closure_step, rho_df_closure_step_pre_dedup |
no_dup_keys |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_pre_dedup_in_c |
RDF.Entailment.RDFS.RhoDFClosure |
rho_df_closure_step_pre_dedup |
no_dup_keys |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_is_rho_df_object_ok_correct |
RDF.Entailment.RDFS.RhoDFClosure |
is_rho_df_object_ok |
rho_df_object_ok |
yes |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_is_rho_df_frag_triple_correct |
RDF.Entailment.RDFS.RhoDFClosure |
is_rho_df_frag_triple |
rho_df_frag_triple |
yes |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_is_rho_df_frag_correct |
RDF.Entailment.RDFS.RhoDFClosure |
is_rho_df_frag |
rho_df_frag_graph |
yes |
RDF.Entailment.RDFS.RhoDFClosure |
theorem_rdfs_regime_bgp_sound |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp, instantiate_bgp, rho_df_closure |
bgp_frag, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
theorem_rdfs_regime_bgp_complete_conditional |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp, instantiate_bgp, rho_df_closure |
eval_bgp_complete_at, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
theorem_rdfs_regime_bgp_exact |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp, instantiate_bgp, rho_df_closure |
bgp_frag, eval_bgp_complete_at, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
theorem_rdfs_regime_ask_sound |
SPARQL11.EntailmentRegime.RDFS |
instantiate_bgp, rho_df_closure |
bgp_frag, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
theorem_rdfs_regime_ask_complete_conditional |
SPARQL11.EntailmentRegime.RDFS |
instantiate_bgp, rho_df_closure |
eval_bgp_complete_at, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
theorem_rdfs_regime_bgp_sound_selective |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp_store, graph_to_store_for, instantiate_bgp, rho_df_closure |
bgp_frag, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
theorem_rdfs_regime_ask_pattern_sound |
SPARQL11.EntailmentRegime.RDFS |
instantiate_bgp, rho_df_closure |
bgp_frag, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
theorem_rdfs_regime_ask_query_sound |
SPARQL11.EntailmentRegime.RDFS |
eval_ask_query, instantiate_bgp, query, rho_df_closure |
bgp_frag, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
theorem_rdfs_regime_bgp_complete_conditional_selective |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp_store, graph_to_store_for, instantiate_bgp, rho_df_closure |
eval_bgp_store_complete_at, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
theorem_rdfs_regime_ask_query_complete_conditional |
SPARQL11.EntailmentRegime.RDFS |
eval_ask_query, instantiate_bgp, query, rho_df_closure |
eval_bgp_store_complete_at, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
lemma_regime_answer_is_subgraph |
SPARQL11.EntailmentRegime.RDFS |
instantiate_bgp, rho_df_closure |
rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
theorem_rdfs_regime_bgp_complete |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp, instantiate_bgp, rho_df_closure |
bgp_frag, bgp_instantiable, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
theorem_rdfs_regime_bgp_exact_answer |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp, instantiate_bgp, rho_df_closure |
bgp_frag, bgp_instantiable, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
theorem_rdfs_regime_ask_complete |
SPARQL11.EntailmentRegime.RDFS |
instantiate_bgp, rho_df_closure |
bgp_frag, bgp_instantiable, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
theorem_rdfs_regime_bgp_complete_selective |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp_store, graph_to_store_for, instantiate_bgp, rho_df_closure |
bgp_frag, bgp_instantiable, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.RDFS.RhoDFClosure |
theorem_rdfs_regime_ask_query_complete |
SPARQL11.EntailmentRegime.RDFS |
eval_ask_query, instantiate_bgp, query, rho_df_closure |
bgp_frag, bgp_instantiable, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
RDF.Entailment.Simple |
lemma_try_match_complete |
RDF.Entailment.Simple.Refinement |
try_match |
all_matched, binding_compat, bnd_total, leq_reflexive |
no (has requires) |
RDF.Entailment.Simple |
lemma_match_term_ground_sound |
RDF.Entailment.Simple.Refinement |
match_term |
leq_always_identity |
no (has requires) |
RDF.Entailment.Simple |
lemma_match_triple_ground_sound |
RDF.Entailment.Simple.Refinement |
match_triple |
leq_always_identity |
no (has requires) |
RDF.Graph |
lemma_dedup_sorted_decorated_extensive |
RDF.Entailment.RDFS.FixedPoint |
dedup_sorted_decorated_aux, triple_to_key |
decoration_consistent, no_dup_keys_combined |
no (has requires) |
RDF.Graph |
lemma_graph_dedup_sort_extensive |
RDF.Entailment.RDFS.FixedPoint |
graph_dedup_sort |
no_dup_keys |
no (has requires) |
RDF.Graph |
lemma_len_eq_saturated |
RDF.Entailment.RDFS.FixedPoint |
graph_len, rdfs_closure_step |
no_dup_keys, step_saturated |
no (has requires) |
RDF.Graph |
lemma_sortWith_sorted_pairs_dt |
RDF.Entailment.RDFS.FixedPoint |
cmp_decorated_triple |
sorted_pairs_dt |
yes |
RDF.Graph |
lemma_dedup_sorted_decorated_no_repeats |
RDF.Entailment.RDFS.FixedPoint |
dedup_sorted_decorated_aux |
decoration_consistent, dedup_acc_inv, sorted_pairs_dt |
no (has requires) |
RDF.Graph |
lemma_len_eq_saturated_gapB |
RDF.Entailment.RDFS.FixedPoint |
graph_len, rdfs_closure_step |
no_dup_keys, step_saturated |
no (has requires) |
RDF.Graph |
rho_df_len_eq_saturated |
RDF.Entailment.RDFS.RhoDFClosure |
graph_len, rho_df_closure_step, rho_df_closure_step_pre_dedup |
no_dup_keys |
no (has requires) |
RDF.Graph |
lemma_lit_key_lang_part_sep_free |
RDF.Indexed.KeyInjectivity |
lit_key_lang_part |
str_sep_free |
no (has requires) |
RDF.Graph |
lemma_literal_key_injective |
RDF.Indexed.KeyInjectivity |
term_to_key_total |
literal_sep_free |
no (has requires) |
RDF.Graph |
lemma_term_to_key_total_injective |
RDF.Indexed.KeyInjectivity |
term_to_key_total |
term_sep_free |
no (has requires) |
RDF.Graph |
lemma_triple_to_key_injective |
RDF.Indexed.KeyInjectivity |
triple_to_key |
triple_full_sep_free |
no (has requires) |
RDF.Graph |
lemma_graph_full_sep_free_no_dup_keys |
RDF.Indexed.KeyInjectivity |
triple_to_key |
graph_full_sep_free |
no (has requires) |
RDF.Graph.Executable |
stream_fold_eq_batch |
RDF.NQuads.Streaming |
dataset_finalise, fs_byte_length, parse_nquads_acc |
stream_fold_wf |
no (has requires) |
RDF.Graph.Executable |
theorem_stream_consume_dataset_eq_batch |
RDF.NQuads.Streaming |
dataset_finalise |
stream_fold_wf |
no (has requires) |
RDF.Indexed |
lemma_tree_ok_lookup |
OWL.Semantics.MemLemmas |
bucket_lookup |
tree_ok |
no (has requires) |
RDF.Indexed |
lemma_slt_tree_ok |
OWL.Semantics.MemLemmas |
sorted_list_to_tree_fuel |
pairs_ok, tree_ok |
no (has requires) |
RDF.Indexed |
lemma_group_ok |
OWL.Semantics.MemLemmas |
group_sorted_decorated_aux |
dec_ok, pairs_ok |
no (has requires) |
RDF.Indexed |
lemma_build_bucket_ok |
OWL.Semantics.MemLemmas |
build_bucket |
tree_ok |
yes |
RDF.Indexed |
lemma_sortWith_sorted_pairs |
RDF.Indexed.Completeness |
cmp_by_decorated_key |
sorted_pairs |
yes |
RDF.Indexed |
lemma_group_sorted |
RDF.Indexed.Completeness |
group_sorted_decorated_aux |
group_sorted_inv, sorted_kv_desc |
no (has requires) |
RDF.Indexed |
lemma_slt_lookup_complete |
RDF.Indexed.Completeness |
bucket_lookup, sorted_list_to_tree_fuel |
sorted_kv |
no (has requires) |
RDF.Indexed |
lemma_subject_key_sep_free |
RDF.Indexed.KeyInjectivity |
subject_to_key |
str_sep_free, subj_label_sep_free |
no (has requires) |
RDF.Indexed |
sp_key_injective_one_sided |
RDF.Indexed.KeyInjectivity |
sp_key |
str_sep_free, subj_label_sep_free |
no (has requires) |
RDF.Indexed |
po_key_injective_one_sided |
RDF.Indexed.KeyInjectivity |
po_key |
str_sep_free, subj_label_sep_free |
no (has requires) |
RDF.Indexed |
lemma_triple_term_prefix_sep_free |
RDF.Indexed.KeyInjectivity |
subject_to_key |
str_sep_free |
no (has requires) |
RDF.Store.Columnar.DeltaMerge |
lemma_state_agrees_init |
RDF.Store.Columnar.DeltaMerge |
delta_resolved_empty |
state_agrees |
yes |
RDF.Store.Columnar.DeltaMerge |
lemma_state_agrees_step |
RDF.Store.Columnar.DeltaMerge |
apply_entry_ref_step, apply_entry_to_delta |
state_agrees |
no (has requires) |
RDF.Store.Columnar.DeltaMerge |
lemma_apply_entries_state_agrees |
RDF.Store.Columnar.DeltaMerge |
apply_entries_ref, fold_entries_for_graph |
state_agrees |
no (has requires) |
RDF.Store.Columnar.OffsetIndex |
row_positions_for_count_sound |
RDF.Store.Columnar.OffsetIndex |
row_positions_for |
offsets_built_correctly |
no (has requires) |
RDF.Store.Columnar.SubjectOffsetIndex |
range_for_subject_count_sound |
RDF.Store.Columnar.SubjectOffsetIndex |
range_for_subject, subject_range_count |
subject_offsets_built_correctly |
no (has requires) |
RDF.Term |
lemma_rdf_term_eq_denot |
OWL.Semantics |
rdf_term_eq |
cond_literal_term_eq_respecting |
no (has requires) |
RDF.Term |
lemma_rdf_term_eq_sound |
RDF.Entailment.RDFS.RhoDFClosure |
rdf_term_eq |
rho_df_object_ok |
no (has requires) |
RDF.Turtle.Serialize |
lemma_ts_abbreviate_iri_pname_safe |
RDF.Turtle.Serialize |
ts_abbreviate_iri |
compacts_to_pname_safe |
yes |
RDF.Vocabulary.Axioms |
finite_rdf_axioms_sound |
RDF.Entailment.RDF.Spec |
rdf_axiomatic_triples |
rdf_axiomatic |
no (has requires) |
RDF.Vocabulary.Axioms |
lemma_f1_witness_frag |
RDF.Entailment.RDFS.RhoDFClosure |
f1_witness, i_rdfs_subPropertyOf |
rho_df_frag_graph |
no (has requires) |
RDFS.Closure |
lemma_step_extensive |
RDF.Entailment.RDFS.FixedPoint |
rdfs_closure_step |
no_dup_keys |
no (has requires) |
RDFS.Closure |
lemma_len_eq_saturated |
RDF.Entailment.RDFS.FixedPoint |
graph_len, rdfs_closure_step |
no_dup_keys, step_saturated |
no (has requires) |
RDFS.Closure |
lemma_len_eq_saturated_gapB |
RDF.Entailment.RDFS.FixedPoint |
graph_len, rdfs_closure_step |
no_dup_keys, step_saturated |
no (has requires) |
RDFS.Closure |
lemma_chain_shift |
RDF.Entailment.RDFS.ModelTheory |
rdfs_closure_step |
closure_chain_wf |
no (has requires) |
RDFS.Closure |
rdfs_closure_entails |
RDF.Entailment.RDFS.ModelTheory |
rdfs_closure |
closure_chain_wf, rdfs_entails |
no (has requires) |
RDFS.Closure |
rdf_property_axiom_closure_entails |
RDF.Entailment.RDFS.ModelTheory |
rdf_property_axiom_closure |
rdf_entails |
yes |
RDFS.Closure |
rdfs_closure_with_reflexivity_entails |
RDF.Entailment.RDFS.ModelTheory |
rdfs_closure_with_reflexivity |
closure_chain_wf, rdfs_entails |
no (has requires) |
RDFS.Closure |
collect_related_iris_source |
RDF.Entailment.RDFS.Refinement |
collect_related_iris |
harvest_source |
yes |
RIF.Core.Eval |
lemma_fixpoint_extends |
RIF.Core.Eval |
fixpoint |
graph_subset |
yes |
RIF.Core.Eval |
rif_fixpoint_extensive |
RIF.Core.Refinement |
fixpoint |
graph_subset |
yes |
RIF.Core.Eval |
rif_one_round_extensive |
RIF.Core.Refinement |
one_round |
graph_subset |
yes |
RIF.Core.Eval |
rif_fire_rule_extensive |
RIF.Core.Refinement |
fire_rule |
graph_subset |
yes |
RIF.Core.Eval |
fire_head_per_bindings_licensed |
RIF.Core.Refinement |
fire_head_per_bindings |
rif_bindings_derive |
yes |
RIF.Core.Eval |
fire_rule_licensed |
RIF.Core.Refinement |
fire_rule |
rif_rule_derives |
yes |
RIF.Core.Eval |
lemma_one_round_aux_licensed |
RIF.Core.Refinement |
one_round_aux |
graph_subset, rif_derives |
no (has requires) |
RIF.Core.Eval |
one_round_licensed |
RIF.Core.Refinement |
one_round |
rif_derives |
yes |
RIF.Core.Eval |
fixpoint_licensed |
RIF.Core.Refinement |
fixpoint |
rif_derives |
yes |
RIF.Core.Tests |
lemma_saturate_extends |
RIF.Core.Tests |
saturate_with_program |
graph_subset |
yes |
SPARQL11.Algebra |
lemma_pick_smaller_bucket_sound |
SPARQL11.Algebra.BGPRefinement |
pick_smaller_bucket |
bucket_cand_sound |
no (has requires) |
SPARQL11.Algebra |
lemma_pick_smaller_bucket_complete |
SPARQL11.Algebra.BGPRefinement |
pick_smaller_bucket |
bucket_cand_complete |
no (has requires) |
SPARQL11.Algebra |
lemma_ig_search_complete_selective |
SPARQL11.Algebra.BGPRefinement |
ig_search |
bound_obj_exact |
no (has requires) |
SPARQL11.Algebra |
lemma_ig_search_complete |
SPARQL11.Algebra.BGPRefinement |
ig_search |
bound_obj_exact |
no (has requires) |
SPARQL11.Algebra |
lemma_store_search_complete |
SPARQL11.Algebra.BGPRefinement |
graph_to_store, store_search |
bound_obj_exact |
no (has requires) |
SPARQL11.Algebra |
lemma_store_search_complete_for |
SPARQL11.Algebra.BGPRefinement |
graph_to_store_for, group_graph_pattern, store_search |
bound_obj_exact |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_subgraph |
SPARQL11.Algebra.BGPRefinement |
eval_bgp |
bgp_frag, bgp_subgraph_clause, graph_frag |
no (has requires) |
SPARQL11.Algebra |
lemma_instantiate_bgp_subset |
SPARQL11.Algebra.BGPRefinement |
instantiate_bgp |
bgp_subgraph_clause |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_instantiates_into_graph |
SPARQL11.Algebra.BGPRefinement |
eval_bgp, instantiate_bgp |
bgp_frag, graph_frag |
no (has requires) |
SPARQL11.Algebra |
lemma_graph_to_store_sound |
SPARQL11.Algebra.BGPRefinement |
graph_to_store |
store_search_sound |
yes |
SPARQL11.Algebra |
lemma_graph_to_store_for_sound |
SPARQL11.Algebra.BGPRefinement |
graph_to_store_for, group_graph_pattern |
store_search_sound |
yes |
SPARQL11.Algebra |
lemma_eval_single_tp_sound_at |
SPARQL11.Algebra.BGPRefinement |
eval_single_tp_store_default, tp_match |
store_search_sound |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_store_subgraph |
SPARQL11.Algebra.BGPRefinement |
eval_bgp_store |
bgp_frag, bgp_subgraph_clause, graph_frag, store_search_sound |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_store_instantiates_into_graph |
SPARQL11.Algebra.BGPRefinement |
eval_bgp_store, instantiate_bgp |
bgp_frag, graph_frag, store_search_sound |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_store_for_instantiates_into_graph |
SPARQL11.Algebra.BGPRefinement |
eval_bgp_store, graph_to_store_for, group_graph_pattern, instantiate_bgp |
bgp_frag, graph_frag |
no (has requires) |
SPARQL11.Algebra |
lemma_graph_to_store_complete |
SPARQL11.Algebra.BGPRefinement |
graph_to_store |
store_search_complete |
yes |
SPARQL11.Algebra |
lemma_graph_to_store_for_complete |
SPARQL11.Algebra.BGPRefinement |
graph_to_store_for, group_graph_pattern |
store_search_complete |
yes |
SPARQL11.Algebra |
lemma_subgraph_clause_of_instantiated |
SPARQL11.Algebra.BGPRefinement |
instantiate_bgp, instantiate_tp |
bgp_subgraph_clause |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_store_complete_answer |
SPARQL11.Algebra.BGPRefinement |
eval_bgp_store, instantiate_bgp |
bgp_frag, bgp_subgraph_clause, graph_frag, store_search_complete, store_search_sound |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_store_complete_from_subset |
SPARQL11.Algebra.BGPRefinement |
eval_bgp_store, instantiate_bgp, instantiate_tp |
bgp_frag, graph_frag, store_search_complete, store_search_sound |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_complete_from_subset |
SPARQL11.Algebra.BGPRefinement |
eval_bgp, instantiate_bgp, instantiate_tp |
bgp_frag, graph_frag |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_store_for_complete_from_subset |
SPARQL11.Algebra.BGPRefinement |
eval_bgp_store, graph_to_store_for, group_graph_pattern, instantiate_bgp, instantiate_tp |
bgp_frag, graph_frag |
no (has requires) |
SPARQL11.Algebra |
lemma_eval_single_tp_store_domain |
SPARQL11.Algebra.BGPRefinement |
eval_single_tp_store, tp_vars |
tp_frag |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_store_domain_fuel |
SPARQL11.Algebra.BGPRefinement |
eval_bgp_store_from_mu_fuel |
bgp_dom_grow_clause, bgp_frag |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_domain |
SPARQL11.Algebra.BGPRefinement |
eval_bgp, sm_empty |
bgp_dom_grow_clause, bgp_frag |
no (has requires) |
SPARQL11.Algebra |
theorem_eval_bgp_dom_clause |
SPARQL11.Algebra.BGPRefinement |
eval_bgp |
bgp_dom_clause, bgp_frag |
no (has requires) |
SPARQL11.Algebra |
lemma_sm_compatible_sound |
SPARQL11.Algebra.Refinement |
sm_compatible |
smap_exact |
no (has requires) |
SPARQL11.Algebra |
lemma_try_bind_term_instantiates |
SPARQL11.Algebra.Refinement |
bound_object_of_pattern, try_bind_term |
binding_extends, ptrm_exact, smap_exact, term_exact |
no (has requires) |
SPARQL11.Algebra |
lemma_try_bind_subject_instantiates |
SPARQL11.Algebra.Refinement |
bound_subject_of_pattern, try_bind_subject |
binding_extends, smap_exact |
no (has requires) |
SPARQL11.Algebra |
theorem_tp_match_instantiates |
SPARQL11.Algebra.Refinement |
instantiate_tp, tp_match |
binding_extends, ptrm_exact, smap_exact, term_exact |
no (has requires) |
SPARQL11.Algebra |
theorem_sort_solutions_sorted |
SPARQL11.Algebra.Refinement |
compare_on_conditions, order_condition, sort_solutions |
sorted_by, totality_on, transitivity_on |
no (has requires) |
SPARQL11.Algebra |
lemma_sparql_order_numeric_frag_totality |
SPARQL11.Algebra.Refinement |
sparql_order |
er_num_plain |
no (has requires) |
SPARQL11.Algebra |
lemma_sparql_order_numeric_frag_trans |
SPARQL11.Algebra.Refinement |
sparql_order |
er_num_plain |
no (has requires) |
SPARQL11.Algebra |
lemma_smap_ground_lookup |
SPARQL11.EntailmentRegime.RDFS |
sm_lookup |
smap_ground, term_ground |
no (has requires) |
SPARQL11.Algebra |
lemma_bound_subject_ground |
SPARQL11.EntailmentRegime.RDFS |
bound_subject_of_pattern |
smap_ground, subject_ground |
no (has requires) |
SPARQL11.Algebra |
lemma_bound_object_ground |
SPARQL11.EntailmentRegime.RDFS |
bound_object_of_pattern |
smap_ground, term_ground |
no (has requires) |
SPARQL11.Algebra |
lemma_instantiate_tp_ground |
SPARQL11.EntailmentRegime.RDFS |
instantiate_tp |
smap_ground, tp_ground_positions, triple_ground |
no (has requires) |
SPARQL11.Algebra |
lemma_instantiate_bgp_ground |
SPARQL11.EntailmentRegime.RDFS |
instantiate_bgp |
bgp_ground_positions, smap_ground |
no (has requires) |
SPARQL11.Algebra |
theorem_rdfs_regime_bgp_sound |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp, instantiate_bgp, rho_df_closure |
bgp_frag, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
SPARQL11.Algebra |
theorem_rdfs_regime_bgp_complete_conditional |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp, instantiate_bgp, rho_df_closure |
eval_bgp_complete_at, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
SPARQL11.Algebra |
theorem_rdfs_regime_bgp_exact |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp, instantiate_bgp, rho_df_closure |
bgp_frag, eval_bgp_complete_at, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
SPARQL11.Algebra |
theorem_rdfs_regime_ask_sound |
SPARQL11.EntailmentRegime.RDFS |
instantiate_bgp, rho_df_closure |
bgp_frag, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
SPARQL11.Algebra |
theorem_rdfs_regime_ask_complete_conditional |
SPARQL11.EntailmentRegime.RDFS |
instantiate_bgp, rho_df_closure |
eval_bgp_complete_at, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
SPARQL11.Algebra |
theorem_rdfs_regime_bgp_sound_selective |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp_store, graph_to_store_for, instantiate_bgp, rho_df_closure |
bgp_frag, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
SPARQL11.Algebra |
theorem_rdfs_regime_ask_pattern_sound |
SPARQL11.EntailmentRegime.RDFS |
instantiate_bgp, rho_df_closure |
bgp_frag, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
SPARQL11.Algebra |
theorem_rdfs_regime_ask_query_sound |
SPARQL11.EntailmentRegime.RDFS |
eval_ask_query, instantiate_bgp, query, rho_df_closure |
bgp_frag, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
SPARQL11.Algebra |
theorem_rdfs_regime_bgp_complete_conditional_selective |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp_store, graph_to_store_for, instantiate_bgp, rho_df_closure |
eval_bgp_store_complete_at, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
SPARQL11.Algebra |
theorem_rdfs_regime_ask_query_complete_conditional |
SPARQL11.EntailmentRegime.RDFS |
eval_ask_query, instantiate_bgp, query, rho_df_closure |
eval_bgp_store_complete_at, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
SPARQL11.Algebra |
lemma_regime_answer_is_subgraph |
SPARQL11.EntailmentRegime.RDFS |
instantiate_bgp, rho_df_closure |
rho_df_decides_hyps, rho_df_entails |
no (has requires) |
SPARQL11.Algebra |
theorem_rdfs_regime_bgp_complete |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp, instantiate_bgp, rho_df_closure |
bgp_frag, bgp_instantiable, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
SPARQL11.Algebra |
theorem_rdfs_regime_bgp_exact_answer |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp, instantiate_bgp, rho_df_closure |
bgp_frag, bgp_instantiable, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
SPARQL11.Algebra |
theorem_rdfs_regime_ask_complete |
SPARQL11.EntailmentRegime.RDFS |
instantiate_bgp, rho_df_closure |
bgp_frag, bgp_instantiable, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
SPARQL11.Algebra |
theorem_rdfs_regime_bgp_complete_selective |
SPARQL11.EntailmentRegime.RDFS |
eval_bgp_store, graph_to_store_for, instantiate_bgp, rho_df_closure |
bgp_frag, bgp_instantiable, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
SPARQL11.Algebra |
theorem_rdfs_regime_ask_query_complete |
SPARQL11.EntailmentRegime.RDFS |
eval_ask_query, instantiate_bgp, query, rho_df_closure |
bgp_frag, bgp_instantiable, graph_frag, rho_df_decides_hyps, rho_df_entails |
no (has requires) |
| Module | Theorems | Unconditional | Example |
|---|---|---|---|
Dep.Reachability |
1 | 0 | no_root_reaches (all_mem, is_closed) |
HDT.Container |
2 | 0 | lemma_parse_control_info_rejects_bad_cookie (byte_get, parse_control_info) |
OWL.Closure |
13 | 13 | lemma_vocab_symp_agree (owl_SymmetricProperty, rdf_type) |
Parquet.Footer |
2 | 2 | lemma_parse_version_hex_literal (cottas_format_version, parse_file_metadata_version_hex) |
Parser.Combinators |
5 | 0 | lemma_ptake_while_acc_pos_shift_headroom (fs_byte_length, ptake_while_acc) |
Parser.FastString |
78 | 18 | fs_byte_sub_self (fs_byte_length, fs_byte_sub) |
Parser.FastString.Spec |
37 | 22 | lemma_decode_all_aux_encode (utf8_decode_all_aux, utf8_enc_char) |
Parser.JSON |
1 | 1 | lemma_json_val_of_response_roundtrip (json_get_array, json_get_field, json_get_string_array) |
Parser.JSONResults |
1 | 1 | lemma_json_val_of_response_roundtrip (json_get_array, json_get_field, json_get_string_array) |
Parser.NQuads |
15 | 6 | stream_parse_single_chunk_shape (dataset_finalise, fs_byte_length, parse_nquads_acc) |
Parser.NTriples |
56 | 3 | checkpoint_a_closed_triple_round_trip (nq_line_for_triple_default_graph, parse_triple) |
Parser.RIFXML |
1 | 0 | lemma_parse_none_yields_false (parse_rif_program, run_rif_select_rows) |
RDF.Bytes |
20 | 18 | lemma_int_of_byte_of_int (byte_of_int, int_of_byte) |
RDF.CottasStore.BaseWriter |
3 | 3 | lemma_version_field_bytes_eq (byte_of_int, version_field_bytes) |
RDF.CottasStore.ColumnSeq |
1 | 0 | column_decode_sound (column_to_list, probe_parquet_column_decode_in_row_group_seq) |
RDF.CottasStore.CompoundPresenceWriter |
5 | 3 | lemma_parse_n_u64s_one (parse_n_u64s, write_u64_le) |
RDF.CottasStore.DictWriter |
11 | 1 | lemma_parse_serialize_dict_empty_case (parse_dict, serialize_dict) |
RDF.CottasStore.OffsetsWriter |
7 | 3 | lemma_parse_n_u64s_one (parse_n_u64s, write_u64_le) |
RDF.CottasStore.PageCache |
3 | 1 | find_oldest_aux_returns_present (find_oldest_aux, key_eq) |
RDF.CottasStore.PresenceWriter |
2 | 1 | lemma_parse_serialize_presence_empty_case (parse_presence, serialize_presence) |
RDF.CottasStore.SubjectOffsetsWriter |
3 | 1 | lemma_unflatten_flatten (flatten_ranges, unflatten_ranges) |
RDF.Entailment.RDFS.RhoDFClosure |
8 | 3 | lemma_rho_df_step_is_dedup_of_pre_dedup (graph_dedup_sort, rho_df_closure_step, rho_df_closure_step_pre_dedup) |
RDF.Entailment.Simple |
1 | 1 | lemma_simple_entails_unfold (simple_entails, try_match) |
RDF.Graph |
11 | 10 | lemma_step_is_dedup_of_pre_dedup (graph_dedup_sort, rdfs_closure_step) |
RDF.Graph.Executable |
1 | 1 | stream_parse_single_chunk_shape (dataset_finalise, fs_byte_length, parse_nquads_acc) |
RDF.Indexed |
28 | 21 | lemma_build_indexed_wf_pred (bucket_lookup, build_indexed) |
RDF.List.Helpers |
1 | 1 | lemma_eval_bgp_store_unfold (choose_best_tp, concatMap_tr, eval_bgp_store_from_mu_fuel) |
RDF.NQuads.Serialize |
7 | 1 | checkpoint_a_closed_triple_round_trip (nq_line_for_triple_default_graph, parse_triple) |
RDF.Store.Columnar.DeltaLog |
24 | 12 | lemma_u8_roundtrip (parse_u8, write_u8) |
RDF.Store.Columnar.DeltaMerge |
3 | 3 | lemma_mem_matches_bound_acc (bound_matches, triple_matches_bound_acc) |
RDF.Term |
14 | 0 | lemma_parse_iri_shift (fs_byte_index, fs_byte_length, is_iri) |
RDF.Vocabulary.Axioms |
3 | 3 | lemma_rho_df_vocab_distinct (i_rdf_type, i_rdfs_domain, i_rdfs_range) |
RDFS.Closure |
24 | 17 | lemma_vocab_symp_agree (owl_SymmetricProperty, rdf_type) |
RDFS.SchemaSplit |
2 | 2 | witness_stable_holds (schema_stable_check, witness_stable) |
RIF.Core.Tests |
1 | 0 | lemma_parse_none_yields_false (parse_rif_program, run_rif_select_rows) |
Regex.Derivative |
8 | 4 | deriv_correct (deriv, mem) |
Regex.Exec |
16 | 12 | insert_regex_ok (insert_regex, mem, mem_alt_list) |
Regex.Syntax |
30 | 22 | deriv_correct (deriv, mem) |
SPARQL.Eval.Limits |
5 | 1 | take_capped_unlimited_id (no_cap, take_capped) |
SPARQL.Eval.TimeBudget |
2 | 0 | disabled_never_expires (is_disabled, is_expired) |
SPARQL.FullText |
2 | 0 | lemma_parse_object_list_simple_1 (fulltext_query_pred, ggp_add_triple, group_graph_pattern) |
SPARQL.Protocol |
2 | 2 | lemma_srj_single_row (json_row, json_var_list, serialise_response_json) |
SPARQL11.Algebra |
53 | 18 | lemma_mem_matches_bound_acc (bound_matches, triple_matches_bound_acc) |
SPARQL11.Parser |
21 | 0 | lemma_path_elt_iri (parse_path_elt, parse_peek) |
Tableau.CountingOracle |
8 | 2 | lin_dot_zeros (lin_dot, zeros) |
assume val = active assumed declarations. Adm = active admissions plus --lax/--admit_smt_queries regions. Local = local refinement lemmas. Alg / Int / W3C = algorithm-correctness, internal-refinement and W3C-refinement theorems about this module's shipping functions.
| Module | Tier | Extraction | assume val | Adm | Local | Alg | Int | W3C | Suites |
|---|---|---|---|---|---|---|---|---|---|
CSVW.Conversion |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | csvw-nonnorm |
CSVW.Formats |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
CSVW.Json |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | csvw-csv2json, csvw-nonnorm |
CSVW.Metadata |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
CSVW.URITemplate |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
CSVW.Validate |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | csvw-validation |
DID.Key |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
Dep.Reachability |
algorithm-correctness theorem | extracted | 0 | 0 | 2 | 1 | 0 | 0 | — |
GRDDL.Discovery |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | grddl |
HDT.Container |
algorithm-correctness theorem | extracted | 0 | 0 | 0 | 2 | 0 | 0 | — |
HDT.Dictionary |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
HDT.Triples |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
JSONLD.Compact |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | jsonld-compact, jsonld-flatten, jsonld-frame |
JSONLD.Context |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | jsonld-compact, jsonld-expand, jsonld-flatten |
JSONLD.Expand |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | jsonld-compact, jsonld-expand, jsonld-flatten, jsonld-frame |
JSONLD.Flatten |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | jsonld-flatten, jsonld-frame |
JSONLD.Frame |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | jsonld-frame |
JSONLD.FromRdf |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
JSONLD.Loader |
merely Tot | extracted | 1 | 0 | 0 | 0 | 0 | 0 | — |
JSONSchema.Validate |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | jsonschema |
LWS.Core.Spec |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 28 | 0 | 0 | 0 | — |
LWS.Solid.Registry |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 0 | 0 | 0 | 0 | — |
Math.Diff |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | toan-matrix |
Math.Expr |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | toan-matrix |
Math.Matrix |
local lemmas only | extracted | 0 | 0 | 1 | 0 | 0 | 0 | toan-matrix |
Math.Series |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | toan-matrix |
Math.Sigmoid |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | toan-matrix |
Math.Simplify |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | toan-matrix |
Math.Subst |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | toan-matrix |
MathML.Content |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | toan-matrix |
MathML.Present |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | toan-matrix |
OWL.Closure |
W3C-refinement theorem | extracted | 0 | 0 | 0 | 13 | 11 | 108 | local-negative-test-vacuity, owl-profile-el, owl-profile-ql, owl-semantics-direct, +4 more |
OWL.DirectMapping.Filter |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | rif |
OWL.QueryEval |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | rif, sparql11-entailment, sparql11-query |
OWL.QueryRewrite |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | rif, sparql11-entailment, sparql11-query |
OWL.RL.Refinement |
specification / proof module | fully-erased | 0 | 0 | 15 | 0 | 0 | 0 | — |
OWL.RL.Spec |
specification / proof module | fully-erased | 0 | 0 | 0 | 0 | 0 | 0 | — |
OWL.Semantics |
specification / proof module | fully-erased | 0 | 0 | 2 | 0 | 0 | 0 | — |
OWL.Semantics.MemLemmas |
specification / proof module | fully-erased | 0 | 0 | 11 | 0 | 0 | 0 | — |
OWL.Semantics.Soundness |
specification / proof module | fully-erased | 0 | 0 | 4 | 0 | 0 | 0 | — |
OWL.Tests.Manifest |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
OWL.Vocabulary |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | csvw-csv2json, csvw-nonnorm, csvw-validation, csvw, +78 more |
OWL2.SyntaxDL |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | owl-syntax-dl |
Parquet.Footer |
algorithm-correctness theorem | extracted | 3 | 0 | 0 | 2 | 0 | 0 | local-cottas-corpus, local-cottas-row-order, local-parquet-footer-version-gate, local-parquet-footer |
Parser.BallyhooCOTTAS |
merely Tot | extracted | 13 | 0 | 0 | 0 | 0 | 0 | local-cottas-corpus, local-cottas-row-order |
Parser.BallyhooHDT |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
Parser.CSVResults |
local lemmas only | extracted | 0 | 0 | 1 | 0 | 0 | 0 | sparql11-federated-query, sparql11-query |
Parser.Combinators |
algorithm-correctness theorem | extracted | 0 | 0 | 0 | 5 | 0 | 0 | local-parser-unicode, local-sparql-parser, rdf-mt, rdf-n-quads, +6 more |
Parser.Diagnostics |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
Parser.FastString |
internal-refinement theorem | extracted | 0 | 0 | 0 | 78 | 31 | 0 | csvw-csv2json, csvw-nonnorm, csvw-validation, csvw, +78 more |
Parser.FastString.Axioms |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 12 | 0 | 0 | 0 | — |
Parser.FastString.BaseCases |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 31 | 0 | 0 | 0 | — |
Parser.FastString.CharBoundary |
merely Tot | extracted | 1 | 0 | 0 | 0 | 0 | 0 | — |
Parser.FastString.ConcatSpec |
local lemmas only | extracted | 0 | 0 | 6 | 0 | 0 | 0 | — |
Parser.FastString.RoundTripLemmas |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 20 | 0 | 0 | 0 | — |
Parser.FastString.Spec |
algorithm-correctness theorem | extracted | 0 | 0 | 15 | 37 | 0 | 0 | — |
Parser.IRI |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | csvw-csv2json, csvw-nonnorm, csvw-validation, csvw, +78 more |
Parser.JSON |
algorithm-correctness theorem | extracted | 0 | 0 | 0 | 1 | 0 | 0 | eecc-interop, jsonld-frame, jsonld-html, jsonld-tordf, +5 more |
Parser.JSONLD |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | jsonld-compact, jsonld-expand, jsonld-flatten, jsonld-frame, +4 more |
Parser.JSONLD.Html |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | jsonld-html |
Parser.JSONResults |
algorithm-correctness theorem | extracted | 0 | 0 | 0 | 1 | 0 | 0 | sparql11-federated-query, sparql11-query |
Parser.NQuads |
internal-refinement theorem | extracted | 0 | 0 | 0 | 15 | 21 | 0 | jsonld-html, jsonld-tordf, local-parser-unicode, rdf-n-quads, +3 more |
Parser.NTriples |
W3C-refinement theorem | extracted | 0 | 0 | 0 | 56 | 2 | 1 | local-parser-unicode, rdf-mt, rdf-n-quads, rdf-n-triples, +5 more |
Parser.NTriples.Locality |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 4 | 0 | 0 | 0 | — |
Parser.OWLFunctional |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | owl-semantics-direct, owl-syntax-dl, owl-type-consistency, owl-type-inconsistency, +2 more |
Parser.RDFXML |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | local-parser-unicode, owl-profile-el, owl-profile-ql, owl-profile-rl, +7 more |
Parser.RIFXML |
algorithm-correctness theorem | extracted | 0 | 0 | 0 | 1 | 0 | 0 | rif, sparql11-entailment |
Parser.SRX |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | sparql11-federated-query, sparql11-query |
Parser.ShExC |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | shex-negative-syntax |
Parser.TriG |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | local-parser-unicode, rdf-trig, sparql11-query, sparql11-update |
Parser.Turtle |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | local-parser-unicode, local-rdf12-semantics-tight, local-turtle-pretty, rdf-mt, +11 more |
Parser.TurtleScanner |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | local-parser-unicode, local-turtle-pretty, rdf-mt, rdf-trig, +6 more |
Parser.WKT |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | geosparql |
Parser.XML |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | local-parser-unicode, owl-profile-el, owl-profile-ql, owl-profile-rl, +7 more |
Parser.XPath |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | xpath-unit |
RDF.Bytes |
algorithm-correctness theorem | extracted | 0 | 0 | 8 | 20 | 0 | 0 | local-parquet-footer-version-gate |
RDF.Canonical |
internal-refinement theorem | extracted | 2 | 0 | 4 | 0 | 2 | 0 | jsonld-html, jsonld-tordf, local-graphs-api, local-jsonld-regressions, +4 more |
RDF.Canonical.Manifest |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | rdfc10 |
RDF.CottasStore |
internal-refinement theorem | extracted | 3 | 0 | 1 | 0 | 3 | 0 | local-cottas-corpus, local-cottas-row-order, local-parquet-footer-version-gate |
RDF.CottasStore.BaseWriter |
algorithm-correctness theorem | extracted | 0 | 0 | 6 | 3 | 0 | 0 | local-parquet-footer-version-gate |
RDF.CottasStore.ColumnSeq |
algorithm-correctness theorem | extracted | 4 | 0 | 0 | 1 | 0 | 0 | local-cottas-ask-decode-failure |
RDF.CottasStore.CompoundPresenceBitmap |
internal-refinement theorem | extracted | 0 | 0 | 0 | 0 | 1 | 0 | — |
RDF.CottasStore.CompoundPresenceWriter |
algorithm-correctness theorem | extracted | 0 | 0 | 2 | 5 | 0 | 0 | — |
RDF.CottasStore.DictWriter |
algorithm-correctness theorem | extracted | 0 | 0 | 6 | 11 | 0 | 0 | — |
RDF.CottasStore.LazyDict |
merely Tot | extracted | 9 | 0 | 0 | 0 | 0 | 0 | local-cottas-ask-decode-failure |
RDF.CottasStore.LazyDictRegistry |
merely Tot | extracted | 5 | 0 | 0 | 0 | 0 | 0 | — |
RDF.CottasStore.OffsetsWriter |
algorithm-correctness theorem | extracted | 0 | 0 | 2 | 7 | 0 | 0 | — |
RDF.CottasStore.OnDiskIndex |
local lemmas only | extracted | 7 | 0 | 1 | 0 | 0 | 0 | local-cottas-row-order |
RDF.CottasStore.PageCache |
algorithm-correctness theorem | extracted | 4 | 0 | 0 | 3 | 0 | 0 | local-cottas-ask-decode-failure, local-cottas-groupby-counts |
RDF.CottasStore.PageCache.Bounds |
local lemmas only | fully-erased | 0 | 0 | 12 | 0 | 0 | 0 | — |
RDF.CottasStore.PresenceBitmap |
internal-refinement theorem | extracted | 0 | 0 | 0 | 0 | 1 | 0 | — |
RDF.CottasStore.PresenceWriter |
algorithm-correctness theorem | extracted | 0 | 0 | 0 | 2 | 0 | 0 | — |
RDF.CottasStore.SubjectOffsetsWriter |
algorithm-correctness theorem | extracted | 0 | 0 | 1 | 3 | 0 | 0 | — |
RDF.Dataset.Graphs |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | local-graphs-api |
RDF.Dataset.Merge |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | local-graph-default-semantics |
RDF.Entailment.RDF.Spec |
specification / proof module | fully-erased | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDF.Entailment.RDFS.ChainWf |
local lemmas only | fully-erased | 0 | 0 | 9 | 0 | 0 | 0 | — |
RDF.Entailment.RDFS.Completeness |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 25 | 0 | 0 | 0 | — |
RDF.Entailment.RDFS.DatatypeClash |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDF.Entailment.RDFS.FixedPoint |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 31 | 0 | 0 | 0 | — |
RDF.Entailment.RDFS.ModelTheory |
specification / proof module | fully-erased | 0 | 0 | 22 | 0 | 0 | 0 | — |
RDF.Entailment.RDFS.Refinement |
specification / proof module | fully-erased | 0 | 0 | 21 | 0 | 0 | 0 | — |
RDF.Entailment.RDFS.RhoDFClosure |
W3C-refinement theorem | extracted | 0 | 0 | 9 | 8 | 25 | 20 | — |
RDF.Entailment.RDFS.SepFree |
specification / proof module | fully-erased | 0 | 0 | 38 | 0 | 0 | 0 | — |
RDF.Entailment.RDFS.Spec |
specification / proof module | fully-erased | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDF.Entailment.RDFSPlus |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDF.Entailment.Regime |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | local-negative-test-vacuity, local-rdf12-semantics-tight |
RDF.Entailment.RegimeDispatch |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDF.Entailment.Simple |
W3C-refinement theorem | extracted | 0 | 0 | 0 | 1 | 3 | 21 | local-rdf12-semantics-tight |
RDF.Entailment.Simple.Boundary |
local lemmas only | fully-erased | 0 | 0 | 13 | 0 | 0 | 0 | — |
RDF.Entailment.Simple.ModelTheory |
specification / proof module | fully-erased | 0 | 0 | 30 | 0 | 0 | 0 | — |
RDF.Entailment.Simple.Refinement |
specification / proof module | fully-erased | 0 | 0 | 14 | 0 | 0 | 0 | — |
RDF.Entailment.Simple.Spec |
specification / proof module | fully-erased | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDF.Format |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | csvw-csv2json, csvw-nonnorm, csvw-validation, csvw, +78 more |
RDF.Geo.BBox |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | geosparql |
RDF.Geo.Functions |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | geosparql |
RDF.Geo.Topology |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | geosparql |
RDF.Geo.Types |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | geosparql |
RDF.Graph |
W3C-refinement theorem | extracted | 0 | 0 | 0 | 11 | 12 | 18 | — |
RDF.Graph.Executable |
internal-refinement theorem | extracted | 0 | 0 | 3 | 1 | 2 | 0 | csvw-csv2json, csvw-nonnorm, csvw-validation, csvw, +78 more |
RDF.GraphIsomorphism |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDF.IRI |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDF.Indexed |
W3C-refinement theorem | extracted | 0 | 0 | 0 | 28 | 11 | 72 | — |
RDF.Indexed.Completeness |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 18 | 0 | 0 | 0 | — |
RDF.Indexed.KeyInjectivity |
specification / proof module | fully-erased | 0 | 0 | 10 | 0 | 0 | 0 | — |
RDF.Indexed.StringOrder |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 3 | 0 | 0 | 0 | — |
RDF.List.Helpers |
W3C-refinement theorem | extracted | 0 | 0 | 6 | 1 | 0 | 1 | sparql11-query |
RDF.NQuads.Serialize |
algorithm-correctness theorem | extracted | 0 | 0 | 0 | 7 | 0 | 0 | local-serializer-unicode, rdf-n-quads, rdfc10 |
RDF.NQuads.Streaming |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 34 | 0 | 0 | 0 | — |
RDF.NTriples.RoundTrip |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 12 | 0 | 0 | 0 | — |
RDF.Pretty |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDF.Semantics.HypothesisWitness |
specification / proof module | fully-erased | 0 | 0 | 32 | 0 | 0 | 0 | — |
RDF.Store.Capabilities |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDF.Store.Capabilities.Cottas |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDF.Store.Capabilities.Delta |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDF.Store.Columnar.DeltaLog |
algorithm-correctness theorem | extracted | 5 | 0 | 5 | 24 | 0 | 0 | — |
RDF.Store.Columnar.DeltaMerge |
internal-refinement theorem | extracted | 0 | 0 | 24 | 3 | 3 | 0 | — |
RDF.Store.Columnar.OffsetIndex |
internal-refinement theorem | extracted | 0 | 0 | 2 | 0 | 1 | 0 | — |
RDF.Store.Columnar.SubjectOffsetIndex |
internal-refinement theorem | extracted | 0 | 0 | 2 | 0 | 1 | 0 | — |
RDF.Store.Combine |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDF.Store.LazyTermCache |
merely Tot | extracted | 6 | 0 | 0 | 0 | 0 | 0 | — |
RDF.Store.Loader |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDF.Term |
W3C-refinement theorem | extracted | 0 | 0 | 5 | 14 | 2 | 3 | — |
RDF.Triple |
local lemmas only | extracted | 0 | 0 | 1 | 0 | 0 | 0 | — |
RDF.Turtle.Serialize |
internal-refinement theorem | extracted | 0 | 0 | 0 | 0 | 1 | 0 | local-turtle-pretty |
RDF.Vocabulary |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDF.Vocabulary.Axioms |
W3C-refinement theorem | extracted | 0 | 0 | 0 | 3 | 2 | 8 | — |
RDFS.Closure |
W3C-refinement theorem | extracted | 0 | 0 | 0 | 24 | 8 | 113 | local-negative-test-vacuity, local-rdf12-semantics-tight |
RDFS.Closure.SemiNaive |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
RDFS.SchemaSplit |
algorithm-correctness theorem | extracted | 0 | 0 | 5 | 2 | 0 | 0 | — |
RIF.Core.Builtins |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | rif |
RIF.Core.Conformance |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | rif |
RIF.Core.Eval |
internal-refinement theorem | extracted | 0 | 0 | 8 | 0 | 9 | 0 | rif, sparql11-entailment |
RIF.Core.Refinement |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 4 | 0 | 0 | 0 | — |
RIF.Core.Syntax |
local lemmas only | extracted | 0 | 0 | 2 | 0 | 0 | 0 | rif, sparql11-entailment |
RIF.Core.Tests |
internal-refinement theorem | extracted | 0 | 0 | 0 | 1 | 1 | 0 | sparql11-entailment |
RIF.Core.Translation |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | rif, sparql11-entailment |
RML.Eval |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | rml |
RML.Mapping |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | rml |
RML.Sources |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | csvw-nonnorm, rml |
RML.VirtualSource |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
Regex.Derivative |
algorithm-correctness theorem | extracted | 0 | 0 | 4 | 8 | 0 | 0 | — |
Regex.Exec |
algorithm-correctness theorem | extracted | 0 | 0 | 0 | 16 | 0 | 0 | jsonschema |
Regex.Syntax |
algorithm-correctness theorem | extracted | 0 | 0 | 12 | 30 | 0 | 0 | — |
Regex.XSDPattern |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | jsonschema |
SHACL.NodeExpr |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
SHACL.Rules |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
SHACL.Validation |
merely Tot | extracted | 1 | 0 | 0 | 0 | 0 | 0 | qudt, shacl-core, shacl-sparql |
SPARQL.Diagnostics |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | sparql11-query |
SPARQL.Eval.Limits |
algorithm-correctness theorem | extracted | 0 | 0 | 0 | 5 | 0 | 0 | sparql11-entailment, sparql11-query, sparql11-update |
SPARQL.Eval.TimeBudget |
algorithm-correctness theorem | extracted | 1 | 0 | 0 | 2 | 0 | 0 | sparql11-entailment, sparql11-query, sparql11-update |
SPARQL.Explain |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
SPARQL.FullText |
algorithm-correctness theorem | extracted | 0 | 0 | 0 | 2 | 0 | 0 | — |
SPARQL.GraphStore |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | sparql11-protocol |
SPARQL.HTTP |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | sparql11-protocol, sparql11-service-description |
SPARQL.HTTP.Admin |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | sparql11-protocol |
SPARQL.HTTP.BackendInfo |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | sparql11-protocol, sparql11-service-description |
SPARQL.HTTP.Client |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | sparql11-federated-query |
SPARQL.HTTP.QueriesIndex |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | sparql11-protocol, sparql11-service-description |
SPARQL.HTTP.Response |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | sparql11-protocol |
SPARQL.HTTP.Routes |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
SPARQL.HTTP.RunQuery |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
SPARQL.HTTP.StaticFiles |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | sparql11-protocol |
SPARQL.JSON.Escape |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | sparql11-protocol, sparql11-query, sparql11-update |
SPARQL.Plan.AccessPath |
local lemmas only | extracted | 0 | 0 | 4 | 0 | 0 | 0 | local-cottas-groupby-counts, sparql11-query |
SPARQL.Plan.Pruning |
local lemmas only | extracted | 0 | 0 | 1 | 0 | 0 | 0 | local-cottas-groupby-counts, sparql11-query |
SPARQL.Plan.Streamable |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
SPARQL.Protocol |
algorithm-correctness theorem | extracted | 0 | 0 | 0 | 2 | 0 | 0 | sparql11-protocol, sparql11-service-description |
SPARQL.Protocol.Client |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
SPARQL.Protocol.RoundTrip |
local lemmas only | fully-erased | 0 | 0 | 11 | 0 | 0 | 0 | — |
SPARQL.Query.Analysis |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | sparql11-query |
SPARQL.ServiceDescription |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
SPARQL.Update.Analysis |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | sparql11-update |
SPARQL.Update.Sandbox |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | sparql11-update |
SPARQL11.Algebra |
W3C-refinement theorem | extracted | 11 | 0 | 24 | 53 | 54 | 49 | local-backend-parity-full, local-graph-default-semantics, local-sparql-negative, local-sparql-parser, +11 more |
SPARQL11.Algebra.BGPRefinement |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 29 | 0 | 0 | 0 | — |
SPARQL11.Algebra.Refinement |
specification / proof module | fully-erased | 0 | 0 | 74 | 0 | 0 | 0 | — |
SPARQL11.Algebra.Spec |
specification / proof module | fully-erased | 0 | 0 | 36 | 0 | 0 | 0 | — |
SPARQL11.EntailmentRegime.RDFS |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 12 | 0 | 0 | 0 | — |
SPARQL11.Expression.Refinement |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 19 | 0 | 0 | 0 | — |
SPARQL11.IRI.Resolve |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
SPARQL11.Parser |
algorithm-correctness theorem | extracted | 0 | 0 | 0 | 21 | 0 | 0 | local-sparql-negative, local-sparql-parser, rif, shacl-sparql, +6 more |
SPARQL11.Parser.AskBgpRoundTrip |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 15 | 0 | 0 | 0 | — |
SPARQL11.Parser.TokenRoundTrip |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 45 | 0 | 0 | 0 | — |
SPARQL11.Store |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | local-backend-parity-full, local-backend-parity, local-graph-default-semantics, sparql11-entailment, +3 more |
Schematron.Validate |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
ShEx.Schema |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | shex-negative-syntax, shex |
ShEx.SchemaEq |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
ShEx.Validation |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | shex |
Solid.Protocol.Spec |
unclassified (oracle unavailable) | not-in-build-list | 0 | 0 | 43 | 0 | 0 | 0 | — |
Tableau |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | owl-semantics-direct, owl-type-consistency, owl-type-inconsistency, owl-type-negative-entailment, +3 more |
Tableau.CountingOracle |
algorithm-correctness theorem | extracted | 1 | 0 | 5 | 8 | 0 | 0 | owl-semantics-direct, owl-type-consistency, owl-type-inconsistency, owl-type-negative-entailment, +1 more |
Tableau.Refute |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | owl-semantics-direct, owl-type-consistency, owl-type-inconsistency, owl-type-negative-entailment, +1 more |
VC.Context |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | eecc-interop |
VC.Credential |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | eecc-interop, vc, vc20-api |
VC.DataIntegrity |
merely Tot | extracted | 4 | 0 | 0 | 0 | 0 | 0 | eecc-interop, vc-di-eddsa, vc20-api |
VC.Multibase |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | vc-di-eddsa |
XForms.Bind |
local lemmas only | extracted | 0 | 0 | 1 | 0 | 0 | 0 | xforms |
XML.Namespaces |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
XML.Wellformedness |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
XPath.Eval |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | grddl, xpath-unit |
XSD.Datatypes |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | local-rdf12-semantics-tight, rif, shex |
XSD.Facets |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
XSD.IEEE754 |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | — |
XSLT.Transform |
merely Tot | extracted | 0 | 0 | 0 | 0 | 0 | 0 | grddl |
Every suite the per-suite manifests define, with the score read back from the committed runner log or, failing that, from docs/test-results/latest.json. Source records where each number came from, so a disagreement is traceable rather than arguable. A suite reading no numbers has no committed log line the tool can match — that is a gap in the measurement chain, reported rather than filled in.
| Suite | Pass | Fail | Skip | Total | Source |
|---|---|---|---|---|---|
csvw |
— | — | — | — | unresolved — no score line matched in formal/fstar/ocaml-output/csvw_results.log |
csvw-csv2json |
270 | 0 | 0 | 270 | docs/test-results/latest.json:csvw_csv2json |
csvw-nonnorm |
— | — | — | — | unresolved — declared log_path missing: None |
csvw-validation |
281 | 1 | 0 | 282 | docs/test-results/latest.json:csvw_validation |
did |
— | — | — | — | unresolved — no score line matched in formal/fstar/ocaml-output/did_results.log |
eecc-interop |
4 | 0 | 51 | 55 | docs/test-results/latest.json:eecc_interop |
geosparql |
— | — | — | — | unresolved — no committed log carries score lines for geosparql_v0_unit |
grddl |
18 | 50 | 0 | 68 | suite-log:named-line:formal/fstar/ocaml-output/grddl_results.log |
jsonld-compact |
245 | 0 | 0 | 245 | suite-log:named-line:formal/fstar/ocaml-output/jsonld_compact_results.log |
jsonld-expand |
385 | 0 | 0 | 385 | suite-log:named-line:formal/fstar/ocaml-output/jsonld_expand_results.log |
jsonld-flatten |
58 | 0 | 0 | 58 | suite-log:named-line:formal/fstar/ocaml-output/jsonld_flatten_results.log |
jsonld-frame |
28 | 64 | 0 | 92 | suite-log:named-line:formal/fstar/ocaml-output/jsonld_frame_results.log |
jsonld-fromrdf |
53 | 0 | 1 | 54 | docs/test-results/latest.json:jsonld_fromrdf |
jsonld-html |
50 | 0 | 0 | 50 | suite-log:named-line:formal/fstar/ocaml-output/jsonld_html_results.log |
jsonld-tordf |
467 | 0 | 0 | 467 | suite-log:named-line:formal/fstar/ocaml-output/jsonld_results.log |
jsonschema |
770 | 0 | 0 | 770 | docs/test-results/latest.json:jsonschema |
local-backend-parity |
— | — | — | — | unresolved — declared log_path missing: None |
local-backend-parity-full |
— | — | — | — | unresolved — declared log_path missing: None |
local-check-pages-links |
— | — | — | — | unresolved — declared log_path missing: None |
local-cottas-ask-decode-failure |
— | — | — | — | unresolved — declared log_path missing: None |
local-cottas-corpus |
— | — | — | — | unresolved — declared log_path missing: None |
local-cottas-groupby-counts |
— | — | — | — | unresolved — declared log_path missing: None |
local-cottas-row-order |
— | — | — | — | unresolved — declared log_path missing: None |
local-graph-default-semantics |
— | — | — | — | unresolved — declared log_path missing: None |
local-graphs-api |
— | — | — | — | unresolved — declared log_path missing: None |
local-jsonld-regressions |
— | — | — | — | unresolved — declared log_path missing: None |
local-negative-test-vacuity |
— | — | — | — | unresolved — declared log_path missing: None |
local-parquet-footer |
— | — | — | — | unresolved — declared log_path missing: None |
local-parquet-footer-version-gate |
— | — | — | — | unresolved — declared log_path missing: None |
local-parser-unicode |
— | — | — | — | unresolved — declared log_path missing: None |
local-rdf12-semantics-tight |
— | — | — | — | unresolved — declared log_path missing: formal/fstar/ocaml-output/rdf12_semantics_tight.log |
local-serializer-unicode |
— | — | — | — | unresolved — declared log_path missing: None |
local-sparql-negative |
— | — | — | — | unresolved — declared log_path missing: None |
local-sparql-parser |
— | — | — | — | unresolved — declared log_path missing: None |
local-turtle-pretty |
— | — | — | — | unresolved — declared log_path missing: None |
mathml |
81 | 0 | 0 | 81 | docs/test-results/latest.json:mathml |
owl-profile-el |
— | — | — | — | unresolved — no committed log carries score lines for rl |
owl-profile-ql |
— | — | — | — | unresolved — no committed log carries score lines for rl |
owl-profile-rl |
— | — | — | — | unresolved — declared log_path missing: formal/fstar/ocaml-output/owl_results.log |
owl-semantics-direct |
— | — | — | — | unresolved — no committed log carries score lines for dl |
owl-syntax-dl |
— | — | — | — | unresolved — no score line matched in formal/fstar/ocaml-output/owl_syntax_dl_results.log |
owl-type-consistency |
— | — | — | — | unresolved — no committed log carries score lines for dl |
owl-type-inconsistency |
— | — | — | — | unresolved — no committed log carries score lines for dl |
owl-type-negative-entailment |
— | — | — | — | unresolved — no committed log carries score lines for dl |
owl-type-positive-entailment |
— | — | — | — | unresolved — no committed log carries score lines for dl |
qudt |
— | — | — | — | unresolved — no score line matched in formal/fstar/ocaml-output/qudt_results.log |
rdf-mt |
38 | 0 | 0 | 38 | suite-log:per-runner-arg:formal/fstar/ocaml-output/rdf_results.log (manifest log_path points at formal/fstar/ocaml-output/sparql_results.log, which does not carry this suite's score lines) |
rdf-n-quads |
87 | 0 | 0 | 87 | suite-log:per-runner-arg:formal/fstar/ocaml-output/rdf_results.log (manifest log_path points at formal/fstar/ocaml-output/sparql_results.log, which does not carry this suite's score lines) |
rdf-n-triples |
70 | 0 | 0 | 70 | suite-log:per-runner-arg:formal/fstar/ocaml-output/rdf_results.log (manifest log_path points at formal/fstar/ocaml-output/sparql_results.log, which does not carry this suite's score lines) |
rdf-trig |
356 | 0 | 0 | 356 | suite-log:per-runner-arg:formal/fstar/ocaml-output/rdf_results.log (manifest log_path points at formal/fstar/ocaml-output/sparql_results.log, which does not carry this suite's score lines) |
rdf-turtle |
313 | 0 | 0 | 313 | suite-log:per-runner-arg:formal/fstar/ocaml-output/rdf_results.log (manifest log_path points at formal/fstar/ocaml-output/sparql_results.log, which does not carry this suite's score lines) |
rdf-xml |
166 | 0 | 0 | 166 | suite-log:per-runner-arg:formal/fstar/ocaml-output/rdf_results.log (manifest log_path points at formal/fstar/ocaml-output/sparql_results.log, which does not carry this suite's score lines) |
rdfc10 |
86 | 0 | 0 | 86 | docs/test-results/latest.json:rdfc10 |
rif |
— | — | — | — | unresolved — no score line matched in formal/fstar/ocaml-output/rif_results.log |
rml |
— | — | — | — | unresolved — no score line matched in formal/fstar/ocaml-output/rml_results.log |
rml-io |
17 | 1 | 55 | 73 | suite-log:named-line:formal/fstar/ocaml-output/rml_io_results.log |
schematron |
8 | 0 | 0 | 8 | suite-log:named-line:formal/fstar/ocaml-output/schematron_results.log |
shacl-core |
98 | 0 | 0 | 98 | suite-log:named-line:formal/fstar/ocaml-output/shacl_results.log |
shacl-sparql |
22 | 0 | 0 | 22 | suite-log:named-line:formal/fstar/ocaml-output/shacl_sparql_results.log |
shacl12-core |
138 | 0 | 0 | 138 | suite-log:TOTAL-line:formal/fstar/ocaml-output/shacl12_core_results.log |
shacl12-node-expr |
142 | 0 | 0 | 142 | suite-log:TOTAL-line:formal/fstar/ocaml-output/shacl12_node_expr_results.log |
shacl12-rules |
11 | 0 | 0 | 11 | suite-log:TOTAL-line:formal/fstar/ocaml-output/shacl12_rules_results.log |
shacl12-rules-syntax |
62 | 0 | 0 | 62 | suite-log:TOTAL-line:formal/fstar/ocaml-output/shacl12_rules_syntax_results.log |
shacl12-sparql |
25 | 0 | 0 | 25 | suite-log:TOTAL-line:formal/fstar/ocaml-output/shacl12_sparql_results.log |
shex |
1182 | 0 | 0 | 1182 | docs/test-results/latest.json:shex |
shex-negative-syntax |
0 | 0 | 0 | 0 | docs/test-results/latest.json:shex_negative_syntax |
sparql11-entailment |
70 | 0 | 0 | 70 | suite-log:per-runner-arg:formal/fstar/ocaml-output/sparql_results.log |
sparql11-federated-query |
10 | 0 | 0 | 10 | suite-log:per-runner-arg:formal/fstar/ocaml-output/sparql_results.log |
sparql11-protocol |
53 | 0 | 0 | 53 | suite-log:per-runner-arg:formal/fstar/ocaml-output/sparql_results.log |
sparql11-query |
338 | 0 | 0 | 338 | suite-log:per-runner-arg:formal/fstar/ocaml-output/sparql_results.log |
sparql11-service-description |
3 | 0 | 0 | 3 | suite-log:per-runner-arg:formal/fstar/ocaml-output/sparql_results.log |
sparql11-update |
157 | 0 | 0 | 157 | suite-log:per-runner-arg:formal/fstar/ocaml-output/sparql_results.log |
tests-unit |
19 | 28 | 0 | 47 | docs/test-results/latest.json:tests_unit |
toan-matrix |
11 | 0 | 0 | 11 | docs/test-results/latest.json:toan_matrix |
vc |
117 | 0 | 0 | 117 | suite-log:TOTAL-line:formal/fstar/ocaml-output/vc_results.log |
vc-di-eddsa |
31 | 0 | 0 | 31 | docs/test-results/latest.json:vc_di_eddsa |
vc20-api |
59 | 0 | 0 | 59 | docs/test-results/latest.json:vc20_api |
xforms |
2 | 0 | 0 | 2 | docs/test-results/latest.json:xforms |
xml-conformance |
1447 | 0 | 1138 | 2585 | suite-log:named-line:formal/fstar/ocaml-output/xml_conformance_results.log |
xpath-unit |
— | — | — | — | unresolved — no committed log carries score lines for xpath_tests |
xslt |
87 | 0 | 1 | 88 | docs/test-results/latest.json:xslt |
xslt1-xalan |
— | — | — | — | unresolved — declared log_path missing: formal/fstar/ocaml-output/xslt1_xalan_results.log |
Filed as issue #315, sub-issue of the claim-discipline epic #313.