Dynamic Superposition: A Framework for Propositional and First-Order Reasoning
- Speaker: Prof Christoph Weidenbach (Max Planck Institute, Saarbrucken)
- Host: Konstantin Korovin
- 11th July 2012 at 14:15 in Lecture Theatre 1.4, Kilburn Building
Although propositional logic is actually properly contained in first-order logic, it seems that the current prime calculi for propositional and first-order logic, CDCL and superposition, respectively, have not much in common. In this talk I will show that CDCL is an instance of a projection of superposition to propositional logic. This has interesting implications for both calculi.