@InProceedings{Di-05-a, author = {L.~Dixon}, title = {Interactive and Hierarchical Tracing of Techniques in {IsaPlanner}}, booktitle = {Proc.\ of UITP'05}, year = {2005} } @InProceedings{omega02, author = {The OMEGA Group}, title = {Proof Development with {\OMEGA}}, pages = {143--148}, booktitle = {Proc.\ of the 18th {Int.\ Conf.\ on {A}utomated {D}eduction (CADE-18)}}, publisher = {Springer}, series = {LNAI}, year = {2002}, number = {2392}} @InProceedings{quodlibet, author ={J.~Avenhaus and U.~K{\"u}hler and T.~Schmidt-Samoa and C.-P.~Wirth}, title ={How to Prove Inductive Theorems? {\QUODLIBET}!}, pages ={328--333}, year ={2003}, booktitle ={Proc.\ of the 19th {Int.\ Conf.\ on {A}utomated {D}eduction (CADE-19)}}, publisher ={Springer}, series ={LNAI}, number ={2741} } @INPROCEEDINGS{HuSe-96-a, AUTHOR = {D.~Hutter and C.~Sengler}, TITLE = {{INKA - The Next Generation}}, booktitle = {Proc.\ of the 13th {I}nternational {C}onference on {A}utomated {D}eduction (CADE--13)}, publisher = {Springer}, series = {LNAI}, year = 1996 } @Book{Paulson94, key = "Paulson", author = "L.C.~Paulson", title = "Isabelle: {A} Generic Theorem Prover", publisher = "Springer", series = "LNCS", year = "1994", keywords = "Isabelle", } @Misc{nuprl, title = "The Nuprl Open Logical Environment", author = "C.~Kreitz and L.~Lorigo and R.~Eaton and R.L.~Constable and S.F.~Allen", year = "2000", citeseer-references = "oai:CiteSeerPSU:223980; oai:CiteSeerPSU:337666; oai:CiteSeerPSU:348353; oai:CiteSeerPSU:348850; oai:CiteSeerPSU:582895; oai:CiteSeerPSU:141043", annote = "The Pennsylvania State University CiteSeer Archives", language = "en", oai = "oai:CiteSeerPSU:567660", rights = "unrestricted", subject = "C. Kreitz,L. Lorigo,R. Eaton,R. L. Constable,S. F. Allen The Nuprl Open Logical Environment", URL = "http://citeseer.ist.psu.edu/567660.html; http://www.cs.cornell.edu/Info/Projects/NuPrl/html/../documents/Allen/00cade-nuprl.pdf", } @InBook{B1, key = {B01}, author = {J.~Siekmann and C.~Benzm{\"u}ller and A.~Fiedler and A~Meier and I.~Normann and M.~Pollet}, booktitle = {Thirty Five Years of Automating Mathematics}, title = {Proof Development in {OMEGA}: The Irrationality of Square Root of 2}, publisher = {Kluwer Academic Publishers}, year = 2003, pages = {271-314} } @InProceedings{ChSo00, AUTHOR = {L.~Cheikhrouhou and V.~Sorge}, TITLE = {{PDS --- A Three-Dimensional Data Structure for Proof Plans}}, booktitle = {Proc.\ of the {Int.\ Conf.\ on Artificial and Computational Intelligence for Decision, Control and Automation} in Engineering and Industrial Applications (ACIDCA'2000)}, year = 2000, } @Article{J09, key = {J09}, author = {M.~H\"ubner and S.~Autexier and C.~Benzm{\"u}ller and A.~Meier}, title = {Interactive Theorem Proving with Tasks}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {103}, number = {C}, month = {November}, year = 2004, pages = {161-181}, } @Article{ags-2003-d-15, author ={C.-P.~Wirth}, title ={Descente Infinie + {D}eduction}, journal ={Logic J. of the IGPL}, year ={2004}, pages ={1--96}, volume ={12}, number ={1}, publisher ={Oxford University Press} } @phdthesis{sergediss, author = {S.~Autexier}, title = {Hierachical Context Reasoning}, year = {2003}, school = {Saarland University} } @InProceedings{W12, key = {W12}, author = {C.~Benzm{\"u}ller and A.~Meier and E.~Melis and M.~Pollet and V.~Sorge}, title = {Proof Planning: A Fresh Start?}, booktitle = {Proc.\ of the IJCAR 2001 Workshop: Future Directions in Automated Reasoning}, year = 2001, pages = {25--37} } @Article{MePoSo02, author = {A.~Meier and M.~Pollet and V.~Sorge}, title = {{Comparing Approaches to the Exploration of the Domain of Residue Classes}}, journal = {Journal of Symbolic Computation, Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems}, year = 2002, volume = 34, number = 4, pages = {287--306}, publisher = {Elsevier} } @InProceedings{lpar02, author = {J.~Siekmann and C.~Benzm{\"u}ller and A.~Fiedler and A.~Meier and M.~Pollet}, title = {Proof Development with {OMEGA}: Sqrt(2) is irrational}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 9th {Int.\ Conf., LPAR 2002}}, year = 2002, series = {LNAI}, number = 2514, publisher = {Springer}, pages = {367--387} } @phdthesis{multi, author = {Andreas Meier}, title = {Proof Planning with Multiple Strategies}, year = 2004, school = {Saarland Univ.} } @Article{VSE98, author = {Autexier, S. and Hutter, D. and Langenstein, B. and Mantel, H. and Rock, G. and Schairer, A. and Stephan, W. and Vogt, R. and Wolpers, A.}, title = {{VSE}: Formal methods meet industrial needs}, journal = "International Journal on Software Tools for Technology Transfer, Special issue on Mechanized Theorem Proving for Technology, Springer", year = {1998}, month = {september}, note = {}, } @Book{COQ, author = {Y.~Bertot and P.~Cast{\'e}ran}, title = {Interactive Theorem Proving and Program Development --- Coq'Art: The Calculus of Inductive Constructions}, publisher = {Springer}, year = 2004, series = {Texts in Theoretical Computer Science, An EATCS Series}, annote = {ISBN 3-540-20854-2} } @inproceedings{TPS, author = {P.B.~Andrews and M.~Bishop and C.E.~Brown}, title = {System Description: {TPS}: A Theorem Proving System for Type Theory.}, booktitle = {Proc.\ of the 17th {Int.\ Conf.\ on {A}utomated {D}eduction (CADE-17)}}, year = {2000}, pages = {164--169}, publisher = {Springer}, series = {LNCS} } @Article{MelisSiekmann99, author = {E.~Melis and J.~Siekmann}, title = {{Knowledge-Based Proof Planning}}, journal = {Artificial Intelligence}, year = 1999, volume = 115, number = 1, pages = {65-105} } @inproceedings{Huang94a, author = {X.~Huang}, title = {Reconstructing Proofs at the Assertion Level}, booktitle = {Proc.\ of the 12th {Int.\ Conf.\ on {A}utomated {D}eduction (CADE-12)}}, pages = {738--752}, series = {LNAI}, publisher = {Springer}, year = {1994} } @InProceedings{Fiedler:ijcai01, author = {A.~Fiedler}, title = {Dialog-driven Adaptation of Explanations of Proofs}, booktitle = {Proc.\ of the 17th {I}nternational {J}oint {C}onference on {A}rtificial {I}ntelligence ({IJCAI})}, pages = {1295--1300}, year = 2001, publisher = "Morgan Kaufmann", address = "Seattle, WA" }