Zipperposition

Repository on github

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.
• New Techniques for Higher-Order Superposition (draft)

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

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

API Documentation

• latest

• 2.0
• 1.6
• 1.5
• 1.3
• 1.2
• 1.1
• 1.0

(obsolete) high-level documentation