% theorem_provers.bib
% Aaron Stump, 3/17/99
%
% This file contains some references to works about 
% theorem provers.

@inproceedings{FORS01,
author = {J. Filli\^{a}tre and S. Owre and H. Rue\ss and N. Shankar},
title = {{ICS:} Integrated Canonizer and Solver},
booktitle = "13th International Conference on Computer-Aided Verification",
editor = "G. Berry and H. Comon and A. Finkel",
year = 2001}

@article{ROS98,
author= "J. Rushby and S. Owre and N. Shankar",
title={{Subtypes for Specifications: Predicate Subtyping in PVS}},
journal="IEEE Transactions on Software Engineering",
pages="709-720",
volume="24",
number="9",
month=Sep,
year="1998"}

@article{GW92,
author= "F. Giunchiglia and T. Walsh",
title={{A Theory of Abstraction}},
journal="Artificial Intelligence",
pages="323-390",
volume="56",
number="2-3",
month=Oct,
year="1992"}

@unpublished{OS99,
    AUTHOR = {Sam Owre and Natarajan Shankar},
    TITLE = {The Formal Semantics of {PVS}},
    MONTH = {March},
    YEAR = {1999},
    note = {http://www.csl.sri.com/papers/csl-97-2/}
}

@inproceedings{ORS92,
author = "S. Owre and J. Rushby and N. Shankar",
title = {{PVS: A Prototype Verification System}},
booktitle = "11th International Conference on Automated Deduction",
editor = "D. Kapur",
series = "LNAI",
publisher = "Springer-Verlag",
volume = "607",
pages = "748-752",
year = 1992}

@inproceedings{BR99,
author = "A. Bundy and J. Richardson",
title = {{Proofs about lists using ellipsis}},
booktitle = "Logic for Programming and Automated Reasoning, 6th International Conferenece",
editor = "H. Ganzinger and D. McAllester and A. Voronkov",
publisher = "Springer-Verlag",
pages = "1-12",
year = 1999}

@inproceedings{CRSS94,
author = "D. Cyrluk and S. Rajan and N. Shankar and M. K. Srivas",
title = {{Effective Theorem Proving for Hardware Verification}},
booktitle = "2nd International Conference on Theorem Provers in Circuit Design",
editor = "R. Kumar and T. Kropf",
series = "LNCS",
publisher = "Springer-Verlag",
volume = "901",
pages = "203-222",
year = 1994}

@book{KMM00a,
title={{Computer-Aided Reasoning: An Approach}},
author="M. Kaufmann and P. Manolios and J Moore",
publisher="Kluwer Academic",
year= "2000"}

@book{KMM00,
title={{Computer-Aided Reasoning: ACL2 Case Studies}},
author = "M. Kaufmann and P. Manolios and J Moore",
publisher = "Kluwer Academic",
year = "2000"}

@Inbook{MS00,
title = {{ IVY: A preprocessor and proof checker for first-order logic }},
author = "W. McCune and O. Shumsky",
crossref = "KMM00",
chapter = "16"}


@inproceedings{BN00,
author = "S. Berghofer and T. Nipkow",
title = {{ Proof terms for simply typed higher order logic }},
editors= "J. Harrison and M. Aagaard",
booktitle= "Theorem Proving in Higher Order Logics, 13th International Conference", 
publish="Springer-Verlag",
series = "LNCS",
volume="1869",
year=2000}

@article{DNS96,
author= "D. Detlefs and G. Nelson and J. Saxe",
title={{Simplify: the ESC Theorem Prover}},
journal="Draft Paper",
year="1996"}

@article{W99,
author= "W. Wong",
title={{Validation of HOL Proofs by Proof Checking}},
journal="Formal Methods in System Design",
volume="14",
number="2",
pages="193-212",
year="1999"}

@Book{GM93,
title = {{Introduction to HOL: a theorem proving environment for higher order logic}},
author = "M. Gordon and T. Melham",
year = "1993",
publisher = "Cambridge University Press"}

@Book{C86,
title = {{Implementing mathematics with the Nuprl proof development system}},
author = "R. Constable and the PRL group",
year = "1986",
publisher = "Prentice-Hall"}

@inproceedings{M96A,
author = "Z. Manna et al.",
title = {{STeP: Deductive-Algorithmic Verification of Reactive and Real-time Systems}},
booktitle = "8th International Conference on Computer-Aided Verification",
series = "LNCS",
publisher = "Springer-Verlag",
volume = "1102",
pages = "415-418",
year = 1996}

@techreport{M94,
author = "Z. Manna et. al",
institution = {{Computer Science Department, Stanford University}},
title = {{STeP: The Stanford Temporal Prover}},
number = "STAN-CS-TR-94-1518",
month = Jul,
year = "1994"}

@techreport{KPS95,
author = "S. Kromodimoeljo and B. Pase and M. Saaltink",
institution = {{ORA Canada, Ottawa, Ontario (http://www.ora.on.ca)}},
title = {{EVES Proof Checking and Browsing Final Report}},
number = "TR-95-5482-06",
year = "1995"}

@techreport{KP95,
author = "S. Kromodimoeljo and B. Pase",
institution = {{ORA Canada, Ottawa, Ontario (http://www.ora.on.ca)}},
title = {{Proof Logging Final Report}},
number = "TR-95-5471-05",
year = "1995"}

@inproceedings{BGGHHV92,
author = "R. Boulton and A. Gordon and M. Gordon and J. Harrison and J. Herbert and J. Van Tassel",
title = {{Experience with Embedding Hardware Description Languages in HOL}},
booktitle = "International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience",
editor = "V. Stavridou and T. F. Melham and R. T. Boute",
series = "IFIP Transactions",
publisher = "North-Holland/Elsevier",
volume = "A-10",
pages = "129-156",
year = 1992}

@inproceedings{H88,
author = "D. Howe",
title = {{Computational Metatheory in NuPRL}},
booktitle = "9th International Conference on Automated Deduction",
editor = "E. Lusk and R. Overbeek",
series = "LNCS",
publisher = "Springer-Verlag",
volume = "310",
pages = "238-257",
year = 1988}

@Inproceedings{BM81,
author = "R. Boyer and J. Moore",
editor = "R. Boyer and J. Moore",
booktitle = {{The Correctness Problem in Computer Science}},
publisher = "Academic Press",
title = {{Metafunctions: proving them correct and using them efficiently as new proof procedures}},
year = "1981",
pages = "103-184"}

@article{C99,
author="D. Cyrluk",
title ={{Private communication}},
year = "1999"}

@article{MW97,
author= "W. McCune and L. Wos",
title={{Otter. The CADE-13 competition incarnations}},
journal="Journal of Automated Reasoning",
volume="18",
number="2",
pages="211-20",
year="1997"}

@article{M97,
author= "W. McCune",
title={{Solution of the Robbins Problem}},
journal="Journal of Automated Reasoning",
volume="19",
number="3",
pages="263-276",
year="1997"}

@Inproceedings{BFFN97,
author = "P. Baumgartner and P. Frohlich and U. Furbach and W. Nejdl",
editor = "M. Pollack",
title = {{Semantically guided theorem proving for diagnosis applications}},
booktitle = {{15th International Joint Conference on Artificial Intelligence}},
publisher = "Morgan Kaufmann",
volume="1",
year = "1997",
pages = "460-5"}


@Book{Nipkow-Paulson-Wenzel2002,
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  publisher	= {Springer},
  series	= {LNCS},
  volume	= 2283,
  year		= 2002}

@INPROCEEDINGS{deplagne03a,
  AUTHOR = {E. Deplagne and C. Kirchner and H. Kirchner and Q. Nguyen},
  TITLE = {{Proof Search and Proof Check for Equational and Inductive Theorems}},
  BOOKTITLE = {{Conference on Automated Deduction - CADE-19, Miami, USA}},
  editor="F. Baader",
  year = 2003}

@inproceedings{BS04,
author = {Clark Barrett and Sergey Berezin},
title = {{CVC L}ite: A New Implementation of the Cooperating Validity Checker},
booktitle = {Proceedings of the 16th International Conference on Computer Aided Verification},
year = 2004
}

@Article{LH02,
  author =       {B.~L\"{o}chner and Th.~Hillenbrand},
  title =        {A Phytography of \textsc{Wald\-mei\-ster}},
  journal =      {AI Communications},
  year =         2002,
  volume =       15,
  number =       {2--3},
  pages =        {127--133}
}


@inproceedings{LH02a,
author = "B. L{\"{o}}chner and T. Hillenbrand",
title = {{The Next Waldmeister Loop}},
booktitle = "18th International Conference on Automated Deduction",
editor = "A. Voronkov",
pages = "486-500",
year=2002}

@manual{coq,
author={{The Coq Development Team}},
title={{The Coq Proof Assistant Reference Manual, Version V8.0}},
year=2004,
note="http://coq.inria.fr"}

@book{coqart,
author="Y. Bertot and P. Cast{\'e}ran",
title={{Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions}},
publisher="Springer Verlag",
year=2004}

@inproceedings{harrison06,
author="J. Harrison",
title={{Towards Self-verification of HOL Light}},
booktitle="International Joint Conference on Automated Reasoning",
year=2006,
editors="U. Furbach and N. Shankar"}

@misc{harrison06b,
author="J. Harrison",
title={{The HOL Light System Reference}},
year=2006,
url={http://www.cl.cam.ac.uk/~jrh13/hol-light/}}

@TECHREPORT{harrison-reflection,
        author          = "J. Harrison",
        title           = {{Metatheory and Reflection in Theorem Proving:
                           A Survey and Critique}},
        institution     = "SRI Cambridge",
        address         = "Millers Yard, Cambridge, UK",
        year            = 1995,
        number          = "CRC-053"}

@article{davis+79,
author="M. Davis and J. Schwartz",
title={{Metamathematical Extensibility for Theorem Verifiers and Proof-Checkers}},
journal="Computers and Mathematics with Applications",
volume=5,
year=1979,
pages="217--230"}

@Article{robinson-resolution,
  author =       {J. Alan Robinson},
  title =        {{A Machine-oriented Logic Based on the Resolution Principle}},
  journal =      {Journal of the Association for Computing Machinery},
  year =         1965,
  volume =       12,
  pages =        {23--41}
}

@inproceedings{nss-lt,
  author =       {A. Newell and J. C. Shaw and H. A. Simon},
  title =        {{Empirical Explorations of the Logic Theory Machine}},
  booktitle =      {Proceedings of the Western Joint Computer Conference},
  year =         1957,
  pages =        {218--239}
}

@inproceedings{ shankar02little,
  author = "N. Shankar",
  title = "Little engines of proof",
  booktitle = "Formal Methods - Getting IT Right",
  editor = "L.-H. Eriksson and P. Lindsay",
  pages = "1--20",
  publisher = "Springer-Verlag",
  year = "2002"
}

@Book{isabelle,
  author        = {T. Nipkow and L. Paulson and M. Wenzel},
  title         = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  publisher     = {Springer},
  series        = {LNCS},
  volume        = 2283,
  year          = 2002}

@inproceedings{ boyer90theorem,
    author = "R.~S. Boyer and J~S. Moore",
    title = "A Theorem Prover for a Computational Logic",
    booktitle = "Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany)",
    volume = "449",
    publisher = "Springer-Verlag",
    editor = "M. Stickel",
    pages = "1--15",
    year = "1990",
    url = "citeseer.ist.psu.edu/boyer90theorem.html" }

@techreport{ suttner96tptp,
    author = "Christian B. Suttner and Geoff Sutcliffe",
    title = "The {TPTP} Problem Library",
    number = "JCU-CS-96/9",
    month = "18",
    year = "1996",
    url = "citeseer.ist.psu.edu/article/sutcliffe99tptp.html" }


@inproceedings{constable94using,
  author = "R. Constable",
  title = "Using reflection to explain and enhance type theory",
  booktitle = "Proof and Computation, NATO ASI Series",
  year = "1994",
  publisher="Springer-Verlag",
  url = "citeseer.ist.psu.edu/constable94using.html" }

@inproceedings{hunt+05,
title={{Meta Reasoning in ACL2}},
author="W. Hunt and M. Kaufmann and R. Krug and J Moore and E. Smith",
booktitle="18th International Conference on Theorem Proving in Higher Order Logics",
editor="J. Hurd and T. Melham",
publisher="Springer-Verlag",
year=2005,
pages="163--178"}

@inproceedings{ruess97,
 author = {H. Rue{\ss}},
 title = {{Computational Reflection in the Calculus of Constructions and its Application to Theorem Proving}},
 booktitle = {Proceedings of the Third International Conference on Typed Lambda Calculi and Applications},
 year = {1997},
 pages = {319--335},
 publisher = {Springer-Verlag}
 }

@UNPUBLISHED{Ayache+06,
  author = {N. Ayache and J.-C. Filli\^atre},
  title = {{Combining the Coq Proof Assistant with First-Order Decision Procedures}},
  note = {Unpublished},
  month = {March},
  year = 2006,
  url = {http://www.lri.fr/~filliatr/publis/coq-dp.ps.gz}
}

@article{paulson99,
author= "L. Paulson",
title ={{A Generic Tableau Prover and Its Integration with Isabelle}},
journal = {Universal Computer Science},
volume=5,
number=3,
year=1999, 
pages="73--87"}

@InProceedings{Thery98,
  author = 	 {Th\'ery, Laurent},
  title = 	 {{A Certified Version of Buchberger's Algorithm}},
  booktitle =    {Procedings of the 15th International Conference on Automated Deduction, CADE 1998},
  editor = 	 {Kirchener, H. and Kirchner, C.},
  year = 	 {1998},
  publisher =    {Springer-Verlag}
}

@article{meng+06,
 author = {J. Meng and C. Quigley and L. Paulson},
 title = {{Automation for Interactive Proof: First Prototype}},
 journal = {Information and Computation},
 volume = {204},
 number = {10},
 year = {2006},
 pages = {1575--1596}
 }

@INPROCEEDINGS{HOLL,
        title           = {{HOL Light: A Tutorial Introduction}},
        author          = "John Harrison",
        booktitle       = "Proceedings of the First International Conference on
                           Formal Methods in Computer-Aided Design
                           ({FMCAD}'96)",
        editor          = "Mandayam Srivas and Albert Camilleri",
        year            = 1996,
        pages           = "265--269"
}

@article{weber+07,
title={{Efficiently Checking Propositional Refutations in HOL Theorem Provers}},author="T. Weber and H. Amjad",
journal="Journal of Applied Logic",
note="to appear, July 2007"}