25th Anniversary of Superposition: Status and Future

The development of the superposition calculus has been a breakthrough for reasoning in first-order logic with equality. The confluence of resolution with selection, ordered paramodulation, and unfailing completion reached a major milestone at CADE-10 in Kaiserslautern, with Bachmair/Ganzinger’s “On Restrictions of Ordered Paramodulation with Simplification”. We take this 25th anniversary of superposition, coinciding with the 25th  CADE, as an occasion to revisit the superposition calculus in a two-part tutorial.

Part 1: Basics and Implementation

Stephan Schulz

The first part  covers the foundations of superposition: reasoning in equational first-order logic, the Superposition calculus, and  its efficient implementation, including search algorithms, data structures, and search control.

  1. Supporting Material for Part 1

  2. The Superposition-based theorem prover E

Part 2: The Future

Christoph Weidenbach

The second part continues with extensions of superposition and current developments in the field,  including Hierarchic Superposition, Model Building and Superposition-Based Decision Procedures.

  1. Supporting Material for Part 2