@inproceedings{DBLP:conf/lfcs/ConstableM07,
  author    = {Robert L. Constable and
                 Wojciech Moczydlowski},
                   title     = {Extracting the Resolution Algorithm from a
Completeness
               Proof for the Propositional Calculus.},
                 booktitle = {LFCS},
                   year      = {2007},
                     pages     = {147-161},
                       ee        =
{http://dx.doi.org/10.1007/978-3-540-72734-7_11},
  crossref  = {DBLP:conf/lfcs/2007},
    bibsource = {DBLP, http://dblp.uni-trier.de}
    }

@proceedings{DBLP:conf/lfcs/2007,
  editor    = {Sergei N. Art{\"e}mov and
                 Anil Nerode},
                   title     = {Logical Foundations of Computer Science,
International Symposium,
               LFCS 2007, New York, NY, USA, June 4-7, 2007, Proceedings},
                 booktitle = {LFCS},
                   publisher = {Springer},
                     series    = {Lecture Notes in Computer Science},
                       volume    = {4514},
                         year      = {2007},
                           isbn      = {978-3-540-72732-3},
                             bibsource = {DBLP, http://dblp.uni-trier.de}
                             }