# Strix

**Repository Path**: jonas218/strix

## Basic Information

- **Project Name**: Strix
- **Description**: Strix 是一个纯 Rust 实现的 OWL 2 DL 推理引擎，基于 Hypertableau 算法。零外部依赖，覆盖 TBox / RBox / DBox / ABox 共 27/27 项推理任务，6 层自包含 crate 架构。
- **Primary Language**: Unknown
- **License**: Apache-2.0
- **Default Branch**: main
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2026-07-01
- **Last Updated**: 2026-07-02

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# Strix — OWL 2 DL Reasoner

**纯 Rust OWL 2 DL 推理引擎**，基于 Hypertableau 算法，对标 [HermiT](http://www.hermit-reasoner.com/)。支持类层次、属性特征、逆角色、基数限制、个体枚举等 OWL 2 全部核心特性。

## Quick Start

```rust
use strix::ir::*;
use strix::StrixReasoner;

let ontology = Ontology {
    tbox: vec![TBoxAxiom::SubClassOf(
        Concept::Named("Human".into()),
        Concept::Named("Mortal".into()),
    )],
    rbox: vec![],
    dbox: vec![],
    abox: vec![],
};

let mut reasoner = StrixReasoner::new();
reasoner.load_ontology(&ontology);
reasoner.classify();

assert!(reasoner.is_subsumed_by("Human", "Mortal"));
```

## Features

| 维度 | 任务 | 状态 |
|------|------|------|
| **TBox** | 类可满足性、包含、分类、等价类、不相交类、子类 | ✅ |
| **RBox** | 属性层次、属性可满足性、等价属性、定义域/值域、逆属性、传递属性 | ✅ |
| **DBox** | 数据属性层次、等价数据属性、定义域/值域、函数式数据属性 | ✅ |
| **ABox** | 实例检查、角色断言蕴含、SameAs、DifferentFrom、个体类型推导 | ✅ |
| **Meta** | 一致性检查、解释（单一 justification） | ✅ |

## 构建与运行

```bash
# 构建
cargo build --release

# 运行测试（109+ 个测试）
cargo test

# 代码检查
cargo clippy
```

### CLI 用法

```bash
# 分类本体并打印层次
cargo run -- classify ontology.ttl

# 检查蕴含
cargo run -- query ontology.ttl "Person ⊑ Thing"

# 解释蕴含
cargo run -- explain ontology.ttl "Person ⊑ Thing"
```

查询格式：

| 语法 | 含义 |
|------|------|
| `A ⊑ B` | 子类包含检查（Unicode ⊑） |
| `C(a)` | 实例检查 |
| `R(a, b)` | 角色断言蕴含 |

### 输入格式

支持三种标准 OWL 序列化格式：

| 格式 | 扩展名 | 解析器 |
|------|--------|--------|
| OWL Functional Syntax | `.ofn` | 手写递归下降 |
| OWL Manchester | `.omn` | 手写递归下降 |
| **Turtle** | `.ttl` | 手写 TTL 解析器 |
| **RDF/XML** | `.rdf` `.xml` `.owl` | 基于 quick-xml |

## 架构

Strix 采用 5 层架构，数据流单向：

```
Ontology → Normalizer → Tableau → Classifier → StrixReasoner → Result
  (L0)      (L1)        (L2)       (L3)         (L4)
```

| 层 | 模块 | 行数 | 职责 |
|-----|------|------|---------|
| L0 | `ir/` | ~350 | OWL 2 中间表示（Concept, Role, Axiom, Ontology） |
| L1 | `normalize/` | ~550 | NNF 转换、clausification、吸收 |
| L2 | `tableau/` | ~1,500 | Hypertableau 引擎（完成图、22 条规则、阻塞、回溯） |
| L3 | `classify/` | ~613 | 遍历分类（known-subsumer）+ 个体 realization |
| L4 | `reason/` | ~800 | 公开 API、缓存、结果导出、black-box 解释 |

### 关键设计

- **单 crate**（6 个规划 crate 已合并，用 `pub(crate)` 控制可见性）
- **`IndividualId = usize`** — ABox 内部索引
- **结构化 `Role::Inverse`** — 替代 `INV_` 前缀字符串
- **Hypertableau 算法** — 22 条确定性规则 + 3 条非确定性规则 + dependency-directed backjumping
- **known-subsumer 分类** — 拓扑排序 + transitive closure propagation + structural fast path

## 测试

```bash
cargo test                    # 109+ 个测试
cargo test --lib              # 库测试
cargo clippy                  # 0 警告
```

见 [docs/DESIGN.md](docs/DESIGN.md) 了解更多。

## License

Apache 2.0