Decision Procedures (WM 5)

master program

VO2 + VO1 + PS2  SS 2016  703620 + 703621 + 703622

Additional Material

Week 1

On the Complexity of Derivations in Propositional Calculus
G. Tseitin
Studies in Constructive Mathematics and Mathematical Logic 2, pp. 115 – 125, 1970
A Structure-Preserving Clause Form Translation
David A. Plaisted and Steven Greenbaum,
Journal of Symbolic Computation 2(3), pp. 293 – 304, 1986

Week 10

Theorem Proving in Arithmetic without Multiplication
D.C. Cooper
Chapter 5 in Machine Intelligence 7, Edinburgh University Press, pp. 91 – 100, 1972