Module cop::lean

Clausal proof search à la leanCoP.

Re-exports

• pub use context::Context;
• pub use cuts::Cuts;
• pub use search::Search;

Modules

• context
  Path and lemmas.
• cuts
  Backtracking and restrictions thereof.
• search
  Clausal proof search.

Structs

• Contrapositive
  Clausal contrapositive for a literal lit with some inferred information about it.

Enums

• Proof
  A full proof for a literal, including subproofs.

Type Aliases

• Db
  Clausal database.
• Matrix
  A matrix of clauses.