Module resolution 

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₂:

    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

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());

Structs

Clause

A clause is a disjunction of literals: L₁ ∨ L₂ ∨ ... ∨ Lₙ.

Literal

A literal is an atomic formula or its negation.

ProverStats

Statistics for resolution proof search.

ResolutionProver

Resolution-based theorem prover.

ResolutionStep

A single resolution step in a proof.

Enums

ProofResult

Result of a resolution proof attempt.

ResolutionStrategy

Resolution proof strategy.

Functions

to_cnf

Convert a TLExpr to Clausal Normal Form (CNF).