Skip to main content

Module clause

tensorlogic_ir::resolution

Module clause 

Source
Expand description

§Clauses for Resolution

A Clause is a disjunction of literals. This module implements construction, tautology/Horn detection, substitution, renaming, and theta-subsumption used by the resolution prover.

Structs§

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