Crate heyting 

heyting

Overview

heyting answers complex logical queries over a knowledge graph — multi-hop questions with AND, OR, NOT, and implication, like “things that are a mammal and eat fish but are not a cat”. It evaluates a query as a computation tree over atomic one-hop lookups, combining the resulting membership degrees with fuzzy-logic connectives. The engine is geometry-generic: anything that can answer a one-hop query as [0, 1] degrees (point embeddings from tranz, region embeddings from subsume, or the plain FuzzyKg here) plugs in through the AtomicScorer trait. Reach for it when you have trained KG embeddings and want interpretable complex-query answers without training a separate query model.

The logic is a typed algebra

Query degrees live in a residuated lattice, and the choice of lattice is a type parameter (Truth): Godel (min), Product, Lukasiewicz, or Viterbi (product with max, the best-derivation semiring). The lattice’s residuum a → b is the Heyting implication the crate is named for, exposed both as Truth::residuum and as the Query::Implication connective. Picking the algebra picks the logic with no runtime branch — and the negation each one induces is the load-bearing difference (see truth): Lukasiewicz gives the soft involutive ¬a = 1 − a that ranking wants, while Godel/Product give the genuine intuitionistic pseudo-complement.

Relationship to the ecosystem

This is the geometry-generic counterpart of tranz::query (CQD-Beam over point embeddings): any point or region model that implements AtomicScorer gets the same complex-query connectives over it.

Example

use heyting::{answer_query_topk, FuzzyKg, Godel, Query, QueryConfig};

// 0=animal 1=mammal 2=dog 3=cat; relation 0 = is_a.
let mut kg = FuzzyKg::new(4);
kg.add_edge(2, 0, 1, 1.0); // dog is_a mammal
kg.add_edge(3, 0, 1, 1.0); // cat is_a mammal
kg.add_edge(1, 0, 0, 1.0); // mammal is_a animal

// (dog is_a ?) AND (cat is_a ?) -> mammal.
let q = Query::intersection(vec![Query::anchor(2, 0), Query::anchor(3, 0)]);
let top = answer_query_topk::<Godel>(&kg, &q, &QueryConfig::default(), 1);
assert_eq!(top[0].0, 1);

Re-exports

pub use abduce::abduce;

pub use abduce::AbduceConfig;

pub use abduce::Hypothesis;

pub use calibration::AffineSigmoidCalibrator;

pub use calibration::CalibratedScorer;

pub use calibration::Calibrator;

pub use calibration::SoftmaxCalibrator;

pub use conformal::answer_set;

pub use conformal::answer_set_from_scored_pool;

pub use conformal::calibrate;

pub use conformal::empirical_coverage;

pub use conformal::ConformalError;

pub use conformal::ConformalThreshold;

pub use eval::answer_query_report;

pub use eval::crisp_answers;

pub use eval::hard_answer_metrics;

pub use eval::split_answers;

pub use eval::QueryAnswerReport;

pub use eval::QueryAnswers;

pub use eval::QueryMetrics;

pub use kg::FuzzyKg;

pub use provenance::explain_answer;

pub use provenance::Witness;

pub use provenance::WitnessError;

pub use prune::answer_query_topk_pruned;

pub use prune::CandidateSource;

pub use query::answer_query;

pub use query::answer_query_topk;

pub use query::AtomicScorer;

pub use query::Query;

pub use query::QueryConfig;

pub use query::RawProjection;

pub use query::RawScoreOrder;

pub use temporal::TemporalKg;

pub use temporal::TimeSet;

pub use temporal::TimeWindow;

pub use truth::Godel;

pub use truth::Lukasiewicz;

pub use truth::Product;

pub use truth::SelectiveOr;

pub use truth::Truth;

pub use truth::Viterbi;

Modules

abduce

Abductive hypothesis generation: the query that explains an answer set.

adapters

Adapters from ecosystem models to AtomicScorer.

calibration

Calibration wrappers for raw one-hop model scores.

conformal

Conformal answer sets: coverage-guaranteed query answering.

eval

Query-answering evaluation with the field-standard easy/hard answer split.

kg

A reference in-memory fuzzy knowledge graph.

provenance

Why-provenance witnesses: the proof behind a degree-path answer.

prune

Candidate-pruned query evaluation: the retrieval-backend seam.

query

The query algebra: a compositional Query evaluated over an AtomicScorer in a chosen Truth algebra.

temporal

Temporal knowledge graphs: time-scoped hops for the query engine.

truth

Truth-degree algebras: the residuated lattices that logical query answering composes in.