Superposition @25
 

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