This is a simple parser for the pq-system as described in Chapter 2 of Gödel, Escher, Bach by Douglas R. Hofstadter.
(valid-theorem? '(- - p - - q - - - -))
(valid-theorem? '(- - p - - - q - - - - -))
(valid-theorem? '(- - p - - q - - - - -))
(valid-theorem? '(- p - - - q -))
(produce-theorem 2 3) -> '(- - p - - - q - - - - -)
(produce-theorem 4 5) -> '(- - - - p - - - - - q - - - - - - - - -)