Expand description
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
Modules
- First-order formulas and various normal forms.
- Clausal proof search à la leanCoP.
- Nonclausal proof search à la nanoCoP.
- Offset objects.
- Formula roles and mapping from roles to formulas.
- SZS ontologies.
- TPTP parsing.
Structs
- Application of argument(s) to a head.
- A sequence of arguments of type
T
. - Clause of literals
L
. - A database maps (signed) literal heads
P
to contrapositivesCP
. - A matrix is a conjunction of clauses
C
. - Wrapper around an object to store a sign (+/-) along it.
- Map from variables (
usize
) toT
that can be efficiently restored to earlier states. - Shared string with fast cloning, hashing, and equality check.
Enums
- A litmat is either a literal or a matrix.
- Rewind a
T
either by replacing it with someT
or by rewinding it with another rewinder forT
. - First-order logic term.
Traits
- Restore the state of mutable data structures.
Functions
- Return the keys that are mapped to more than one different value.
- Remove all elements of
v2
fromv1
and appendv2
to the result. - Compute the union of two vectors, removing duplicates from the first one.
Type Aliases
- Literal, i.e. application of term arguments (containing constants
C
and variablesV
) to predicateP
.