From 92e8dcaa9dfc34f9ec9fa8e2f70ae709664cedba Mon Sep 17 00:00:00 2001 From: Michael Kohlhase Date: Thu, 7 Mar 2019 09:57:22 +0100 Subject: [PATCH] more --- .gitignore | 1 + tex/systems.bib | 1688 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 1689 insertions(+) create mode 100644 tex/systems.bib diff --git a/.gitignore b/.gitignore index 808412f..bd70657 100644 --- a/.gitignore +++ b/.gitignore @@ -10,3 +10,4 @@ auto *.run.xml *.synctex.gz *.toc +*.xml diff --git a/tex/systems.bib b/tex/systems.bib new file mode 100644 index 0000000..0f428b5 --- /dev/null +++ b/tex/systems.bib @@ -0,0 +1,1688 @@ +%Systems and applications +@inproceedings{comparing, + AUTHOR = {F. Wiedijk}, + TITLE = "{Comparing mathematical provers}", + BOOKTITLE = "{Proceedings of Mathematical Knowledge Management}", + YEAR = {2003}, + EDITOR = {A. Asperti and B. Buchberger and J. Davenport}, + PAGES = {188-202}, + PUBLISHER = {Springer}, +} + +@inproceedings{pvs, + AUTHOR = {S. Owre and J. Rushby and N. Shankar}, + TITLE = "{PVS: A Prototype Verification System}", + BOOKTITLE = "{11th International Conference on Automated Deduction (CADE)}", + YEAR = {1992}, + EDITOR = {D. Kapur}, + PAGES = {748--752}, + PUBLISHER = {Springer}, +} + +@InProceedings{pvs_shostak_decon, + author = "H. Rue{\ss} and N. Shankar", + title = "Deconstructing {S}hostak", + editor = "J. Halpern", + booktitle = "Logic in Computer Science", + year = "2001", + publisher = "IEEE Computer Society", + pages = "19--28", +} + +@misc{nasapvs, + author = "NASA Langley", + title = "{NASA PVS Library}", + note = "\url{http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html}", + year = 2014, +} + +@inproceedings{specware, + title = "{Specware: Formal Support for Composing Software}", + author = "Y. Srinivas and R. J{\"u}llig", + booktitle = "Mathematics of Program Construction", + editor = "B. M{\"o}ller", + year = 1995, + publisher = "Springer", +} + +@TECHREPORT{pvssemantics, + author = "S. Owre and N. Shankar", + title = "The formal semantics of {PVS}", + institution = "SRI International", + year = "1997", + number = "SRI-CSL-97-2", +} + +@book{nuprl, + author = "R. Constable and S. Allen and H. Bromley and W. Cleaveland and J. Cremer and R. Harper and D. Howe and T. Knoblock and N. Mendler and P. Panangaden and J. Sasaki and S. Smith", + title = "{Implementing Mathematics with the Nuprl Development System}", + publisher = "Prentice-Hall", + year = 1986, +} + +@incollection{nuprl_classes, + title = "{Nuprl's Class Theory and Its Applications}", + author = "R. Constable and J. Hickey", + booktitle = "{Foundations of Secure Computation}", + editor = "F. Bauer and R. Steinbruggen", + publisher = "{IOS Press}", + pages = "91--115", + year = "2000", +} + +@Inproceedings{delphin, + author = "A. Poswolsky and C. Sch{\"u}rmann", + title = "{System Description: Delphin - A Functional Programming Language for Deductive Systems}", + booktitle = "{International Workshop on Logical Frameworks and Metalanguages: Theory and Practice}", + year = "2008", + editor = "A. Abel and C. Urban", + pages = "135--141", + publisher = "ENTCS", +} + +@phdthesis{agdaphd, + author = "U. Norell", + title = "{Towards a practical programming language based on dependent type theory}", + school = "{Chalmers University of Technology and G{\"o}teborg University}", + year = "2007", +} + +@misc{agda, + author = "U. Norell", + title = "{The Agda WiKi}", + note = {\url{http://wiki.portal.chalmers.se/agda}}, + year = "2005", +} + +@InCollection{hol, + author = "M. Gordon", + editor = "G. Birtwistle and P. Subrahmanyam", + year = "1988", + title = "{HOL: A Proof Generating System for Higher-Order Logic}", + booktitle = "{VLSI Specification, Verification and Synthesis}", + pages = "73--128", + publisher = "{Kluwer-Academic Publishers}", +} + +@InCollection{holsemantics, + author = "M. Gordon and A. Pitts", + title = "{The HOL Logic}", + booktitle = "{Introduction to HOL, Part III}", + editor = "M. Gordon and T. Melham", + publisher = "Cambridge University Press", + year = "1993", + pages = "191--232", +} + +@Book{holbook, + author = "M. Gordon and T. Melham", + title = "{Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic}", + publisher = "Cambridge University Press", + year = "1993", +} + +@misc{hol4, + key = "HOL4", + author = "{HOL4 development team}", + note = "\url{http://hol.sourceforge.net/}", +} + +@misc{proofpower, + author = "R. Arthan", + title = "{ProofPower}", + note = "\url{http://www.lemma-one.com/ProofPower/}", +} + +@inproceedings{hollight, + author = "J. Harrison", + title ="{HOL Light: A Tutorial Introduction}", + pages = "265--269", + booktitle = "{Proceedings of the First International Conference on Formal Methods in Computer-Aided Design}", + year = "1996", + publisher = "Springer", +} + +@InProceedings{hollight_hints, + title = "{Automated Reasoning Service for HOL Light}", + author = "C. Kaliszyk and J. Urban", + booktitle = "Intelligent Computer Mathematics", + publisher = "Springer", + year = "2013", + editor = "J. Carette and D. Aspinall and C. Lange and P. Sojka and W. Windsteiger", + pages = "120--135", +} + +@INPROCEEDINGS{hollight_realclosedfield, + title = "A Proof-Producing Decision Procedure for Real Arithmetic", + author = "S. McLaughlin and J. Harrison", + booktitle = "Automated Deduction", + editor = "R. Nieuwenhuis", + publisher = "Springer", + year = 2005, + pages = "295--314" +} + +@Article{isabelle1, + author = "L. Paulson", + title = "{The Foundation of a Generic Theorem Prover}", + journal = "{Journal of Automated Reasoning}", + pages = "363--397", + volume = "5", + number = "3", + year = "1989", +} + +@InProceedings{isabelle2, + author = "L. Paulson", + title = "{Isabelle: The Next 700 Theorem Provers}", + year = "1990", + pages = "361--386", + editor = "P. Odifreddi", + publisher = "Academic Press", + booktitle = "Logic and Computer Science", +} + +@misc{isabellemanual, + author = "M. Wenzel", + title = "{The Isabelle/Isar Reference Manual}", + note = "\url{http://isabelle.in.tum.de/documentation.html}, Dec 3, 2009", + year = "2009", +} + +@Book{isabelle, + author = "L. Paulson", + title = "{Isabelle: A Generic Theorem Prover}", + publisher = "Springer", + series = "Lecture Notes in Computer Science", + volume = "828", + year = "1994", +} + +@Book{isabellehol, + author= {T. Nipkow and L. Paulson and M. Wenzel}, + title= "{Isabelle/HOL --- A Proof Assistant for Higher-Order Logic}", + publisher= {Springer}, + year= "2002" +} + +@misc{isabelle_zf, + author = "L. Paulson and M. Coen", + title = "{Zermelo-Fraenkel Set Theory}", + note = "{Isabelle distribution, ZF/ZF.thy}", + year = 1993, +} + +@InProceedings{isabelle_documentoriented, + title = "Isabelle as a Document-Oriented Proof Assistant", + author = "M. Wenzel", + booktitle = "Intelligent Computer Mathematics", + publisher = "Springer", + year = "2011", + editor = "J. Davenport and W. Farmer and J. Urban and F. Rabe", + pages = "244--259", +} + +@InProceedings{isabelle_jedit, + title = "{Isabelle/jEdit - {A} Prover {IDE} within the {PIDE} Framework}", + author = "M. Wenzel", + booktitle = "Intelligent Computer Mathematics", + year = "2012", + editor = "J. Jeuring and J. Campbell and J. Carette and G. Dos Reis and P. Sojka and M. Wenzel and V. Sorge", + pages = "468--471", +} + +@InProceedings{isabelle_async, + title = "{Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit}", + author = "M. Wenzel", + booktitle = "{User Interfaces for Theorem Provers}", + editor = "D. Aspinall and C. {Sacerdoti Coen}", + year = "2010", + publisher = "ENTCS", + pages = "101--114", +} + +@InProceedings{isar, + title = "{Isar - A Generic Interpretative Approach to Readable Formal Proof Documents}", + author = "M. Wenzel", + booktitle = "Theorem Proving in Higher Order Logics", + publisher = "Springer", + year = "1999", + editor = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th{\'e}ry", + pages = "167--184", +} + +@misc{isabellehol2, + author= {T. Nipkow and L. Paulson and M. Wenzel}, + title= "{Isabelle's Logics: HOL}", + year= "2004", + note= {\url{http://isabelle.in.tum.de/dist/Isabelle2004/doc/logics-HOL.pdf}} +} + +@InProceedings{isabelle_locales, + title = "{Locales -- a Sectioning Concept for Isabelle}", + author = "F. Kamm{\"u}ller and M. Wenzel and L. Paulson", + editor = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Thery", + year = "1999", + booktitle = "{Theorem Proving in Higher Order Logics}", + publisher = "Springer", + pages = "149--166" +} + +@InProceedings{isabelle_classes, + title = "{Constructive Type Classes in Isabelle}", + author = "F. Haftmann and M. Wenzel", + publisher = "Springer", + year = "2006", + booktitle = "TYPES conference", + editor = "T. Altenkirch and C. McBride", + pages = "160--174", +} + +@misc{isabelle_library, + title = "Isabelle Library", + key = "Isabelle", + year = 2008, + note = "\url{http://isabelle.in.tum.de/dist/library/index.html}", +} + +@InProceedings{isabellehol_codegen, + title = "{Code Generation via Higher-Order Rewrite Systems}", + author = "F. Haftmann and T. Nipkow", + booktitle = "Functional and Logic Programming", + publisher = "Springer", + year = "2010", + editor = "M. Blume and N. Kobayashi and G. Vidal", + pages = "103--117", +} + +@TechReport{isabelle_nuprl, + title = "{Formalization of Isabelle Meta Logic in NuPRL}", + author = "P. Naumov", + year = "1999", + institution = "Cornell", +} + +@InProceedings{proof_general, + title = "{Proof General: {A} Generic Tool for Proof Development}", + author = "D. Aspinall", + booktitle = "Tools and Algorithms for Construction and Analysis of Systems", + publisher = "Springer", + year = "2000", + editor = "S. Graf and M. Schwartzbach", + pages = "38--42", +} + +@InProceedings{lambdaprolog, + author = "D. Miller and G. Nadathur", + title = "Higher-order logic programming", + booktitle = "Proceedings of the Third International Conference on Logic Programming", + year = "1986", + editor = "E. Shapiro", + publisher = "Springer", + pages = "448--462", +} + +@Book{acl2, + author = "M. Kaufmann and P. Manolios and J Moore", + title = "{Computer-Aided Reasoning: An Approach}", + publisher = "Kluwer Academic Publishers", + year = "2000", +} + +@InProceedings{acl2sedan, + title = "{ACL2s: The ACL2 Sedan}", + author = "P. Dillinger and P. Manolios and D. Vroon and J. Strother Moore", + booktitle = "Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006)", + editor = "S. Autexier and C. Benzm{\"u}ller", + pages = "3--18", + year = "2007", +} + +@InProceedings{chiron_biform, + title = "{Biform Theories in Chiron}", + author = "W. Farmer", + booktitle = "Towards Mechanized Mathematical Assistants", + publisher = "Springer", + year = "2007", + editor = "M. Kauers and M. Kerber and R. Miner and W. Windsteiger", + pages = "66--79", + series = "Lecture Notes in Computer Science", + volume = "4573", +} + +@Article{tps, + title = "{TPS: A Theorem-Proving System for Classical Type Theory}", + author = "P. Andrews and M. Bishop and S. Issar and D. Nesmith and F. Pfenning and H. Xi", + journal = "{Journal of Automated Reasoning}", + pages = "321--353", + year = "1996", + volume = "16", + number = "3", +} + +@Article{imps, + author = "W. Farmer and J. Guttman and F. Thayer", + title = "{IMPS: An Interactive Mathematical Proof System}", + journal = "{Journal of Automated Reasoning}", + pages = "213--248", + volume = "11", + number = "2", + year = "1993", +} + +@InProceedings{lutins, + author = "{J. Guttman}", + title = "An Interface Logic for Verification Environments", + editor = "M. Archer and J. Joyce and K. Levitt and P. Windley", + booktitle = "{International Workshop on Higher Order Logic Theorem Proving and its Applications}", + publisher = "IEEE Computer Society Press", + year = "1991", +} + + +@InProceedings{alf, + author = "L. Magnusson and B. Nordstr{\"o}m", + title = "{The ALF proof editor and its proof engine}", + booktitle = "{Types for Proofs and Programs}", + editor = "H. Barendregt and T. Nipkow", + year = "1994", + series = "Lecture Notes in Computer Science", + publisher = "Springer", + volume = "806", + pages = "213--237", +} + +@Book{coqbook, + author= {Y. Bertot and P. Cast{\'e}ran}, + title= {Coq'Art: The Calculus of Inductive Constructions}, + publisher= {Springer}, + year= "2004", +} + +@techreport{coq, + author = "{Coq Development Team}", + title = "{The Coq Proof Assistant: Reference Manual}", + institution = "INRIA", + year = 2015 +} + +@misc{coq_library, + title = "Coq Library", + key = "Coq", + year = 2008, + note = "\url{http://coq.inria.fr/library-eng.html}", +} + +@incollection{coq_cct, + author = "G. Huet and A. Sa{\"\i}bi", + title = "Constructive category theory", + editor = "G. Plotkin and C. Stirling and M. Tofte", + booktitle = "{Proof, Language and Interaction: Essays in Honour of Robin Milner}", + year = "1998", + publisher = "MIT Press" +} +@techreport{coq_ssreflect, + title = "{A Small Scale Reflection Extension for the Coq system}", + author = "G. Gonthier and A. Mahboubi", + institution = "{INRIA}", + number = "{RR-6455}", + year = {2008}, +} +@InProceedings{gonthier_packaging, + title = "Packaging Mathematical Structures", + author = "F. Garillot and G. Gonthier and A. Mahboubi and L. Rideau", + booktitle = "Theorem Proving in Higher Order Logics", + publisher = "Springer", + year = "2009", + editor = "S. Berghofer and T. Nipkow and C. Urban and M. Wenzel", + pages = "327--342", +} + +@InProceedings{dedukti, + author = "M. Boespflug and Q. Carbonneaux and O. Hermant", + title = "The {$\lambda\Pi$}-calculus modulo as a universal proof language", + editor = "D. Pichardie and T. Weber", + booktitle = "Proceedings of PxTP2012: Proof Exchange for Theorem Proving", + pages = "28--43", + year = "2012", +} + +@misc{holide, + author = "A. Assaf and G. Burel", + title = "Holide", + note = "\url{https://www.rocq.inria.fr/deducteam/Holide/index.html}", + year = 2013, +} + +@inproceedings{coqine, + author = "M. Boespflug and G. Burel", + title = "{CoqInE: Translating the Calculus of Inductive Constructions into the lambda Pi-calculus Modulo}", + booktitle = "Proof Exchange for Theorem Proving", + editor = "D. Pichardie and T. Weber", + year = 2012, +} + +@InProceedings{lambdaPimodulo, + title = "Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo", + author = "D. Cousineau and G. Dowek", + booktitle = "Typed Lambda Calculi and Applications", + publisher = "Springer", + year = "2007", + editor = "S. Ronchi Della Rocca", + pages = "102--117", +} + +@misc{focalize, + author = "T. Hardin and others", + title = "The FoCaLiZe Essential", + note = "\url{http://focalize.inria.fr/}", + year = 2012 +} + +@Book{bmethod, + author = "J. Abrial", + title = "{The B-Book: Assigning Programs to Meanings}", + publisher = "Cambridge University Press", + year = "1996", +} + +@InProceedings{etb, + title = "{Tool Integration with the Evidential Tool Bus}", + author = "S. Cruanes and G. Hamon and S. Owre and N. Shankar", + booktitle = "Verification, Model Checking, and Abstract Interpretation", + publisher = "Springer", + year = "2013", + editor = "R. Giacobazzi and J. Berdine and I. Mastroeni", + pages = "275--294", +} + +@inproceedings{why3, + author = {F. Bobot and J. Filli{\^a}tre and C. March{\'e} and A. Paskevich}, + title = "{Why3: Shepherd Your Herd of Provers}", + booktitle = "{Boogie 2011: First International Workshop on Intermediate Verification Languages}", + year = 2011, + pages = {53--64}, +} + +@Book{caslmanual, + author = "{CoFI (The Common Framework Initiative)}", + title = "{CASL Reference Manual}", + year = "2004", + publisher = "Springer", + series = "LNCS", + volume = "2960", +} + +@incollection{obj, + author = "J. Goguen and Timothy Winkler and J. Meseguer and K. Futatsugi and J. Jouannaud", + title = "{Introducing OBJ}", + booktitle = "Applications of Algebraic Specification using {OBJ}", + publisher = "Cambridge", + editor = "J. Goguen and D. Coleman and R. Gallimore", + year = "1993", +} + +@Article{clear, + title = "The Semantics of {Clear}, a Specification Language", + author = "Joseph A. Goguen and Rod M. Burstall", + journal = "Journal of the ACM", + publisher = "Springer", + volume = "39", + number = "1", + pages = "95--146", + year = "1980", +} + +@InProceedings{aspinallaslplus, + author = "D. Aspinall", + title = "{Types, Subtypes, and ASL+}", + editor = "E. Astesiano and G. Reggio and A. Tarlecki", + booktitle = "{Recent Trends in Data Type Specification}", + publisher = "Springer", + year = "1994", + pages = "116--131", +} + +@InProceedings{asl, + title = "{A Kernel Language for Algebraic Specification and Implementation}", + author = "D. Sannella and M. Wirsing", + booktitle = "{Fundamentals of Computation Theory}", + publisher = "Springer", + year = "1983", + editor = "M. Karpinski", + pages = "413--427", +} + +@Article{extendedml, + title = "{The definition of extended ML: A gentle introduction}", + author = "S. Kahrs and D. Sannella and A. Tarlecki", + pages = "445--484", + journal = "Theoretical Computer Science", + year = "1997", + volume = "173", + number = "2", +} + +@Article{aslplus, + author = "D. Sannella and S. Sokolowski and A. Tarlecki", + title = "{Toward Formal Development of Programs from Algebraic Specifications: Parameterisation Revisited}", + journal = "{Acta Informatica}", + volume = "29", + number = "8", + year = "1992", + pages = "689--736", +} + +@inproceedings{maude, + author = "M. Clavel and S. Eker and P. Lincoln and J. Meseguer", + title = "Principles of {Maude}", + booktitle = "Proceedings of the First International Workshop on Rewriting Logic", + volume = "4", + editor = "J. Meseguer", + pages = "65--89", + year = "1996", +} + +@inproceedings{maude_rewriting, + author = "R. Bruni and J. Meseguer", + title = "Generalized rewrite theories", + booktitle = "Proceedings of ICALP '03.", + publisher = "Springer", + year = "2003", +} + +@INPROCEEDINGS{omega, + author = {C. Benzm{\"u}ller and L. Cheikhrouhou and D. Fehrer and A. Fiedler and X. Huang and M. Kerber and M. Kohlhase and K. Konrad and E. Melis and A. Meier and W. Schaarschmidt and J. Siekmann and V. Sorge}, + title = "{$\Omega$MEGA: Towards a mathematical assistant}", + booktitle = "{Proceedings of the 14th Conference on Automated Deduction}", + editor = {W. McCune}, + publisher = {Springer}, + year = {1997}, + pages = {252--255}, +} + +@InProceedings{mathweb, + author = "A. Franke and M. Kohlhase", + title = "{System Description: MATHWEB, an Agent-Based Communication Layer for Distributed Automated Theorem Proving}", + editor = "H. Ganzinger", + booktitle = "Automated Deduction", + pages = "217--221", + publisher = "Springer", + year = "1999", +} + +@InProceedings{matita, + title = "{Crafting a Proof Assistant}", + author = "A. Asperti and C. Sacerdoti Coen and E. Tassi and S. Zacchiroli", + publisher = "Springer", + year = "2006", + booktitle = "TYPES", + editor = "T. Altenkirch and C. McBride", + pages = "18--32", +} + +@Article{matita_refiner, + title = "{A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions}", + author = "A. Asperti and W. Ricciotti and C. Sacerdoti Coen and E. Tassi", + journal = "Logical Methods in Computer Science", + year = "2012", + number = "1", + volume = "8", +} + +@InProceedings{matita_hints, + title = "Hints in Unification", + author = "A. Asperti and W. Ricciotti and C. Sacerdoti Coen and E. Tassi", + booktitle = "Theorem Proving in Higher Order Logics", + publisher = "Springer", + year = "2009", + editor = "S. Berghofer and T. Nipkow and C. Urban and M. Wenzel", + pages = "84--98", +} + + +@Article{pientka_reconstruction, + title = "{An insider's look at {LF} type reconstruction: everything you (n)ever wanted to know}", + author = "B. Pientka", + journal = "J. Funct. Program", + year = "2013", + number = "1", + volume = "23", + pages = "1--37", +} + +@InProceedings{luther_reconstruction, + title = "{More On Implicit Syntax}", + author = "M. Luther", + booktitle = "Automated Reasoning", + publisher = "Springer", + year = "2001", + editor = "R. Gor{\'e} and A. Leitsch and T. Nipkow", + pages = "386--400", +} + +@InProceedings{mizar, + author = "A. Trybulec and H. Blair", + title = "{Computer Assisted Reasoning with MIZAR}", + editor = "A. Joshi", + booktitle = "Proceedings of the 9th International Joint Conference on Artificial Intelligence", + publisher = {Morgan Kaufmann}, + pages = "26--28", + year = "1985", +} +@Article{mizar_nutshell, + title = "{Mizar in a Nutshell}", + author = "A. Grabowski and A. Kornilowicz and A. Naumowicz", + year = "2010", + journal = "Journal of Formalized Reasoning", + volume = 3, + number = 2 +} +@article{mizar_tarski, + author = "A. Trybulec", + title = "{Tarski Grothendieck Set Theory}", + journal = "{Journal of Formalized Mathematics}", + year = "1989", + volume = "Axiomatics", +} +@Article{jaskowski_nd, + author = "S. Ja{\'s}kowski", + journal = "{Studia Logica}", + title = "{On the rules of suppositions in formal logic}", + volume = "1", + year = "1934", + pages = "5--32", +} +@misc{mizarmanual, + author = "E. Bonarska", + title = "An Introduction to {PC} Mizar", + year = "1990", + note = "\url{http://www.mizar.org/project/bonarska91.ps.gz}", +} +@misc{mizar_grammar, + author = "Mizar", + title = "{Grammar, version 7.11.02}", + year = "2009", + note = "http://mizar.org/language/mizar-grammar.xml" +} +@InProceedings{mizar_types, + title = "{Mizar's Soft Type System}", + author = "F. Wiedijk", + booktitle = "{Theorem Proving in Higher Order Logics}", + publisher = "Springer", + year = "2007", + volume = "4732", + editor = "K. Schneider and J. Brandt", + pages = "383--399", + series = "Lecture Notes in Computer Science", +} +@InProceedings{mizar_types_bancerek, + author = "G. Bancerek", + title = "{On the structure of Mizar types}", + series = "Electronic Notes in Theoretical Computer Science", + volume = "85", + number = "7", + pages = "69--85", + year = 2003, +} + +@misc{mml, + title = "{Mizar Mathematical Library}", + author = "Mizar Community", + note = "\url{http://mizar.org/library/}", + year = 1989 +} + +@InCollection{mizar_omdoc, + author = {G. Bancerek and M. Kohlhase}, + title = "{Towards a Mizar Mathematical Library in OMDoc Format}", + booktitle = "{From Insight to Proof: Festschrift in Honour of Andrzej Trybulec}", + editor = {R. Matuszewski and A. Zalewska}, + publisher = "{University of Bia{\l}ystok}", + year = {2007}, + series = "{Studies in Logic, Grammar and Rhetoric}", + pages = {265--275}, +} +@inproceedings{mizarwiki, + author = {J. Urban and J. Alama and P. Rudnicki and H. Geuvers}, + booktitle = {Intelligent Computer Mathematics}, + editor = {S. Autexier and J. Calmet and D. Delahaye and P. Ion and L. Rideau and R. Rioboo and A. Sexton}, + title = "{A Wiki for Mizar: Motivation, Considerations, and Initial Prototype}", + publisher = {Springer}, + year = {2010}, + pages = {455-469}, +} +@inproceedings{largeformalwikis, + author = {J. Alama and K. Brink and L. Mamane and J. Urban}, + booktitle = {Intelligent Computer Mathematics}, + editor = {J. Davenport and W. Farmer and J. Urban and F. Rabe}, + title = {Large Formal Wikis: Issues and Solutions}, + publisher = {Springer}, + pages = {133-148}, + year = {2011}, +} +@InProceedings{proofweb, + title = "{Web Interfaces for Proof Assistants}", + author = "C. Kaliszyk", + booktitle = "User Interfaces for Theorem Provers", + editors = "S. Autexier and C. Benzm{\"u}ller", + year = "2007", + pages = "49--61", +} +@InProceedings{pide, + title = "{Isabelle/jEdit - A Prover IDE within the PIDE Framework}", + author = "M. Wenzel", + booktitle = "Intelligent Computer Mathematics", + publisher = "Springer", + year = "2012", + editor = "Johan Jeuring and John A. Campbell and Jacques Carette and Gabriel Dos Reis and Petr Sojka and Makarius Wenzel and Volker Sorge", + pages = "468--471", +} + +@InProceedings{scunak, + title = "{Combining Type Theory and Untyped Set Theory}", + author = "C. Brown", + booktitle = "{International Joint Conference on Automated Reasoning}", + publisher = "Springer", + year = "2006", + editor = "U. Furbach and N. Shankar", + pages = "205--219", +} +@InProceedings{chadcombining, + title = "{Combining Type Theory and Untyped Set Theory}", + author = "C. Brown", + booktitle = "{International Joint Conference on Automated Reasoning}", + publisher = "Springer", + year = "2006", + editor = "U. Furbach and N. Shankar", + pages = "205--219", +} + +@inproceedings{beluga, + title = "{A Framework for Programming and Reasoning with Deductive Systems (System description)}", + author = "B. Pientka and J. Dunfield", + booktitle = "{International Joint Conference on Automated Reasoning}", + year = "2010", + note = "To appear", +} + +@Book{automathpapers, + title = "Selected Papers on Automath", + publisher = "North-Holland", + year = "1994", + editor = "R. P. Nederpelt and J. H. Geuvers and R. C. de Vrijer", + volume = "133", + series = "Studies in Logic and the Foundations of Mathematics", +} + +@InCollection{automath, + author = "N. de Bruijn", + title = "{The Mathematical Language AUTOMATH}", + booktitle = "{Proceedings of the Symposium on Automated Demonstration}", + editor = "M. Laudet", + pages = "29--61", + series = "Lecture Notes in Mathematics", + volume = "25", + publisher = "Springer", + year = "1970", +} + +@article{vampire, + author = {A. Riazanov and A. Voronkov}, + title = {The design and implementation of {Vampire}}, + journal = {AI Communications}, + volume = {15}, + pages = {91--110}, + year = 2002 +} + +@techreport{prover9, + author = "W. McCune", + title = "{Otter 3.3 Reference Manual}", + institution = "{Mathematics and Computer Science Division, Argonne National Laboratory}", + year = "2003", + number = "ANL/MCS-TM-263", + note = "\url{http://www.cs.unm.edu/~mccune/mace4/manual-examples.html}", +} + +@inproceedings{zenon, + author = {R. Bonichon and D. Delahaye and D. Doligez}, + title = "{Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs}", + booktitle = "{Logic for Programming, Artificial Intelligence, and Reasoning}", + editor = {N. Dershowitz and A. Voronkov}, + pages = {151--165}, + publisher = "Springer", + year = {2007}, +} + +@inproceedings{leo2, + title = "{LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)}", + author ="C. Benzm{\"u}ller and L. Paulson and F. Theiss and A. Fietzke", + year = "2008", + booktitle = "Automated Reasoning", + editor = "A. Armando and P. Baumgartner and G. Dowek", + publisher = "Springer", + pages = "162--170", +} + +@InProceedings{satallax, + title = "{Satallax: An Automatic Higher-Order Prover}", + author = "C. Brown", + booktitle = "Automated Reasoning", + editor = "B. Gramlich and D. Miller and U. Sattler", + publisher = "Springer", + year = "2012", + pages = "111--117", +} + +@inproceedings{paradox, + title ="{New Techniques that Improve MACE-style Finite Model Finding}", + author ="K. Claessen and N. Sorensson", + year = "2003", + booktitle = "CADE-19 Workshop on Model Computation - Principles, Algorithms, Applications" +} + +@InProceedings{spass, + author = "C. Weidenbach and U. Brahm and T. Hillenbrand and E. Keen and C. Theobalt and D. Topic", + title = "{SPASS Version 2.0}", + editor = "A. Voronkov", + booktitle = "Conference on Automated Deduction", + year = "2002", + publisher = "Springer", + pages = "275--279", +} + +@InProceedings{E, + title = "{System Abstract: E 0.61}", + author = "S. Schulz", + booktitle = "{International Joint Conference on Automated Reasoning}", + publisher = "Springer", + year = "2001", + editor = "R. Gor{\'e} and A. Leitsch and T. Nipkow", + pages = "370--375", +} + +@InProceedings{metitarski, + title = "{MetiTarski: An Automatic Prover for the Elementary Functions}", + author = "B. Akbarpour and L. Paulson", + booktitle = "Intelligent Computer Mathematics", + publisher = "Springer", + year = "2008", + editor = "S. Autexier and J. Campbell and J. Rubio and V. Sorge and M. Suzuki and F. Wiedijk", + pages = "217--231", +} + +@InProceedings{theorema, + title = "{Theorema 2.0: A System for Mathematical Theory Exploration}", + author = "W. Windsteiger", + booktitle = "International Congress on Mathematical Software", + publisher = "Springer", + year = "2014", + editor = "H. Hong and C. Yap", + pages = "49--52", +} + +@InProceedings{cvc4, + title = "{CVC4}", + author = "C. Barrett and C. Conway and M. Deters and L. Hadarean and D. Jovanovic and T. King and A. Reynolds and C. Tinelli", + booktitle = "Computer Aided Verification", + editor = "G. Gopalakrishnan and S. Qadeer", + publisher = "Springer", + year = "2011", + pages = "171--177", +} + +@inproceedings{z3, + author = {L. de Moura and N. Bj{\o}rner}, + title = "{Z3: An Efficient SMT Solver}", + booktitle = {Tools and Algorithms for the Construction and Analysis of Systems}, + editor = {C. Ramakrishnan and J. Rehof}, + pages = {337--340}, + year = {2008}, + publisher = {Springer} +} + +@InProceedings{yices, + title = "Yices 2.2", + author = "B. Dutertre", + booktitle = "Computer Aided Verification", + publisher = "Springer", + year = "2014", + editor = "A. Biere and R. Bloem", + pages = "737--744", +} + +@inproceedings{opentheory, + author = {J. Hurd}, + title = "{OpenTheory: Package Management for Higher Order Logic Theories}", + booktitle = "{Programming Languages for Mechanized Mathematics Systems}", + editor = {G. Dos Reis and L. Th{\'e}ry}, + pages = {31--37}, + publisher = "{ACM}", + year = 2009 +} + +@Article{klone, + author = "R. Brachman and J. Schmolze", + title = "{An Overview of the KL-ONE Knowledge Representation Scheme}", + journal = "Cognitive Science", + volume = "9", + number = "2", + year = "1985", +} + +@inproceedings{activemath, + title = "{ActiveMath: System Description}", + author = "E. Melis and E. Andr{\'e}s and G. Goguadze and P. Libbrecht and M. Pollet and C. Ullrich", + booktitle = "{Artificial Intelligence in Education}", + pages = "580--582", + publisher = "IOS Press", + year = 2001, +} + +@book{omdoc, + author = "M. Kohlhase", + title = "{OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2)}", + series = "{Lecture Notes in Artificial Intelligence}", + number = "4180", + publisher = "Springer", + year = "2006", +} + +@article{kohlhaseopenmath, + author = "M. Kohlhase", + title = "{OMDoc: An Infrastructure for OpenMath Content Dictionary Information}", + journal = "Bulletin of the ACM Special Interest Group on Symbolic and Automated Mathematics", + volume = "34", + pages = "43--48", + year = 2000 +} + +@INPROCEEDINGS{mathwebsearch, + author = {M. Kohlhase and I. {\c{S}}ucan}, + title = "{A Search Engine for Mathematical Formulae}", + booktitle = "{Artificial Intelligence and Symbolic Computation}", + pages = {241--253}, + year = {2006}, + editor = {T. Ida and J. Calmet and D. Wang}, + publisher = {Springer}, +} + +@INPROCEEDINGS{IK:flatsearch:12, + author = {M. Iancu and M. Kohlhase}, + title = "{Searching the Space of Mathematical Knowledge}", + booktitle = "{Mathematics Information Retrieval Workshop}", + year = {2012}, + editor = {M.Kohlhase and P. Sojka}, +} + +@INPROCEEDINGS{mathhub, + author = "M. Iancu and C. Jucovschi and M. Kohlhase and T. Wiesing", + title = "{System Description: MathHub.info}", + booktitle = "Intelligent Computer Mathematics", + editor = "S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban", + pages = "431--434", + publisher = "Springer", + year = {2014}, +} + +@Article{dlmf, + title = "{Technical Aspects of the Digital Library of Mathematical Functions}", + author = "B. Miller and A. Youssef", + journal = "{Annals of Mathematics and Artificial Intelligence}", + year = "2003", + volume = "38", + number = "1-3", + pages = "121--136", +} + +@misc{locutor, + author = {N. M{\"u}ller and M. Kohlhase}, + title = {{Fine-Granular Version Control \& Redundancy Resolution}}, + note = {To be submitted}, + year = {2008}, +} + +@InProceedings{stexide, + author = {C. Jucovschi and M. Kohlhase}, + title = "{sTeXIDE: An Integrated Development Environment for sTeX Collections}", + editor = {S. Autexier and J. Calmet and D. Delahaye and P. Ion and L. Rideau and R. Rioboo and A. Sexton}, + booktitle = "{Intelligent Computer Mathematics}", + series = {Lecture Notes in Artificial Intelligence}, + publisher = {Springer}, + number = {6167}, + year = {2010}, +} + +@InProceedings{latexml, + title = "{The LaTeXML Daemon: Editable Math on the Collaborative Web}", + author = "D. Ginev and H. Stamerjohanns and B. Miller and M. Kohlhase", + booktitle = "{Intelligent Computer Mathematics}", + publisher = "Springer", + year = "2011", + editor = "J. Davenport and W. Farmer and J. Urban and F. Rabe", + pages = "292--294", +} + +@Article{stex, + author = "M. Kohlhase", + title = "{Using {\LaTeX} as a Semantic Markup Format}", + journal = "Mathematics in Computer Science", + volume = "2", + number = "2", + pages = "279--304", + year = "2008", +} + +@inproceedings{planetary, + author = {M. Kohlhase and C. David and D. Ginev and A. Kohlhase and C. Lange and B. Matican and S. Mirea and V. Zholudev}, + title = "{The Planetary System: Web 3.0 \& Active Documents for STEM}", + note = {To appear at ICCS 2011 (finalist at the Executable Papers Challenge), see \url{https://svn.mathweb.org/repos/planetary/doc/epc11/paper.pdf}}, + year = 2011, +} + +@InProceedings{tntbase, + author = {V. Zholudev and M. Kohlhase}, + booktitle = "{Proceedings of Balisage: The Markup Conference 2009}", + title = "{TNTBase: a Versioned Storage for XML}", + year = "2009", + series = "{Balisage Series on Markup Technologies}", + volume = 3, + publisher = {Mulberry Technologies, Inc.}, +} + +@InProceedings{tntbase_virtual, + author = {V. Zholudev and M. Kohlhase}, + title = "{Scripting Documents with XQuery: Virtual Documents in TNTBase}", + booktitle = {Proceedings of Balisage: The Markup Conference}, + publisher = {Mulberry Technologies, Inc.}, + series = {Balisage Series on Markup Technologies}, + year = {2010} +} + +@misc{omdoc_pvs, + author = "M. Kohlhase and S. Owre", + title = "An {OMDoc} interface to {PVS}", + year = "2005", + note = "See \url{https://svn.mathweb.org/repos/mathweb.org/trunk/omdoc/projects/pvs/doc/index.html}" +} + +@TECHREPORT{openmath, + Author = {S. Buswell and O. Caprotti and D. Carlisle and M. Dewar and M. Gaetano and M. Kohlhase}, + title = "{The Open Math Standard, Version 2.0}", + institution = {The Open Math Society}, + year = 2004, + note = {See \url{http://www.openmath.org/standard/om20}}, +} +@Article{sts, + author = {J. Davenport}, + title = {A small {OpenMath} type system}, + journal = {Bulletin of the ACM Special Interest Group on Symbolic and Automated Mathematics (SIGSAM)}, + volume = {34}, + number = {2}, + pages = {16--21}, + year = 2000} + +@InProceedings{openmath_kohlhase_davenport, + title = "{Unifying Math Ontologies: A Tale of Two Standards}", + author = "J. Davenport and M. Kohlhase", + booktitle = "Intelligent Computer Mathematics", + year = "2009", + editor = "J. Carette and L. Dixon and C. Sacerdoti Coen and S. Watt", + pages = "263--278", + publisher = "Springer" +} +@InProceedings{openmath_hellstrom_binders, + title = "{Quantifiers and n-ary binders: an OpenMath standard enhancement proposal}", + author = "L. Hellstr{\"o}m", + bibdate = "2013-09-26", + bibsource = "DBLP, + http://dblp.uni-trier.de/db/conf/mkm/cicmws2013.html#Hellstrom13", + booktitle = "{Joint Proceedings of the MathUI, OpenMath, PLMMS, and ThEdu Workshops and Work in Progress at CICM}", + year = "2013", + editor = "C. Lange and D. Aspinall and J. Carette and J. Davenport and A. Kohlhase and M. Kohlhase and P. Libbrecht and P. Quaresma and F. Rabe and P. Sojka and I. Whiteside and W. Windsteiger", + publisher = "CEUR-WS.org" +} + +@misc{openmathtypes, + author = "O. Caprotti and A. Cohen", + title = "A Type System For OpenMath", + note = "See \url{http://www.openmath.org/cocoon/openmath/standard/}" +} + +@misc{omcds, + key = "OMCD", + title = "{OpenMath Content Dictionaries}", + note = "\url{http://www.openmath.org/cd/}", +} + +%editor = {D. Carlisle and P. Ion and R. Miner and N. Poppelier}, +@misc{mathml, + author = {R. Ausbrooks and S. Buswell and D. Carlisle and S. Dalmas and S. Devitt and A. Diaz and M. Froumentin and R. Hunter and P. Ion and M. Kohlhase and R. Miner and N. Poppelier and B. Smith and N. Soiffer and R. Sutor and S. Watt}, + title = "{Mathematical Markup Language (MathML) Version 2.0 (second edition)}", + year = {2003}, + note = {See \url{http://www.w3.org/TR/MathML2}}, +} +@misc{mathjax, + title = "{Accessible Pages with MathJax}", + author = "N. Soiffer", + note = "Design Science, Inc., \url{http://www.mathjax.org/resources/articles-and-presentations/accessible-pages-with-mathjax/}" +} + + +@TECHREPORT{mathml3, + author = "R. Ausbrooks and S. Buswell and D. Carlisle and G. Chavchanidze and S. Dalmas and S. Devitt and A. Diaz and S. Dooley and R. Hunter and P. Ion and M. Kohlhase and A. Lazrek and P. Libbrecht and B. Miller and R. Miner and C. Rowley and M. Sargent and B. Smith and N. Soiffer and R. Sutor and S. Watt", + title = "{Mathematical Markup Language (MathML) Version 3.0}", + institution = {World Wide Web Consortium}, + year = {2010}, + note = {See \url{http://www.w3.org/TR/MathML3}}, + editor = {D. Carlisle and P. Ion and R. Miner}, +} + +@TECHREPORT{mathml3:short, + author = {D. Carlisle and P. Ion and R. Miner (eds.)}, + title = "{Mathematical Markup Language (MathML) Version 3.0}", + institution = {World Wide Web Consortium}, + year = {2010}, + note = {See \url{http://www.w3.org/TR/MathML3}}, + editor = {D. Carlisle and P. Ion and R. Miner}, +} + +@InProceedings{omdoc_kenzo, + title = "{Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems}", + author = "J. Heras and V. Pascual and J. Rubio", + booktitle = "Intelligent Computer Mathematics", + publisher = "Springer", + year = "2009", + editor = "J. Carette and L. Dixon and C. Sacerdoti Coen and S. Watt", + pages = "467--473", +} + +@InProceedings{kenzo_integrating, + title = "{Integrating Multiple Sources to Answer Questions in Algebraic Topology}", + author = "J. Heras and V. Pascual and A. Romero and J. Rubio", + booktitle = "Intelligent Computer Mathematics", + publisher = "Springer", + year = "2010", + editor = "S. Autexier and J. Calmet and D. Delahaye and P. Ion and L. Rideau and R. Rioboo and A. Sexton", + pages = "331--335", +} + +@TECHREPORT{uri, + author = {T. Berners-Lee and R. Fielding and L. Masinter}, + title = "{Uniform Resource Identifier (URI): Generic Syntax}", + institution = {Internet Engineering Task Force}, + year = {2005}, + type = {RFC}, + number = {3986}, + url = {http://www.ietf.org/rfc/rfc3986.txt} +} + +@TECHREPORT{iri, + author = {M. Duerst and M. Suignard}, + title = "{Internationalized Resource Identifiers (IRIs)}", + institution = {Internet Engineering Task Force}, + year = {2005}, + type = {RFC}, + number = {3987}, + url = {http://www.ietf.org/rfc/rfc3987.txt} +} + +@TECHREPORT{curie, + author = "M. Birbeck and S. McCarron", + title = "{A syntax for expressing Compact URIs}", + institution = {World Wide Web Consortium}, + year = {2009}, + note = {See \url{http://www.w3.org/TR/2009/CR-curie-20090116/}}, +} + +@Article{cml, + author = "P. Murray-Rust and H. Rzepa", + title = "{Chemical Markup, XML and the Worldwide Web. Part 4. CML Schema}", + journal = "{Journal of Chemical Information and Computer Sciences}", + volume = "43", + number = "3", + pages = "757--772", + year = "2003", +} + +@misc{rdf, + author = "{RDF Core Working Group of the W3C}", + title = "{Resource Description Framework Specification}", + year = "2004", + note = "\url{http://www.w3.org/RDF/}" +} + +@misc{sparql, + author = "{W3C}", + title = "{SPARQL Query Language for RDF}", + year = "2008", + note = "\url{http://www.w3.org/TR/rdf-sparql-query/}" +} + +@TECHREPORT{json, + author = {T. Bray}, + title = "{The JavaScript Object Notation (JSON) Data Interchange Format}", + institution = {Internet Engineering Task Force}, + year = {2014}, + type = {RFC}, + number = {7159}, + url = {http://tools.ietf.org/html/rfc7159} +} + +@misc{xml, + author = "{W3C}", + title = "{Extensible Markup Language (XML)}", + year = "1998", + note = "\url{http://www.w3.org/XML}" +} + +@misc{xquery, + author = "{W3C}", + title = "{XQuery 1.0: An XML Query Language}", + year = "2007", + note = "\url{http://www.w3.org/TR/xquery/}" +} + +@misc{xpath, + author = "{W3C}", + title = "{XML Path Language}", + year = "1999", + note = "\url{http://www.w3.org/TR/xpath/}" +} + +@misc{xpointerframework, + author = "{W3C}", + title = "{XPointer Framework}", + year = "2002", + note = "\url{http://www.w3.org/TR/xptr-framework/}" +} + +@misc{owl, + author = "{W3C}", + title = "{OWL 2 Web Ontology Language}", + year = "2009", + note = "\url{http://www.w3.org/TR/owl-overview/}", +} + +@misc{relaxng, + key = "RELAXNG", + author = "J. Clark and M. Makoto", + title = "{RELAX NG Specification}", + note = "{By the Organization for the Advancement of Structured Information Standards (OASIS). \url{http://relaxng.org/}}", + year = "2001", +} + +@PhdThesis{rest, + author = "R. Fielding", + title = "{Architectural Styles and the Design of Network-based Software Architectures}", + school = "{University of California, Irvine}", + year = "2000", +} + +@misc{sql, + author = "{ANSI/ISO/IEC}", + title = "{9075:2003, Database Language SQL}", + year = "2003", +} + +@misc{svn, + author = "{Apache Software Foundation}", + title = "{Apache Subversion}", + note = "see http://subversion.apache.org/", + year = "2000", +} + +@misc{berkeleydb, + author = "Oracle", + title = "{Oracle Berkeley DB}", + note = "see \url{http://www.oracle.com/us/products/database/berkeley-db/db/index.html}", + year = "2010", +} + +@misc{berkeleydbxml, + author = "Oracle", + title = "{Oracle Berkeley DB XML}", + note = "see \url{http://www.oracle.com/us/products/database/berkeley-db/xml/index.html}", + year = "2010", +} + +@inproceedings{popcorn, + author = {P. Horn and D. Roozemond}, + title = "{OpenMath in SCIEnce: SCSCP and POPCORN}", + booktitle = {Intelligent Computer Mathematics}, + editor = "J. Carette and L. Dixon and C. Sacerdoti Coen and S. Watt", + year = {2009}, + pages = {474--479}, + publisher = {Springer}, +} + +@Manual{commoncriteria, + title = "{Common Criteria for Information Technology Security Evaluation}", + key = "Common Criteria", + organization = "ISO/IEC Standard 15408", + year = "1998", + note = "See \url{http://www.commoncriteriaportal.org/}", +} + +@Book{sml, + author = "R. Milner and M. Tofte and R. Harper and D. MacQueen", + title = "{The Definition of {S}tandard {ML}, {\rm Revised edition}}", + publisher = "{MIT Press}", + year = "1997", +} + +@misc{smlnj, + title = "{Standard ML of New Jersey}", + key = "SML", + note = "See \url{http://www.smlnj.org}" +} + +@misc{sml_library, + title = "{Standard ML Basis Library}", + key = "SML", + note = "See \url{http://www.standardml.org/Basis/}", + year = 1997, +} + +@Article{ml_mixin, + author = "A. Rossberg and D. Dreyer", + title = "{Mixin' Up the ML Module System}", + journal = "ACM Transactions on Programming Languages and Systems", + volume = "35", + number = "1", + year = "2013", +} + +@Book{java, + title = "{The Java Language Specification}", + author = "J. Gosling and W. Joy and G. Steele Jr.", + publisher = "{Addison-Wesley}", + year = "1996", +} + +@Book{scala, + title = "{Programming in Scala}", + author = "M. Odersky and L. Spoon and B. Venners", + year = "2007", + publisher = "artima", +} + +@InProceedings{scala_extractors, + title = "Matching Objects with Patterns", + author = "B. Emir and M. Odersky and J. Williams", + booktitle = "European Conference on Object-Oriented Programming", + publisher = "Springer", + year = "2007", + editor = "E. Ernst", + pages = "273--298", +} + +@misc{lift, + title = "Lift Web Framework", + author = "D. Pollak and et. al.", + year = "2007", + note = "\url{http://liftweb.net}", +} + +@misc{tiscaf, + title = "tiscaf http server", + author = "A. Gaydenko", + year = "2008", + note = "\url{http://gaydenko.com/scala/tiscaf/httpd/}", +} + +@misc{javadoc, + title = "{Javadoc Tool}", + key = "Javadoc", + note = "Part of the Java 2 SDK, see \url{http://java.sun.com/j2se/javadoc/}", + year = 2004 +} + +@misc{mathscheme, + author = "J. Carette and W. Farmer and R. O'Connor", + title = "The MathScheme Project", + year = 2010, + note = "\url{http://www.cas.mcmaster.ca/research/mathscheme}", +} + +@InProceedings{mathscheme_theoexp, + title = "{Theory Presentation Combinators}", + author = "J. Carette and R. O'Connor", + booktitle = "Intelligent Computer Mathematics", + publisher = "Springer", + year = "2012", + volume = "7362", + editor = "J. Jeuring and J. Campbell and J. Carette and G. Dos Reis and P. Sojka and M. Wenzel and V. Sorge", + pages = "202--215", +} + +@Article{tptp_old, + Author = "G. Sutcliffe and C. Suttner", + Year = "1998", + Title = "{The {TPTP} Problem Library: {CNF} Release v1.2.1}", + Journal = "Journal of Automated Reasoning", + Volume = "21", + Number = "2", + Pages = "177-203", +} + +@Article{tptp, + Author = "G. Sutcliffe", + Year = "2009", + Title = "{The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0}", + Journal = "Journal of Automated Reasoning", + Volume = "43", + Number = "4", + Pages = "337-362" +} + +@InProceedings{tptp_tff_arithmetic, + title = "{The TPTP Typed First-Order Form with Arithmetic}", + author = "G. Sutcliffe and S. Schulz and K. Claessen and P. Baumgartner", + booktitle = "Logic for Programming, Artificial Intelligence", + publisher = "Springer", + year = "2012", + editor = "N. Bj{\o}rner and A. Voronkov", + pages = "406--419", +} + +@InProceedings{tptp_pff, + title = "{TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism}", + author = "J. Blanchette and A. Paskevich", + booktitle = "Automated Deduction", + editor = "M. Bonacina", + publisher = "Springer", + year = "2013", + pages = "414--420", +} + +@inproceedings{tptp_booleansort, + author = "E. Kotelnikov and L. Kovacs and A. Voronkov", + title = "{A First Class Boolean Sort in First-Order Theorem Proving and TPTP}", + year = "2015", + booktitle = "Intelligent Computer Mathematics", + editor = "M. Kerber and J. Carette and C. Kaliszyk and F. Rabe and V. Sorge", + publisher = "Springer" +} + +@Article{casc, + Author = "F. Pelletier and G. Sutcliffe and C. Suttner", + Year = "2002", + Title = "{The Development of {CASC}}", + Journal = "{AI} Communications", + Volume = "15", + Number = "2-3", + Pages = "79-90" +} + +@InProceedings{maya, + author = "S. Autexier and D. Hutter and T. Mossakowski and A. Schairer", + title = "{The Development Graph Manager Maya (System Description)}", + editor = "H. Kirchner and C. Ringeissen", + booktitle = "Algebraic Methods and Software Technology, 9th International Conference", + year = "2002", + publisher = "Springer", + pages = "495--502", +} + +@InProceedings{fact, + title = "{The FaCT System}", + author = "I. Horrocks", + booktitle = "{Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX}", + publisher = "Springer", + year = "1998", + editor = "H. de Swart", + pages = "307--312", +} + +@Article{key, + author = "W. Ahrendt and T. Baar and B. Beckert and R. Bubel and M. Giese and R. H{\"a}hnle and W. Menzel and W. Mostowski and A. Roth and S. Schlager and P. Schmitt", + title = "{The KeY Tool}", + journal = "{Software and System Modeling}", + volume = "4", + pages = "32--54", + year = "2005", +} + +@Book{keybook, + editor = {B. Beckert and R. H\"ahnle and P. Schmitt}, + title = {Verification of Object-Oriented Software: The {KeY} Approach}, + series = {LNCS 4334}, + publisher = {Springer-Verlag}, + year = {2007} +} + +@book{sumo, + author = "A. Pease", + title = "Ontology: A Practical Guide", + publisher = "Articulate Software Press", + year = 2011 +} + +@misc{cyc, + author = "Cycorp", + title = "Cyc", + year = "1984", + note = "http://www.cyc.com/" +} + +@InProceedings{hets, + author = "T. Mossakowski and C. Maeder and K. L{\"u}ttich", + title = "{The Heterogeneous Tool Set}", + year = {2007}, + editor = "{O. Grumberg and M. Huth}", + booktitle = "{Tools and Algorithms for the Construction and Analysis of Systems 2007}", + volume = "4424", + pages = "519--522", + series = "{Lecture Notes in Computer Science}", +} + +@inproceedings{plato, + author = {M. Wagner and S. Autexier and C. Benzm{\"u}ller}, + editor = {S. Autexier and C. Benzm{\"u}ller}, + booktitle = "{7th Workshop on User Interfaces for Theorem Provers (UITP'06)}", + title = "{PLATO: A Mediator between Text-Editors and Proof Assistance Systems}", + publisher = {Elsevier}, + pages = {87-107}, + year = {2007}, +} + +@inproceedings{mspass, +author = {U. Hustadt and R. Schmidt}, +year = {2000}, +title = "{MSPASS: Modal Reasoning by Translation and First-Order Resolution}", +editor = {R. Dyckhoff}, +booktitle = "{Automated Reasoning with Analytic Tableaux and Related Methods, International Conference (TABLEAUX 2000)}", +pages = {67--71}, +} + +@InProceedings{tptpsigmakee, + title = "{Integration of the TPTPWorld into SigmaKEE}", + author = "S. Trac and G. Sutcliffe and A. Pease", + booktitle = "Practical Aspects of Automated Reasoning", + year = "2008", + volume = "373", + editor = "B. Konev and R. Schmidt and S. Schulz", + series = "CEUR Workshop Proceedings", +} + +@InProceedings{tramp, + title = "{System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level}", + author = "A. Meier", + booktitle = "Automated Deduction", + publisher = "Springer", + year = "2000", + series = "Lecture Notes in Computer Science", + volume = "1831", + editor = "D. McAllester", + pages = "460--464", +} + + +@Article{modula, + author = "N. Wirth", + title = "{Design and Implementation of Modula}", + journal = "{Software-Practice and Experience}", + volume = "7", + number = "1", + pages = "67--84", + year = "1977", +} + +@TechReport{chiron, + author = {W. Farmer}, + title = "{Chiron: A set theory with types, undefinedness, quotation, and evaluation}", + institution = {McMaster University}, + year = 2010, + type = {SQRL Report}, + number = 38, + url = {http://imps.mcmaster.ca/doc/chiron-tr.pdf}, +} + +@misc{maple, + title = "Maple", + key = "Maple", + author = "Maplesoft", + year = 2012, +} + +@misc{mathematica, + title = "Mathematica", + key = "Mathematica", + author = "Wolfram", + year = 2012, +} + +@manual{sage, + key = {Sage}, + author = {W. Stein and others}, + organization = {The Sage Development Team}, + title = "{Sage Mathematics Software}", + note = {\url{http://www.sagemath.org}}, + year = {2013}, +} + +@article{magma, + AUTHOR = {W. Bosma and J. Cannon and C. Playoust}, + TITLE = "{The Magma algebra system. I. The user language}", + JOURNAL = {Journal of Symbolic Computation}, + VOLUME = {24}, + NUMBER = {3-4}, + YEAR = {1997}, + PAGES = {235--265}, +} + +@book{axiom, + author = {R. Jenks and R. Sutor}, + title = "{AXIOM: The Scientific Computation System}", + publisher = {Springer}, + year = {1992}, +} + +@misc{maxima, + author = {Maxima}, + year = {2014}, + title = {Maxima, a Computer Algebra System. Version 5.34.1}, + note = {\url{http://maxima.sourceforge.net/}}, +} -- GitLab