Struct ResolutionProver 

pub struct ResolutionProver {
    pub stats: ProverStats,
    /* private fields */
}

Resolution-based theorem prover.

Fields

stats: ProverStats

Statistics

Implementations

impl ResolutionProver

pub fn new() -> Self

Create a new resolution prover with default strategy.

pub fn with_strategy(strategy: ResolutionStrategy) -> Self

Create a prover with a specific strategy.

pub fn add_clause(&mut self, clause: Clause)

Add a clause to the initial clause set.

pub fn add_clauses(&mut self, clauses: Vec<Clause>)

Add multiple clauses.

pub fn reset(&mut self)

Reset the prover (clear clauses and stats).

pub fn resolve_first_order( &self, c1: &Clause, c2: &Clause, ) -> Vec<(Clause, Literal)>

Perform first-order binary resolution with unification.

This supports resolution on clauses with variables by using unification. Clauses are standardized apart before resolution to avoid variable conflicts.

Returns all possible resolvents with their MGUs.

Example

use tensorlogic_ir::{TLExpr, Term, Literal, Clause, ResolutionProver};

// {P(x)} and {¬P(a)} resolve to {} (empty clause) with MGU {x/a}
let p_x = Literal::positive(TLExpr::pred("P", vec![Term::var("x")]));
let not_p_a = Literal::negative(TLExpr::pred("P", vec![Term::constant("a")]));

let c1 = Clause::unit(p_x);
let c2 = Clause::unit(not_p_a);

let prover = ResolutionProver::new();
let resolvents = prover.resolve_first_order(&c1, &c2);

assert_eq!(resolvents.len(), 1);
assert!(resolvents[0].0.is_empty()); // Empty clause derived

pub fn prove(&mut self) -> ProofResult

Attempt to prove the clause set unsatisfiable using resolution.

Trait Implementations

impl Default for ResolutionProver

fn default() -> Self

Returns the “default value” for a type.