# Zipperposition

## Papers

- Logtk : A Logic ToolKit for Automated Reasoning and its Implementation regarding the library of terms, formulas, and logic algorithms
- Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond (PhD thesis) contains explanations about the prover’s structure and its inductive and arithmetic abilities as of 2015.
- Superposition with Structural Induction is a more up to date description of the induction and rewriting sub-systems.
- Superposition for Lambda-Free Higher-Order Logic describes the newer improvements to the higher-order reasoning techniques.

The slides of some of Simon Cruanes’ talks are on my page.

Some papers related to combinations of Superposition, higher-order logic, Induction, etc. can be found on Matryoshka’s website.