@article{V01,
author= "A. Voronkov",
title={{How to optimize proof-search in modal logics: new methods of proving redundancy criteria in sequent calculi}},
journal="ACM Transactions on Computation Logic",
pages="1-34",
volume="1",
number="4",
month=Apr,
year="2001"}

@Book{RV01,
title = {{Handbook of Automated Reasoning}},
editor = "A. Robinson and A. Voronkov",
year = "2001",
publisher = "Elsevier and MIT Press"}

@Inbook{DV01,
title = {{The Inverse Method}},
author = "A. Degtyarev and A. Voronkov",
crossref = "RV01",
chapter = "4"}

@Inbook{bachmair+01,
title = {{Resolution Theorem Proving}},
author = "L. Bachmair and H. Ganzinger",
crossref = "RV01",
chapter = "2"}

@Inbook{DP01,
title = {{Rewriting}},
author = "N. Dershowitz and D. Plaisted",
crossref = "RV01",
volume=1,
chapter = "9"}

@Inbook{SRV01,
title = {{Term Indexing}},
author = "R. Sekar and I. Ramakrishnan and A. Voronkov",
crossref = "RV01",
volume=2,
chapter = "26"}

@Inbook{P01,
title = {{Logical Frameworks}},
author = "F. Pfenning",
crossref = "RV01",
volume=2,
chapter = "21"}

@Inbook{BG01,
title = {{Proof-Assistants Using Dependent Type Systems}},
author = "H. Barendregt and H. Geuvers",
crossref = "RV01",
volume=2,
chapter = "18"}

@Inbook{BW01,
title = {{Solving Numerical Constraints}},
author = "A. Bockmayr and V. Weispfenning",
crossref = "RV01",
chapter = "12"}

@article{T75,
title = {{Efficiency of a good but not linear set union algorithm}},
author = "R. Tarjan",
journal = "Journal of the ACM",
volume=22,
number=2,
year=1975,
pages="215-225"}

@article{af02,
title={{Dependent Types Ensure Partial Correctness of Theorem Provers}},
author="A. Appel and A. Felty",
journal="Journal of Functional Programming",
volume=14,
number=1,
pages="3-19",
month=jan,
year=2004}

@INPROCEEDINGS{pollackExtensibility,
  AUTHOR = {Robert Pollack},
  TITLE = {On Extensibility of Proof Checkers},
  BOOKTITLE = {Types for Proofs and Programs: International
                  Workshop TYPES'94, B\aa stad, June 1994, Selected
                  Papers},
  EDITOR = {Dybjer and Nordstrom and Smith},
  SERIES = {{LNCS}},
  VOLUME = 996,
  PAGES = {140--161},
  YEAR = 1995,
  PUBLISHER = {Springer-Verlag}
}

@inproceedings{aw92,
author="A. Aiken and E. Wimmers",
title = {{Solving Systems of Set Constraints}},
booktitle={Seventh Annual IEEE Symposium on Logic in Computer Science},
pages={329-340},
year={1992}}

@Article{PSS02,
    Author       = "Pelletier, F.J. and Sutcliffe, G. and Suttner, C.B.",
    Year         = "2002",
    Title        = "{The Development of CASC}",
    Journal      = "AI Communications",
    Volume       = "15",
    Number       = "2-3",
    Pages        = "79-90"
} 

@inproceedings{leberre+03,
author= "D. Le Berre and L. Simon",
title={{The essentials of the SAT 2003 competition}},
booktitle="Sixth International Conference on Theory and Applications of Satisfiability Testing",
volume=2919,
year=2003,
series="LNCS",
pages="452--467",
publisher="Springer-Verlag"}

@inproceedings{Contejean05+,
author="E. Contejean and P. Corbineau",
title={{Reflecting Proofs in First-Order Logic with Equality}},
booktitle={{20th International Conference on Automated Deduction}},
editor="R. Nieuwenhuis",
year=2005}

@inproceedings{corbineau05,
author="P. Corbineau",
title={{Deciding Equality in the Constructor Theory}},
booktitle={{Types for Proofs and Programs}},
publisher="Springer-Verlag",
year=2005}