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.