tensorlogic_ir/resolution/
mod.rs

1//! # Resolution-Based Theorem Proving
2//!
3//! This module implements Robinson's resolution principle for automated theorem proving.
4//! Resolution is a refutation-based proof procedure: to prove `Γ ⊢ φ`, we show that
5//! `Γ ∪ {¬φ}` is unsatisfiable by deriving the empty clause (⊥).
6//!
7//! ## Overview
8//!
9//! **Resolution** is a complete inference rule for first-order logic:
10//! - Given clauses `C₁ ∨ L` and `C₂ ∨ ¬L`, derive resolvent `C₁ ∨ C₂`
11//! - The empty clause (∅) represents a contradiction
12//! - If ∅ is derived, the original clause set is unsatisfiable
13//!
14//! ## Key Components
15//!
16//! ### Literals
17//! A literal is an atom or its negation:
18//! - Positive literal: `P(x, y)`
19//! - Negative literal: `¬P(x, y)`
20//!
21//! ### Clauses
22//! A clause is a disjunction of literals:
23//! - `P(x) ∨ Q(x) ∨ ¬R(y)`
24//! - Empty clause: `∅` (contradiction)
25//! - Unit clause: single literal
26//!
27//! ### Resolution Rule
28//! From clauses `C₁ ∨ L` and `C₂ ∨ ¬L`, derive `C₁ ∨ C₂`:
29//! ```text
30//!     C₁ ∨ L    C₂ ∨ ¬L
31//!     ───────────────────
32//!         C₁ ∨ C₂
33//! ```
34//!
35//! ## Algorithms
36//!
37//! 1. **Saturation**: Generate all resolvents until empty clause or saturation
38//! 2. **Set-of-Support**: Focus resolution on specific clause set
39//! 3. **Linear Resolution**: Chain resolutions from initial clause
40//! 4. **Unit Resolution**: Only resolve with unit clauses (more efficient)
41//!
42//! ## Example
43//!
44//! ```rust
45//! use tensorlogic_ir::{TLExpr, Term, Clause, Literal, ResolutionProver};
46//!
47//! // Clauses: { P(a), ¬P(a) }
48//! // This is unsatisfiable (derives empty clause via direct resolution)
49//! let p_a = Literal::positive(TLExpr::pred("P", vec![Term::constant("a")]));
50//! let not_p_a = Literal::negative(TLExpr::pred("P", vec![Term::constant("a")]));
51//!
52//! let mut prover = ResolutionProver::new();
53//! prover.add_clause(Clause::from_literals(vec![p_a]));
54//! prover.add_clause(Clause::from_literals(vec![not_p_a]));
55//!
56//! let result = prover.prove();
57//! assert!(result.is_unsatisfiable());
58//! ```
59//!
60//! ## Module Layout
61//!
62//! - [`literal`]: `Literal` type and matching helpers.
63//! - [`clause`]: `Clause` type with substitution, renaming, and subsumption.
64//! - [`proof`]: Proof result, resolution step, strategy and statistics types.
65//! - [`prover`]: [`ResolutionProver`] driving the different proof strategies.
66//! - [`cnf`]: Simplified conversion from [`crate::TLExpr`] to clausal normal form.
67
68pub mod clause;
69pub mod cnf;
70pub mod literal;
71pub mod proof;
72pub mod prover;
73
74pub use clause::Clause;
75pub use cnf::to_cnf;
76pub use literal::Literal;
77pub use proof::{ProofResult, ProverStats, ResolutionStep, ResolutionStrategy};
78pub use prover::ResolutionProver;
79
80#[cfg(test)]
81use crate::expr::TLExpr;
82#[cfg(test)]
83use crate::term::Term;
84#[cfg(test)]
85use crate::unification::Substitution;
86
87#[cfg(test)]
88mod tests;
89
90#[cfg(test)]
91mod tests_first_order;
92
93#[cfg(test)]
94mod tests_subsumption;
tensorlogic_ir/resolution/mod.rs

tensorlogic_ir/resolution/
mod.rs
