mrs-proof 0.3.0

Proof objects and TSTP output for automated theorem proving
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

# mrs-proof

Proof extraction and TSTP-formatted output.

Given the `ClauseId` of the empty clause and the clause store, traces parent pointers back through the derivation DAG and formats the result as a TSTP proof accepted by external verifiers.

## Key API

```rust
// Reconstruct the proof DAG (topologically sorted)
extract_proof(empty_id: ClauseId, clause_store: &ClauseStore) -> Vec<Clause>

// Render as TSTP
format_tstp(proof: &[Clause], symbols: &SymbolTable) -> String
```

### Example TSTP output

```
cnf(c0, axiom,    p(a),          file('input', ax1)).
cnf(c1, negated_conjecture, ~p(a), file('input', conj)).
cnf(c2, plain,    $false,        inference(resolution, [status(thm)], [c0,c1])).
```

## Dependencies

`mrs-core`, `mrs-szs`