Crate cop

Data structures and algorithms for clausal and nonclausal connection proof search.

This crate provides a multitude of fast data structures and associated algorithms for connection proof search in first-order logic, such as formulas, literals, terms, substitutions, clauses, matrices, … This is significantly based on the work “Efficient Low-Level Connection Tableaux” (2015) by Cezary Kaliszyk, in particular the idea of offset terms/clauses.

This crate should allow you to build own, customised connection provers without having to do all the foundational work necessary otherwise.

Re-exports

• pub use fof::Fof;
• pub use offset::Offset;
• pub use role::Role;

Modules

• fof
  First-order formulas and various normal forms.
• lean
  Clausal proof search à la leanCoP.
• nano
  Nonclausal proof search à la nanoCoP.
• offset
  Offset objects.
• role
  Formula roles and mapping from roles to formulas.
• szs
  SZS ontologies.
• tptp
  TPTP parsing.

Structs

• App
  Application of argument(s) to a head.
• Args
  A sequence of arguments of type T.
• Clause
  Clause of literals L.
• Db
  A database maps (signed) literal heads P to contrapositives CP.
• Matrix
  A matrix is a conjunction of clauses C.
• Signed
  Wrapper around an object to store a sign (+/-) along it.
• Subst
  Map from variables (usize) to T that can be efficiently restored to earlier states.
• Symbol
  Shared string with fast cloning, hashing, and equality check.

Enums

• LitMat
  A litmat is either a literal or a matrix.
• PutRewind
  Rewind a T either by replacing it with some T or by rewinding it with another rewinder for T.
• Term
  First-order logic term.

Traits

• Rewind
  Restore the state of mutable data structures.

Functions

• nonfunctional
  Return the keys that are mapped to more than one different value.
• union1
  Remove all elements of v2 from v1 and append v2 to the result.
• union2
  Compute the union of two vectors, removing duplicates from the first one.

Type Aliases

• Lit
  Literal, i.e. application of term arguments (containing constants C and variables V) to predicate P.