mrs_proof/lib.rs
1//! Proof objects and TSTP output for automated theorem proving.
2//!
3//! After a refutation is found, this crate:
4//!
5//! 1. **Extracts** the proof DAG by tracing back from the empty clause
6//! through `ClauseSource::Inference` parent pointers ([`extract`]).
7//! 2. **Formats** the proof in TSTP format for verification by external
8//! tools ([`tstp`]).
9
10pub mod extract;
11pub mod tstp;