tensorlogic-ir 0.1.0

Intermediate representation (IR) and AST types for TensorLogic
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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94

//! # Resolution-Based Theorem Proving
//!
//! This module implements Robinson's resolution principle for automated theorem proving.
//! Resolution is a refutation-based proof procedure: to prove `Γ ⊢ φ`, we show that
//! `Γ ∪ {¬φ}` is unsatisfiable by deriving the empty clause (⊥).
//!
//! ## Overview
//!
//! **Resolution** is a complete inference rule for first-order logic:
//! - Given clauses `C₁ ∨ L` and `C₂ ∨ ¬L`, derive resolvent `C₁ ∨ C₂`
//! - The empty clause (∅) represents a contradiction
//! - If ∅ is derived, the original clause set is unsatisfiable
//!
//! ## Key Components
//!
//! ### Literals
//! A literal is an atom or its negation:
//! - Positive literal: `P(x, y)`
//! - Negative literal: `¬P(x, y)`
//!
//! ### Clauses
//! A clause is a disjunction of literals:
//! - `P(x) ∨ Q(x) ∨ ¬R(y)`
//! - Empty clause: `∅` (contradiction)
//! - Unit clause: single literal
//!
//! ### Resolution Rule
//! From clauses `C₁ ∨ L` and `C₂ ∨ ¬L`, derive `C₁ ∨ C₂`:
//! ```text
//!     C₁ ∨ L    C₂ ∨ ¬L
//!     ───────────────────
//!         C₁ ∨ C₂
//! ```
//!
//! ## Algorithms
//!
//! 1. **Saturation**: Generate all resolvents until empty clause or saturation
//! 2. **Set-of-Support**: Focus resolution on specific clause set
//! 3. **Linear Resolution**: Chain resolutions from initial clause
//! 4. **Unit Resolution**: Only resolve with unit clauses (more efficient)
//!
//! ## Example
//!
//! ```rust
//! use tensorlogic_ir::{TLExpr, Term, Clause, Literal, ResolutionProver};
//!
//! // Clauses: { P(a), ¬P(a) }
//! // This is unsatisfiable (derives empty clause via direct resolution)
//! let p_a = Literal::positive(TLExpr::pred("P", vec![Term::constant("a")]));
//! let not_p_a = Literal::negative(TLExpr::pred("P", vec![Term::constant("a")]));
//!
//! let mut prover = ResolutionProver::new();
//! prover.add_clause(Clause::from_literals(vec![p_a]));
//! prover.add_clause(Clause::from_literals(vec![not_p_a]));
//!
//! let result = prover.prove();
//! assert!(result.is_unsatisfiable());
//! ```
//!
//! ## Module Layout
//!
//! - [`literal`]: `Literal` type and matching helpers.
//! - [`clause`]: `Clause` type with substitution, renaming, and subsumption.
//! - [`proof`]: Proof result, resolution step, strategy and statistics types.
//! - [`prover`]: [`ResolutionProver`] driving the different proof strategies.
//! - [`cnf`]: Simplified conversion from [`crate::TLExpr`] to clausal normal form.

pub mod clause;
pub mod cnf;
pub mod literal;
pub mod proof;
pub mod prover;

pub use clause::Clause;
pub use cnf::to_cnf;
pub use literal::Literal;
pub use proof::{ProofResult, ProverStats, ResolutionStep, ResolutionStrategy};
pub use prover::ResolutionProver;

#[cfg(test)]
use crate::expr::TLExpr;
#[cfg(test)]
use crate::term::Term;
#[cfg(test)]
use crate::unification::Substitution;

#[cfg(test)]
mod tests;

#[cfg(test)]
mod tests_first_order;

#[cfg(test)]
mod tests_subsumption;