@STRING{JRH = "John Harrison"} @STRING{ACM = "Association for Computing Machinery"} @STRING{AP = "Academic Press"} @STRING{AW = "Addison-Wesley"} @STRING{BKH = "Birkh{\"a}user"} @STRING{CUP = "Cambridge University Press"} @STRING{MIT = "MIT Press"} @STRING{NH = "North-Holland"} @STRING{OUP = "Oxford University Press"} @STRING{PH = "Prentice-Hall"} @STRING{RKP = "Routledge \& Kegan Paul"} @STRING{SV = "Springer-Verlag"} @STRING{SIAM = "SIAM Publications, Philadelphia, PA"} @STRING{AMM = "The American Mathematical Monthly"} @STRING{CACM = "Communications of the ACM"} @STRING{CJ = "The Computer Journal"} @STRING{CTTCS = "Cambridge Tracts in Theoretical Computer Science"} @STRING{FM = "Fundamenta Mathematicae"} @STRING{FMSD = "Formal Methods in System Design"} @STRING{GTM = "Graduate Texts in Mathematics"} @STRING{IM = "Indagationes Mathematicae"} @STRING{IPL = "Information Processing Letters"} @STRING{JACM = "Journal of the ACM"} @STRING{JAR = "Journal of Automated Reasoning"} @STRING{JSC = "Journal of Symbolic Computation"} @STRING{JSL = "Journal of Symbolic Logic"} @STRING{LNCS = "Lecture Notes in Computer Science"} @STRING{LNM = "Lecture Notes in Mathematics"} @STRING{MA = "Mathematische Annalen"} @STRING{PHI = "Prentice-Hall International Series in Computer Science"} @STRING{PLMS2 = "Proceedings of the London Mathematical Society (2)"} @STRING{SL = "Studies in Logic and the Foundations of Mathematics"} @STRING{SLIB = "Synthese Library"} @STRING{TOPLAS = "ACM Transactions on Programming Languages and Systems"} @STRING{TCS = "Theoretical Computer Science"} @STRING{UTM = "Undergraduate Texts in Mathematics"} @STRING{ZML = "Zeitschrift f{\"u}r mathematische Logik und Grundlagen der Mathematik"} @STRING{CL = "University of Cambridge Computer Laboratory"} @STRING{CLA = "New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK"} @STRING{CLT = "Technical Report"} %****************************************************************************% % BOOKS ("Standalone") % %****************************************************************************% @BOOK{aberth, author = "O. Aberth", title = "Computable Analysis", publisher = "McGraw-Hill", year = 1980} @BOOK{abian-ba, author = "Alexander Abian", title = "Boolean Rings", publisher = "Branden Press, Boston", year = 1976} @BOOK{abian-linalg, author = "Alexander Abian", title = "Linear Associative Algebras", publisher = "Pergamon", year = 1971} @BOOK{abian-sets, author = "Alexander Abian", title = "The Theory of Sets and Transfinite Arithmetic", publisher = "W. B. Saunders Company", year = 1965, series = "Saunders Mathematics Books"} @BOOK{abramowitz-stegun, editor = "Milton Abramowitz and Irene A. Stegun", title = "Handbook of Mathematical Functions With Formulas, Graphs, and Mathematical Tables", publisher = "US National Bureau of Standards", year = 1964, series = "Applied Mathematics Series", volume = 55} @BOOK{ackermann-decision, author = "W. Ackermann", title = "Solvable Cases of the Decision Problem", publisher = NH, series = SL, year = 1954} @BOOK{adams-loustaunau, author = "William W. Adams and Philippe Loustaunau", title = "An introduction to Gr{\"o}bner Bases", publisher = "American Mathematical Society", series = "Graduate Studies in Mathematics", volume = 3, year = 1994} @BOOK{aho-dragon, author = "Alfred V. Aho and Ravi Sethi and Jeffrey D. Ullman", title = "Compilers: principles,techniques and tools", publisher = AW, year = 1986} @BOOK{aigner-thebook, author = "Martin Aigner and G{\"u}nter M. Ziegler", title = "Proofs from The Book", edition = "2nd", publisher = SV, year = 2001} @BOOK{akgul-ellipsoidal, author = "M. Akg{\"u}l", title = "Topics in relaxation and ellipsoidal methods", publisher = "Pitman", series = "Research notes in mathematics", volume = 97, year = 1984} @BOOK{anderson-lapack, author = "E. Anderson and Z. Bai and C. Bischof and J. Demmel and J. Dongarra and J. DuCroz and A. Greenbaum and S. Hammarling and A. McKenney and S. Ostrouchov and D. Sorensen", title = "LAPACK User's Guide", edition = "2nd", publisher = SIAM, year = 1995} @BOOK{andrews, author = "Peter B. Andrews", title = "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof", publisher = AP, year = 1986} @BOOK{arm-arm, editor = "Dave Jagger and David Seal", title = "{ARM} Architecture Reference Manual", publisher = AW, edition = "2nd", year = 2000} @BOOK{arnold-newtonhooke, author = "Vladimir Igorevich Arnol'd", title = "Huygens and Barrow, Newton and Hooke: pioneers in mathematical analysis and catastrophe theory from evolents to quasicrystals", publisher = BKH, year = 1990, note = "Translated from the Russian by Eric J.F. Primrose"} @BOOK{artmann, author = "Benno Artmann", title = "The Concept of Number: From Quaternions to Monads and Topological Fields", publisher = "Ellis Horwood", series = "Ellis Horwood series in Mathematics and its Applications", year = 1988, note = "Original German edition, `Der Zahlbegriff', published in 1983 by Vandenhoeck and Rupprecht, G{\"o}ttigen. Translated with additional exercises and material by H.B. Griffiths"} @BOOK{aubrey, author = "John Aubrey", title = "Brief Lives", year = 1813, note = "Recent edition by Secker and Warburg, 1960"} @BOOK{axford-concurrent, author = "Tom Axford", title = "Concurrent Programming: Fundamental Techniques for Real-Time and Parallel Software Design", publisher = "Wiley", series = "Wiley Series in Parallel Computing", year = 1990} @BOOK{baader-nipkow, author = "Franz Baader and Tobias Nipkow", title = "Term Rewriting and All That", publisher = CUP, year = 1998} @BOOK{back-refine, author = "Ralph Back", title = "Correctness Preserving Program Transformations: Proof Theory and Applications", publisher = "Mathematical Centre, Amsterdam", series = "Mathematical Centre Tracts", volume = 131, year = 1980} @BOOK{back-vonwright, author = "Ralph-Johan Back and Joakim von Wright", title = "Refinement Calculus: A Systematic Introduction", publisher = SV, series = "Graduate texts in computer science", year = 1998} @BOOK{baker, author = "Alan Baker", title = "Transcendental Number Theory", publisher = CUP, year = 1975} @BOOK{baker-concise, author = "Alan Baker", title = "A Concise Introduction to the Theory of Numbers", publisher = CUP, year = 1985} @BOOK{barendregt, author = "H. P. Barendregt", title = "The Lambda Calculus: Its Syntax and Semantics", publisher = NH, year = 1984, series = SL, volume = 103} @BOOK{barnes-mack, author = "D. W. Barnes and J. M. Mack", title = "An algebraic introduction to mathematical logic", publisher = SV, year = 1975, series = GTM, volume = 22} @BOOK{barrow-tipler, author = "John D. Barrow and Frank J. Tipler", title = "The Anthropic Cosmological Principle", publisher = OUP, year = 1988} @BOOK{barwise-etchemendy, author = "John Barwise and John Etchemendy", title = "The Language of First-Order Logic", edition = "second", publisher = "CSLI", year = 1991} @BOOK{basu-algorithms, author = "Saugata Basu and Richard Pollack and Marie-Fran{\c{c}}oise Roy", title = "Algorithms in Real Algebraic Geometry", publisher = SV, series = "Algorithms and COmputation in Mathematics", volume = 10, year = 2006} @BOOK{beeson, author = "M. J. Beeson", title = "Foundations of constructive mathematics: metamathematical studies", publisher = SV, year = 1984, series = "Ergebnisse der Mathematik und ihrer Grenzgebiete", volume = 3} @BOOK{bell-infinitesimal, author = "John L. Bell", title = "A Primer of Infinitesimal Analysis", publisher = CUP, year = 1998} @BOOK{bell-slomson, author = "J. L. Bell and T. S. Slomson", title = "Models and Ultraproducts", publisher = NH, year = 1969} @BOOK{benacerraf-putnam, author = "P. Benacerraf and H. Putnam", title = "Philosophy of mathematics: selected readings", edition = "2nd", publisher = CUP, year = 1983} @BOOK{benedetti-risler, author = "Riccardo Benedetti and Jean-Jacques Risler", title = "Real algebraic and semi-algebraic sets", publisher = "Hermann, Paris", year = 1990} @BOOK{bibel-book, author = "W. Bibel", title = "Automated theorem proving", publisher = "Vieweg Verlag", year = 1987, edition = "2nd"} @BOOK{biggs-graph, author = "Norman L. Biggs and E. Keith Lloyd and Robin J. Wilson", title = "Graph Theory 1736--1936", publisher = "Clarendon Press", year = 1976} @BOOK{bishop-bridges, author = "Errett Bishop and Douglas Bridges", title = "Constructive analysis", publisher = SV, year = 1985, series = "Grundlehren der mathematischen Wissenschaften", volume = 279} @BOOK{bochenski, author = "I. M. Boche{\'n}ski", title = "A History of Formal Logic", publisher = "Notre Dame", year = 1961} @BOOK{bochnak-realag, author = "J. Bochnak and M. Coste and M.-F. Roy", title = "Real Algebraic Geometry", publisher = SV, year = 1998, series = "Ergebnisse der Mathematik und ihrer Grenzgebiete", volume = 36} @BOOK{boizumault-prolog, author = "Patrice Boizumault", title = "The implementation of Prolog", publisher = "Princeton University Press", series = "Princeton series in computer science", year = 1993, note = "Translated from `Prolog: l'implantation' by A. M. Djamboulian and J. Fattouh"} @BOOK{boole-analysis, author = "George Boole", title = "The Mathematical Analysis of Logic", publisher = CUP, year = 1847} @BOOK{boolos-jeffrey, author = "George S. Boolos and Richard C. Jeffrey", title = "Computability and Logic", publisher = CUP, edition = "3rd", year = 1989, note = "First edition 1974"} @BOOK{boolos-provability, author = "George S. Boolos", title = "The Logic of Provability", publisher = CUP, year = 1995} @BOOK{borger-decision, author = "E. B{\"o}rger and E. Gr{\"a}del and Y. Gurevich", title = "The classical Decision Problem", publisher = SV, year = 2001} @BOOK{bourbaki-sets, author = "Nicolas Bourbaki", title = "Theory of sets", publisher = AW, year = 1968, series = "Elements of mathematics", note = "Translated from French {`Th{\'e}orie des ensembles'} in the series {`El{\'e}ments de math{\'e}matique'}, originally published by Hermann in 1968"} @BOOK{bourbaki-topology1, author = "Nicolas Bourbaki", title = "General topology", volume = 1, publisher = AW, year = 1966, series = "Elements of mathematics", note = "Translated from French {`Topologie Gen{\'e}rale'} in the series {`El{\'e}ments de math{\'e}matique'}, originally published by Hermann in 1966"} @BOOK{boyer-acl, author = "Robert S. Boyer and J Strother Moore", title = "A Computational Logic", publisher = AP, year = 1979, series = "ACM Monograph Series"} @BOOK{bridges-richmann, author = "Douglas Bridges and Fred Richman", title = "Varieties of Constructive Mathematics", publisher = CUP, year = 1987, series = "London Mathematical Society Lecture Note Series", volume = 97} @BOOK{brooks-manmonth, author = "Frederick P. Brooks", title = "The Mythical Man-Month", publisher = "Addison-Wesley", year = 1975} @BOOK{bundy-mm, author = "Alan Bundy", title = "The Computer Modelling of Mathematical Reasoning", publisher = AP, year = 1983} @BOOK{burge-recursive, author = "W. H. Burge", title = "Recursive Programming Techniques", publisher = AW, year = 1975} @BOOK{burkill1, author = "J. C. Burkill", title = "A first course in mathematical analysis", publisher = CUP, year = 1962, note = "New printing 1978"} @BOOK{burkill2, author = "J. C. Burkill and H. Burkill", title = "A second course in mathematical analysis", publisher = CUP, year = 1970, note = "New printing 1980"} @BOOK{burkill-lebesgue, author = "J. C. Burkill", title = "The {L}ebesgue Integral", publisher = CUP, year = 1965, series = "Cambridge Tracts in Mathematics and Mathematical Physics", volume = 44} @BOOK{burrill, author = "Claude W. Burrill", title = "Foundations of Real Numbers", publisher = "McGraw-Hill", year = 1967} @BOOK{cantor-contributions, author = "Georg Cantor", title = "Contributions to the founding of the Theory of Transfinite Numbers", publisher = "La Salle", year = 1915, note = "Edited and introduced by P. Jourdain; reprinted by Dover"} @BOOK{carnap-lsl, author = "Rudolf Carnap", title = "The Logical Syntax of Language", publisher = RKP, year = 1937, series = "International library of psychology, philosophy and scientific method", note = "Translated from `Logische Syntax der Sprache' by Amethe Smeaton (Countess von Zeppelin), with some new sections not in the German original"} @BOOK{carnap-pls, author = "Rudolf Carnap", title = "Philosophy and Logical Syntax", publisher = "Thoemmes Press", year = 1935, note = "Reprinted 1996"} @BOOK{carnap-symlog, author = "Rudolf Carnap", title = "Introduction to Symbolic Logic and its Applications", publisher = "Dover", year = 1958, note = "Translated by William H. Meyer and John Wilkinson; original German edition `Einf{\"u}hring in die symbolische Logik' published by Julius Springer in 1954"} @BOOK{carpenter-turingace, editor = "R. E. Carpenter and R. W. Doran", title = "{A}. {M}. {T}uring's {ACE} Report of 1946 and Other Papers", publisher = MIT, series = "Charles Babbage Institute Reprint Series of the History of Computing", volume = 10, year = 1986} @BOOK{ceruzzi-reckoners, author = "P. E. Ceruzzi", title = "Reckoners: the Prehistory of the Digital Computer, From Relays to the Stored Program Concept, 1933--1945", publisher = "Greenwood Press", year = 1983} @BOOK{chang-keisler, author = "C. C. Chang and H. J. Keisler", title = "Model Theory", edition = "3rd", publisher = NH, series = SL, volume = 73, year = 1992} @BOOK{chang-lee, author = "Chin-Liang Chang and Richard C. Lee", title = "Symbolic Logic and Mechanical Theorem Proving", publisher = AP, year = 1973} @BOOK{char-maple, author = "Bruce W. Char and Keith O. Geddes and Gaston H. Gonnet and Benton L. Leong and Michael B. Monogan and Stephen M. Watt", title = "First leaves: a tutorial introduction to {M}aple {V}", publisher = SV, year = 1992} @BOOK{charniak-mcdermott, author = "Eugene Charniak and Christopher K. Riesbeck and Drew V. McDermott", title = "Artificial intelligence programming", publisher = "Lawrence Erlbaum Associates", year = 1980} @BOOK{chou-book, author = "S.-C. Chou", title = "Mechanical Geometry Theorem Proving", publisher = "Reidel", year = 1988} @BOOK{church-book, author = "Alonzo Church", title = "The calculi of lambda-conversion", publisher = "Princeton University Press", year = 1941, series = "Annals of Mathematics Studies", volume = 6} @BOOK{church-logic1, author = "Alonzo Church", title = "Introduction to mathematical logic", publisher = "Princeton University Press", year = 1956} @BOOK{clarke-model, author = "E. M. Clarke and Orna Grumberg and Doron Peled", title = "Model Checking", publisher = MIT, year = 1999} @BOOK{clocksin-mellish, author = "William F. Clocksin and Christopher S. Mellish", title = "Programming in Prolog", publisher = SV, edition = "3rd", year = 1987} @BOOK{cohen-ehrlich, author = "Leon W. Cohen and Gertrude Ehrlich", title = "The Structure of the Real Number System", series = "The University Series in Undergraduate Mathematics", publisher = "Van Nostrand", year = 1963} @BOOK{cohen-book, author = "Paul J. Cohen", title = "Set Theory and the {C}ontinuum {H}ypothesis", publisher = "W. A. Benjamin, Inc.", year = 1966} @BOOK{cohn-ua, author = "P. M. Cohn", title = "Universal Algebra", publisher = "Harper and Row", series = "Harper's series in modern mathematics", year = 1965} @BOOK{constable-nuprlbook, author = "Robert Constable", title = "Implementing Mathematics with The {N}uprl Proof Development System", publisher = PH, year = 1986} @BOOK{conway, author = "J. H. Conway", title = "On Numbers and Games", publisher = AP, year = 1976, series = "L. M. S. Monographs", volume = 6} @BOOK{cooper-clancy, author = "Coug Cooper and Michael Clancy", title = "Oh! {P}ascal!", publisher = "W. W. Norton and Company", year = 1982} @BOOK{cornea-scientific, author = "Marius Cornea and John Harrison and Ping Tak Peter Tang", title = "Scientific Computing for {I}tanium Based Systems", publisher = "Intel Press", year = 2002} @BOOK{corry-structures, author = "Leo Corry", title = "Modern Algebra and the Rise of Mathematical Structures", publisher = BKH, year = 1996} @BOOK{cousineau-mauny, author = "Guy Cousineau and Michel Mauny", title = "The Functional Approach to Programming", publisher = CUP, year = 1998} @BOOK{cox-iva, author = "David Cox and John Little and Donal O'Shea", title = "Ideals, Varieties, and Algorithms", publisher = SV, year = 1992} @BOOK{curry-feys, author = "Haskell B. Curry and R. Feys", title = "Combinatory Logic", publisher = NH, year = 1958, series = SL} @BOOK{dahl-structured, author = "O. J. Dahl and E. W. Dijsktra and C. A. R. Hoare", title = "Structured Programming", publisher = AP, year = 1972} @BOOK{dalen-brouwer, editor = "Dalen, D. van", title = "{B}rouwer's {C}ambridge lectures on intuitionism", publisher = CUP, year = 1981} @BOOK{dalen-las, author = "Dalen, Dirk van", title = "Logic and Structure", edition = "3rd", publisher = SV, year = 1994} @BOOK{dalen-sets, author = "Dalen, Dirk van and H. C. Doets and Swart, H. de", title = "Sets, naive, axiomatic and applied: a basic compendium with exercises for use in set theory for non logicians, working and teaching mathematicians and students", publisher = "Pergamon", year = 1978, series = "International series in pure and applied mathematics", volume = 106, note = "Translated from Dutch `Verzamelingen', published by Oosthoek, Scheltema and Holkema, Utrecht"} @BOOK{dalen-monna, author = "Dalen, D. van and A. F. Monna", title = "Sets and Integration: an Outline of the Development", publisher = "Wolters-Noordhoff", year = 1972} @BOOK{dantzig-book, author = "G. B. Dantzig", title = "Linear Programming and Extensions", publisher = "Princeton University Press", year = 1963} @BOOK{davenport-ca, author = "James Harold Davenport and Y. Siret and E. Tournier", title = "Computer algebra: systems and algorithms for algebraic computation", publisher = AP, year = 1988} @BOOK{davenport-integration, author = "James Harold Davenport", title = "On the integration of algebraic functions", publisher = SV, year = 1981, series = LNCS, volume = 102} @BOOK{davey-priestley, author = "Brian A Davey and Hilary A. Priestley", title = "Introduction to lattices and order", publisher = CUP, year = 1990} @BOOK{davis-nsa, author = "M. Davis", title = "Applied nonstandard analysis", publisher = AP, year = 1977} @BOOK{davis-universal, author = "Martin Davis", title = "The Universal Computer: The Road from Leibniz to Turing", publisher = "W. W. Norton and Company", year = 2000, note = "Paperback edition (2001) entitled ``Engines of Logic: Mathematicians and the Origin of the Computer''"} @BOOK{davis-weyuker, author = "Martin D. Davis and Ron Sigal and Elaine J. Weyuker", title = "Computability, complexity, and languages: fundamentals of theoretical computer science", publisher = AP, edition = "2nd", year = 1994} @BOOK{debaere-interpretation, author = "Eddy H. Debaere and Campenhout, Jan M. Van", title = "Interpretation and Instruction Path Coprocessing", publisher = MIT, series = "Computer Systems Series", year = 1990} @BOOK{dedekind-irrat, author = "Richard Dedekind", title = "Stetigkeit und Irrationalzahlen", publisher = "Braunschweig", year = 1872} @BOOK{dedekind-was, author = "Richard Dedekind", title = "Was sind und was sollen die Zahlen?", publisher = "Vieweg, Braunschweig", year = 1888, note = "English translation in \cite{dedekind-essays}"} @BOOK{depree, author = "J. DePree and C. Swartz", title = "Introduction to Real Analysis", publisher = "Wiley", year = 1988} @BOOK{devaney-chaotic, author = "R. L. Devaney", title = "An Introduction to Chaotic Dynamical Systems", publisher = AW, year = 1987} @BOOK{devlin-descartes, author = "Keith Devlin", title = "Goodbye Descartes: the end of logic and the search for a new cosmology of the mind", publisher = "Wiley", year = 1997} @BOOK{devlin-sets, author = "Keith J. Devlin", title = "Fundamentals of Contemporary Set Theory", publisher = SV, series = "Universitexts", year = 1979} @BOOK{dijkstra-discipline, author = "E. W. Dijkstra", title = "A Discipline of Programming", publisher = PH, year = 1976} @BOOK{dijkstra-scholten, author = "E. W. Dijkstra and C. S. Scholten", title = "Predicate Calculus and Program Semantics", publisher = SV, year = 1990} @BOOK{dongarra-linpack, author = "J. Dongarra and J. Bunch and C. Moler and G. Stewart", title = "{LINPACK} User's Guide", publisher = SIAM, year = 1979} @BOOK{dreben-goldfarb, author = "Burton Dreben and Warren D. Goldfarb", title = "The Decision Problem: Solvable Cases of Quantificational Formulas", publisher = AW, year = 1979} @BOOK{dudley, author = "Richard M. Dudley", title = "Real analysis and probability", series = "The Wadsworth {\&} Brooks/Cole mathematics series", publisher = "Wadsworth {\&} Brooks/Cole", year = 1988} @BOOK{duffy-atp, author = "David A. Duffy", title = "Principles of Automated Theorem Proving", publisher = "Wiley", year = 1991} @BOOK{dumitriu, author = "Anton Dumitriu", title = "History of logic (4 volumes)", publisher = "Abacus Press", year = 1977, note = "Revised, updated and enlarged translation of the second edition of the Romanian `Istoria logicii' (Editura Didactic{\u{a}}, 1975) by Duiliu Zamfirescu, Dinu Giurc{\u{a}}neanu and Doina Doneaud"} @BOOK{ebbinghaus-etal, author = "Ebbinghaus, Heinz-Dieter and others", title = "Numbers", publisher = SV, year = 1990, series = GTM, volume = 123, note = "Translation of the 2nd edition of `Zahlen', 1988"} @BOOK{eisenbud-ca, author = "D. Eisenbud", title = "Commutative algebra with a view towards algebraic geometry", publisher = SV, year = 1995} @BOOK{enderton-logic, author = "Herbert B. Enderton", title = "A Mathematical Introduction to Logic", publisher = AP, year = 1972} @BOOK{enderton-sets, author = "Herbert B. Enderton", title = "Elements of Set Theory", publisher = AP, year = 1977} @BOOK{engel-philog, author = "Pascal Engel", title = "The Norm of Truth: An Introduction to the Philosophy of Logic", publisher = "Harvester Wheatsheaf", year = 1991, note = "Translated from the French {\em La norme du vrai} by Miriam Kochan and Pascal Engel"} @BOOK{engeler, author = "Erwin Engeler", title = "Foundations of Mathematics: Questions of Analysis, Geometry and Algorithmics", publisher = SV, year = 1993, note = "Original German edition {\em Metamathematik der Elementarmathematik} in the {\em Series Hochschultext}"} @BOOK{engelking, author = "Ryszard Engelking", title = "General Topology", series = "Sigma series in pure mathematics", volume = 6, publisher = "Heldermann Verlag", year = 1989} @BOOK{feferman-numbers, author = "Solomon Feferman", title = "The Number Systems: Foundations of Algebra and Analysis", series = "Addison-Wesley Series in Mathematics", publisher = AW, year = 1964} @BOOK{fermueller-resolution, author = "C. Fermueller and A. Leitsch and T. Tammet and N. Zamov", title = "Resolution Methods for the Decision Problem", publisher = SV, series = LNCS, volume = 679, year = 1993} @BOOK{ferrar-algebra, author = "W. L. Ferrar", title = "Algebra: a text-book of determinants, matrices, and algebraic forms", publisher = OUP, edition = "2nd", year = 1957} @BOOK{fike, author = "C. T. Fike", title = "Computer Evaluation of Mathematical Functions", publisher = PH, series = "Series in Automatic Computation", year = 1968} @BOOK{fitch-book, author = "Frederic Brenton Fitch", title = "Symbolic Logic: an introduction", publisher = "The Ronald Press Company, New York", year = 1952} @BOOK{fitting-book, author = "Melvin Fitting", title = "First-Order Logic and Automated Theorem Proving", publisher = SV, series = "Graduate Texts in Computer Science", year = 1990, note = "Second edition 1996"} @BOOK{forster-theoretical, author = "Thomas Forster", title = "Reasoning about theoretical entities", publisher = "World Scientific", series = "Advances in Logic", volume = 3, year = 2003} @BOOK{fowler, author = "H. W. Fowler", title = "A Dictionary of Modern English Usage", edition = "2nd, revised", publisher = OUP, year = 1965, note = "Revised by Sir Ernest Gowers"} @BOOK{franzen-godel, author = "Torkel Franz{\'e}n", title = "G{\"o}del's Theorem. An Incomplete Guide to its Use and Abuse", publisher = "A. K. Peters", year = 2005} @BOOK{franzen-inexhaustibility, author = "Torkel Franz{\'e}n", title = "Inexhaustibility", publisher = "Association for Symbolic Logic / A. K. Peters", series = "ASL Lecture Notes in Logic", volume = 16, year = 2002} @BOOK{franzen-thesis, author = "Torkel Franz{\'e}n", title = "Provability and Truth", publisher = "Almqvist and Wiksells", series = "Stockholm studies in philosophy", volume = 9, year = 1987} @BOOK{frege-beg, author = "Gottlob Frege", title = "Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens", publisher = "Louis Nebert, Halle", year = 1879, note = "English translation, `Begriffsschrift, a formula language, modeled upon that of arithmetic, for pure thought' in \cite{vanh}, pp. 1--82"} @BOOK{frege-arith, author = "Gottlob Frege", title = "Grundgesetze der Arithmetik begriffsschrift abgeleitet", publisher = "Jena", year = 1893, note = "Partial English translation by Montgomery Furth in `The basic laws of arithmetic. Exposition of the system', University of California Press, 1964"} @BOOK{freyd-allegories, author = "Peter J. Freyd and Andre Scedrov", title = "Categories, allegories", publisher = NH, year = 1990} @BOOK{friedman-pde, author = "Avner Friedman", title = "Generalized Functions and Partial Differential Equations", publisher = PH, year = 1963} @BOOK{gabbay-modal, author = "D. Gabbay and I. Hodkinson and M. Reynolds", title = "Temporal Logic", publisher = OUP, year = 1994} @BOOK{gardner-machines, author = "Martin Gardner", title = "Logic machines and diagrams", publisher = "McGraw-Hill", year = 1958} @BOOK{garey-johnson, author = "Michael R. Garey and David S. Johnson", title = "Computers and Intractibility: A Guide to the Theory of {NP}-Completeness", publisher = "Freeman and Company", year = 1979} @BOOK{garnier-proof, author = "Rowan Garnier and John Taylor", title = "{100\%} mathematical proof", publisher = "Wiley", year = 1996} @BOOK{gibbins-logpro, author = "Peter Gibbins", title = "Logic with {P}rolog", publisher = "Clarendon Press", year = 1988} @BOOK{girard-proof1, author = "Jean-Yves Girard", title = "Proof Theory and Logical Complexity, volume 1", publisher = "Bibliopolis, Napoli", series = "Studies in proof theory", year = 1987} @BOOK{girard-prat, author = "Jean-Yves Girard and Yves Lafont and Paul Taylor", title = "Proofs and Types", publisher = CUP, year = 1989, series = CTTCS, volume = 7} @BOOK{golan, author = "J. S. Golan", title = "The Theory of Semirings with Applications in Mathematics and Computer Science", publisher = "Longman", year = 1992} @BOOK{goldblatt, author = "Robert Goldblatt", title = "Topoi: The Categorial Analysis of Logic", edition = "Revised", publisher = NH, year = 1984, series = SL, note = "Original edition 1979"} @BOOK{goodstein-analysis, author = "R. L. Goodstein", title = "Recursive Analysis", publisher = NH, year = 1960, series = SL} @BOOK{goodstein-development, author = "R. L. Goodstein", title = "Development of mathematical logic", publisher = "Logos Press", year = 1971} @BOOK{goodstein-number, author = "R. L. Goodstein", title = "Recursive Number Theory", publisher = NH, year = 1957, series = SL} @BOOK{gordon-holbook, author = "Michael J. C. Gordon and Thomas F. Melham", title = "Introduction to {HOL}: a theorem proving environment for higher order logic", publisher = CUP, year = 1993} @BOOK{gordon-io, author = "Andrew D. Gordon", title = "Functional Programming and Input/Output", publisher = CUP, year = 1994, series = "Distinguished Dissertations in Computer Science"} @BOOK{gordon-lcfbook, author = "Michael J. C. Gordon and Robin Milner and Christopher P. Wadsworth", title = "{E}dinburgh {LCF}: A Mechanised Logic of Computation", publisher = SV, year = 1979, volume = 78, series = LNCS} @BOOK{gordon-plt, author = "Michael J. C. Gordon", title = "Programming Language Theory and its Implementation: applicative and imperative paradigms", publisher = PH, series = PHI, year = 1988} @BOOK{goubault-mackie, author = "Jean Goubault-Larrecq and Ian Mackie", title = "Proof Theory and Automated Deduction", publisher = "Kluwer", series = "Applied Logic Series", volume = 6, year = 1997} @BOOK{graf-thesis, author = "Peter Graf", title = "Term Indexing", publisher = SV, series = LNCS, volume = 1053, year = 1996, note = "Author's PhD thesis"} @BOOK{graham-concrete, author = "R. L. Graham and D. E. Knuth and O. Patashnik", title = "Concrete Mathematics: A Foundation for Computer Science", edition = "2nd", publisher = AW, year = 1994} @BOOK{graham-ramsey, author = "Ronald L. Graham and Bruce L. Rothschild and Joel H. Spencer", title = "Ramsey Theory", publisher = "Wiley", year = 1980} @BOOK{graham-secdbook, author = "Brian T. Graham", title = "The {SECD} Microprocessor: A verification case study", publisher = "Kluwer Academic Publishers", year = 1992, series = "Kluwer international series in engineering and computer science", volume = 178} @BOOK{grattan-guinness, editor = "I. Grattan-Guinness", title = "Companion Encyclopedia of the History and Philosophy of the Mathematical Sciences (2 vols)", publisher = RKP, year = 1994} @BOOK{grayling-pl, author = "A. C. Grayling", title = "An Introduction to Philosophical Logic", publisher = "Duckworth", year = 1990, note = "First edition published by Harvester Press, 1982"} @BOOK{grothendieck-ega4-20, author = "A. Grothendieck", title = "{\'E}l{\'e}ments de G{\'e}om{\'e}trie Alg{\'e}braique {IV}: {\'E}tude locale de sch{\'e}mas et des morphismes de sch{\'e}mas", series = "Publications Math{\'e}matiques", volume = 20, publisher = "IHES", year = 1964} @BOOK{grothendieck-sga4, author = "A. Grothendieck and M. Artin and J. L. Verdier", title = "Th{\'e}orie des Topos et Cohomologie {\'E}tale des Schemas (SGA 4), vol. 1", publisher = SV, series = LNM, volume = 269, year = 1972} @BOOK{grotschel-geometric, author = "M. Grotschel and L. Lovsz and A. Schrijver", title = "Geometric algorithms and combinatorial optimization", publisher = SV, year = 1993} @BOOK{haack-pol, author = "Susan Haack", title = "Philosophy of Logics", publisher = CUP, year = 1978} @BOOK{haggarty-analysis, author = "Rod Haggarty", title = "Fundamentals of Mathematical Analysis", publisher = AW, year = 1989} @BOOK{halmos, author = "P. R. Halmos", title = "Na{\"i}ve Set Theory", publisher = "Van Nostrand", year = 1960, series = "University series in undergraduate mathematics"} @BOOK{halmos-ba, author = "P. R. Halmos", title = "Lectures on Boolean algebras", publisher = "Van Nostrand", year = 1963, series = "Van Nostrand mathematical studies", volume = 1} @BOOK{halmos-givant, author = "Paul Halmos and Steven Givant", title = "Logic as algebra", publisher = "Mathematical Association of America", series = "Dolciani Mathematical Expositions", year = 1998} @BOOK{handy-cache, author = "Jim Handy", title = "The Cache Memory Book", publisher = "Morgan Kaufmann", year = 1997} @BOOK{hardy-wright, author = "G. H. Hardy and E. M. Wright", title = "An Introduction to the Theory of Numbers", edition = "5th", publisher = "Clarendon Press", year = 1979} @BOOK{harrison-thesis, author = JRH, title = "Theorem Proving with the Real Numbers", publisher = SV, year = 1998, note = "Revised version of author's PhD thesis"} @BOOK{hart-approximations, author = "John F. Hart and E. W. Cheney and Charles L. Lawson and Hans J. Maehly and Charles K. Mesztenyi and John R. Rice and Henry G. Thatcher and Christoph Witzgall", title = "Computer Approximations", publisher = "Robert E. Krieger", year = 1978} @BOOK{hegel-logic, title = "{H}egel's Logic (Being Part {I} of the Encyclopaedia of the Philosophical Sciences)", publisher = OUP, year = 1975, note = "Translated from German of Part I of `Enzyklopadie der philosophischen Wissenschaften im Grundrisse' by W. Wallace"} @BOOK{hellman-mwon, author = "Geoffrey Hellman", title = "Mathematics without numbers: towards a modal-structural interpretation", publisher = "Clarendon Press", year = 1989} @BOOK{henson-book, author = "Martin C. Henson", title = "Elements of functional languages", publisher = "Blackwell Scientific", year = 1987} @BOOK{henstock2, author = "Ralph Henstock", title = "The General Theory of Integration", publisher = "Clarendon Press", year = 1991} @BOOK{hertz-mechanics, author = "Heinrich Hertz", title = "Prinzipien der {M}echanik", publisher = "Johann Ambrosius Barth, Leipzig", year = 1894} @BOOK{hesselink-book, author = "Wim H. Hesselink", title = "Programs, Recursion and Unbounded Choice", publisher = CUP, series = CTTCS, volume = 27, year = 1992} @BOOK{heyting-constructivity, editor = "A. Heyting", title = "Constructivity in Mathematics: Proceedings of the Colloquium held at {A}msterdam 1957", publisher = NH, year = 1959, series = SL} @BOOK{higham-stability, author = "Nicholas J. Higham", title = "Accuracy and Stability of Numerical Algorithms", publisher = "SIAM, Philadelphia", year = 1996} @BOOK{hilbert-ackermann, author = "David Hilbert and Wilhelm Ackermann", title = "Principles of Mathematical Logic", publisher = "Chelsea", year = 1950, note = "Translation of `Grundz{\"u}ge der theoretischen Logik', 2nd edition (1938; first edition 1928); translated by Lewis M. Hammond, George G. Leckie and F. Steinhardt; edited with notes by Robert E. Luce"} @BOOK{hilbert-bernays2, author = "D. Hilbert and P. Bernays", title = "Grundlagen der {M}athematik, vol. 2", publisher = SV, year = 1939} @BOOK{hilbert-fgeom, author = "David Hilbert", title = "Grundlagen der Geometrie", publisher = "Teubner", year = 1899, note = "English translation `Foundations of Geometry' published in 1902 by Open Court, Chicago"} @BOOK{hill-godel, author = "P. M. Hill and J. W. Lloyd", title = "The {G\"o}del Programming Language", publisher = MIT, year = 1994} @BOOK{hindley-seldin, author = "J. Roger Hindley and Jonathan P. Seldin", title = "Introduction to Combinators and {$\lambda$}-Calculus", publisher = CUP, year = 1986, series = "London Mathematical Society Student Texts", volume = 1} @BOOK{hintikka-philos, author = "Jaakko Hintikka", title = "The Philosophy of Mathematics", publisher = OUP, year = 1969, series = "Oxford Readings in Philosophy"} @BOOK{hintikka-revisited, author = "Jaakko Hintikka", title = "The principles of mathematics revisited", publisher = CUP, year = 1996} @BOOK{hitchens-orwell, author = "Christopher Hitchens", title = "Why {O}rwell Matters", publisher = "Basic Books", year = 2002} @BOOK{hodge-pedoe1, author = "W. V. D. Hodge and Daniel Pedoe", title = "Methods of Algebraic Geometry, vol. 1", publisher = CUP, year = 1968} @BOOK{hodges-logic, author = "Wilfrid Hodges", title = "Logic", publisher = "Penguin", year = 1977} @BOOK{hodges-model, author = "Wilfrid Hodges", title = "Model Theory", publisher = CUP, series = "Encyclopedia of Mathematics and its Applications", volume = 42, year = 1993} @BOOK{hodges-turing, author = "Andrew Hodges", title = "{A}lan {T}uring: The Enigma", publisher = "Burnett Books / Hutchinson", year = 1983} @BOOK{holmes-naive, author = "Randall M. Holmes", title = "Naive Set Theory with a Universal Set", publisher = "Bruylant-Academia, Louvain-la-Neuve", series = "Cahiers du Centre de logique", volume = 10, year = 1998} @BOOK{hormander-pdo2, author = "Lars H{\"o}rmander", title = "The Analysis of Linear Partial Differential Operators {II}", publisher = SV, series = "Grundlehren der mathematischen Wissenschaften", volume = 257, year = 1983} @BOOK{hoyle-intelligent, author = "Fred Hoyle", title = "The Intelligent Universe", publisher = "Michael Joseph", series = "Mermaid books", year = 1983} @BOOK{hurd-loeb, author = "A. E. Hurd and P. A. Loeb", title = "An introduction to nonstandard real analysis", publisher = AP, year = 1985} @BOOK{husserl-investigations, author = "Edmund Husserl", title = "{L}ogische {U}ntersuchungen", publisher = "Halle", year = 1900, note = "English translation by J.N. Findlay: `Logical Investigations', published by the Humanities Press, NY, 1970. Based on revised, 1913 Halle edition"} @BOOK{huth-ryan, author = "Michael Huth and Mark Ryan", title = "Logic in Computer Science: Modelling and reasoning about systems", publisher = CUP, year = 1999} @BOOK{jacobson1, author = "Nathan Jacobson", title = "Basic Algebra {I}", publisher = "W. H. Freeman", edition = "2nd", year = 1989} @BOOK{jech-ac, author = "T. J. Jech", title = "The Axiom of Choice", publisher = NH, series = SL, volume = 75, year = 1973} @BOOK{jenks-axiom, author = "Richard D. Jenks and Robert S. Sutor", title = "{AXIOM}: the scientific computation system", publisher = SV, year = 1992} @BOOK{jensen-wirth, author = "Kathleen Jensen and Niklaus Wirth", title = "Pascal user manual and report", publisher = SV, year = 1974} @BOOK{johnstone-logic, author = "Peter T. Johnstone", title = "Notes on Logic and Set Theory", publisher = CUP, year = 1987} @BOOK{johnstone-stone, author = "Peter T. Johnstone", title = "Stone spaces", publisher = CUP, series = "Cambridge studies in advanced mathematics", volume = 3, year = 1982} @BOOK{jones-garbage, author = "Richard Jones and Rafael Lins", title = "Garbage collection: algorithms for automatic dynamic memory management", publisher = "Wiley", year = 1996} @BOOK{kant-critique, author = "Immanuel Kant", title = "Kritik der reinen Vernunft", year = 1787, edition = "2nd", note = "English translation `Critique of pure reason' by Kemp Smith, Macmillan, 1929"} @BOOK{kaufmann-cara, author = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore", title = "Computer-Aided Reasoning: An Approach", publisher = "Kluwer", year = 2000} @BOOK{kaufmann-acl2, author = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore", title = "Computer-Aided Reasoning: An Approach", publisher = "Kluwer", year = 2000} @BOOK{kaufmann-case, author = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore", title = "Computer-Aided Reasoning: {ACL2} Case Studies", publisher = "Kluwer", year = 2000} @BOOK{keisler-calculus, author = "H. Jerome Keisler", title = "Elementary Calculus: An Approach Using Infinitesimals", publisher = "Prindle, Weber and Schmidt", year = 1976, note = "Available in full on the Web at {\verb!http://www.math.wisc.edu/~keisler/calc.html!}"} @BOOK{kelley, author = "John L. Kelley", title = "General topology", publisher = SV, year = 1975, series = "Graduate Texts in Mathematics", volume = 27, note = "First published by D. van Nostrand in 1955"} @BOOK{kleene-meta, author = "Stephen Cole Kleene", title = "Introduction to metamathematics", publisher = NH, year = 1952} @BOOK{kneale, author = "William Kneale and Martha Kneale", title = "The Development Of Logic", publisher = "Clarendon Press", year = 1962} @BOOK{kneebone, author = "G. T. Kneebone", title = "Mathematical Logic and the Foundations of Mathematics: an Introductory Survey", publisher = "D. Van Nostrand", year = 1963} @BOOK{knopp-series, author = "Konrad Knopp", title = "Theory and Application of Infinite Series", publisher = "Blackie and Son Ltd.", year = 1951, edition = "2nd"} @BOOK{knuth-seminum, author = "Donald E. Knuth", title = "The Art of Computer Programming; Volume 2: Seminumerical Algorithms", series = "Addison-Wesley Series in Computer Science and Information processing", publisher = AW, year = 1969} @BOOK{knuth-ss, author = "Donald E. Knuth", title = "The Art of Computer Programming; Volume 3: Sorting and Searching", series = "Addison-Wesley Series in Computer Science and Information processing", publisher = AW, year = 1973} @BOOK{knuth-selected, author = "Donald E. Knuth", title = "Selected Papers on Computer Science", publisher = CUP, series = "CSLI Publications", year = 1996} @BOOK{koetsier-lakatos, author = "T. Koetsier", title = "Lakatos' philosophy of mathematics: a historical approach", publisher = "Elsevier", series = "Studies in the history and philosophy of mathematics", volume = 3, year = 1991} @BOOK{koren-arithmetic, author = "Israel Koren", title = "Computer Arithmetic Algorithms", publisher = PH, year = 1992} @BOOK{kreisel-krivine, author = "Georg Kreisel and Jean-Louis Krivine", title = "Elements of mathematical logic: model theory", edition = "Revised second", publisher = NH, year = 1971, series = SL, note = "First edition 1967. Translation of the French `El{\'e}ments de logique math{\'e}matique, th{\'e}orie des modeles' published by Dunod, Paris in 1964"} @BOOK{krivine-sets, author = "Jean-Louis Krivine", title = "Introduction to Axiomatic Set Theory", publisher = "D. Reidel Publishing Company", year = 1971, series = SLIB, note = "Translation of the French `Th{\'e}orie Axiomatique des Ensembles', first published by Presses Universitaires de France, Paris. Translated by David Miller"} @BOOK{kroeger-temporal, author = "Fred Kr{\"o}ger", title = "Temporal Logic of Programs", publisher = SV, year = 1987, series = "EATCS Monographs on Theoretical Computer Science", volume = 8} @BOOK{kropf-fhv, author = "Thomas Kropf", title = "Introduction to Formal Hardware Verification", publisher = SV, year = 1999} @BOOK{kunen, author = "Kenneth Kunen", title = "Set Theory: An Introduction to Independence Proofs", publisher = NH, year = 1980, series = SL, volume = 102} @BOOK{kushner, author = "B. A. Kushner", title = "Lectures on Constructive Mathematical Analysis", publisher = "American Mathematical Society", year = 1984, series = "Translations of Mathematical Monographs vol. 60"} @BOOK{lakatos-pr, author = "Imre Lakatos", title = "Proofs and Refutations: the Logic of Mathematical Discovery", publisher = "Cambridge University Press", year = 1976, note = "Edited by John Worrall and Elie Zahar. Derived from Lakatos's Cambridge PhD thesis; an earlier version was published in the {\em British Journal for the Philosophy of Science} vol. 14"} @BOOK{lambek-scott, author = "J. Lambek and P. J. Scott", title = "Introduction to higher order categorical logic", publisher = CUP, series = "Cambridge studies in advanced mathematics", volume = 7, year = 1986} @BOOK{landau, author = "Edmund Landau", title = "Grundlagen der Analysis", publisher = "Leipzig", year = 1930, note = "English translation by F. Steinhardt: `Foundations of analysis: the arithmetic of whole, rational, irrational, and complex numbers. A supplement to textbooks on the differential and integral calculus', published by Chelsea; 3rd edition 1966"} @BOOK{lang-algebra, author = "Serge Lang", title = "Algebra", edition = "3rd", publisher = AW, year = 1994} @BOOK{lecat-errors, author = "Maurice Lecat", title = "Erreurs de Math{\'e}maticiens", publisher = "?, Brussels", year = 1935} @BOOK{leisenring-hilbert, author = "A. C. Leisenring", title = "Mathematical logic and Hilbert's {$\epsilon$}-symbol", publisher = "Macdonald", year = 1969} @BOOK{leitsch-resolution, author = "Alexander Leitsch", title = "The Resolution Calculus", publisher = SV, year = 1997} @BOOK{levy-gamesmanship, author = "David Levy", title = "Computer Gamesmanship", publisher = "Century", year = 1983} @BOOK{lewis-classes, author = "David Lewis", title = "Parts of classes", publisher = "Blackwell", year = 1991, note = "With an appendix by John P. Burgess, A.P. Hazen, and David Lewis"} @BOOK{lewis-langford, author = "C. I. Lewis and C. H. Langford", title = "Symbolic Logic", edition = "2nd", publisher = "The Century Co.", year = 1932} @BOOK{lewis-survey, author = "C. I. Lewis", title = "A Survey of Symbolic Logic: the classic algebra of logic", publisher = "University of California Press", year = 1918, note = "Reprinted without last chapters by Dover, 1960"} @BOOK{lewis-unsolvable, author = "H. Lewis", title = "Unsolvable Classes of Quantificational Formulas", publisher = AW, year = 1997} @BOOK{libes-expect, author = "Don Libes", title = "Exploring Expect: a Tcl-based toolkit for automating interactive programs", publisher = "O'Reilly", year = 1995} @BOOK{lightstone, author = "A. H. Lightstone", title = "Symbolic Logic and the Real Number System", publisher = "Harper and Row", year = 1965} @BOOK{lifschitz-mtp, author = "Vladimir Lifschitz", title = "Mechanical Theorem Proving in the USSR: the Leningrad School", series = "Monograph Series on Soviet Union", publisher = "Delphic Associates, 7700 Leesburg Pike, {\#250}, Falls Church, VA 22043. Phone: (703) 556-0278", year = 1986, note = "See also `What is the inverse method?' in the Journal of Automated Reasoning, vol. 5, pp. 1--23, 1989"} @BOOK{littlewood-miscellany, author = "John Edensor Littlewood", title = "Littlewood's Miscellany", publisher = CUP, year = 1986, note = "Edited by Bela Bollobas"} @BOOK{lloyd-flp, author = "J. W. Lloyd", title = "Foundations of Logic Programming", publisher = SV, year = 1984} @BOOK{locke-essay, author = "John Locke", title = "An Essay concerning Human Understanding", publisher = "William Tegg, London", year = 1689} @BOOK{loveland-book, author = "Donald W. Loveland", title = "Automated theorem proving: a logical basis", publisher = NH, year = 1978} @BOOK{lukasiewicz-aristotle, author = "Jan {\L}ukasiewicz", title = "Aristotle's Syllogistic from the standpoint of modern formal logic", publisher = "Clarendon Press", year = 1951} @BOOK{mackenzie-mechanizing, author = "Donald MacKenzie", title = "Mechanizing Proof: Computing, Risk and Trust", publisher = MIT, year = 2001} @BOOK{maclane-mff, author = "Mac Lane, Saunders", title = "Mathematics: Form and Function", publisher = SV, year = 1986} @BOOK{macnamara-border, author = "John Macnamara", title = "A border dispute: the place of logic in psychology", publisher = MIT, year = 1986} @BOOK{malinowski-mvl, author = "Grzegorz Malinowski", title = "Many-valued logics", publisher = OUP, series = "Oxford Logic Guides", volume = 25, year = 1993} @BOOK{manna-pnueli1, author = "Zohar Manna and Amir Pnueli", title = "The temporal logic of reactive and concurrent systems --- Specification", publisher = SV, year = 1992} @BOOK{manna-pnueli2, author = "Zohar Manna and Amir Pnueli", title = "The temporal logic of reactive and concurrent systems --- Safety properties", publisher = SV, year = 1995} @BOOK{marciszewski-murawski, author = "Witold Marciszewski and Roman Murawski", title = "Mechanization of Reasoning in a Historical Perspective", series = "Pozna{\'n} Studies in the Philosophy of the Sciences and the Humanities", volume = 43, publisher = "Rodopi, Amsterdam", year = 1995} @BOOK{markstein-book, author = "Peter Markstein", title = "{IA-64} and Elementary Functions: Speed and Precision", publisher = "Prentice-Hall", year = 2000} @BOOK{mates-book, author = "Benson Mates", title = "Elementary logic", publisher = OUP, year = 1972, edition = "2nd"} @BOOK{matijasevich-book, author = "Yuri V. Matijasevich", title = "Hilbert's Tenth Problem", publisher = MIT, year = 1993} @BOOK{matsumura, author = "Hideyuki Matsumura", title = "Commutative Ring Theory", publisher = CUP, series = "Cambridge Studies in Advanced Mathematics", volume = 8, year = 1986, note = "Translated from Japanese `Kakan kan ron' by Miles Reid"} @BOOK{mauthner-critique, author = "Fritz Mauthner", title = "Beitrage zu einer {K}ritik der {S}prache (3 vols)", publisher = "Berlin", year = 1901} @BOOK{mcallester-onticbook, author = "David A. McAllester", title = "{ONTIC}: A Knowledge Representation System for Mathematics", publisher = MIT, year = 1989} @BOOK{mccarthy-lisp-1.5, author = "John McCarthy", title = "{LISP} 1.5 Programmer's Manual", publisher = MIT, year = 1962} @BOOK{mccune-padmanabhan, author = "W. McCune and R. Padmanabhan", title = "Autoamted Deduction in Equational Logic and Cubic Curves", publisher = SV, series = LNCS, volume = 1095, year = 1996} @BOOK{melham-book, author = "Thomas F. Melham", title = "Higher Order Logic and Hardware Verification", publisher = CUP, year = 1993, series = CTTCS, volume = 31, note = "A revision of the author's PhD thesis"} @BOOK{mendelson, author = "Elliott Mendelson", title = "Introduction to Mathematical Logic", edition = "Third", publisher = "Wadsworth and Brooks Cole", year = 1987, series = "Mathematics series"} @BOOK{menezes-crypto, author = "Alfred J. Manezes and Paul C. van Oorschot and Scott A. Vanstone", title = "Handbook of Applied Crypography", publisher = "CRC", year = 1997} @BOOK{menger-calculus, author = "Karl Menger", title = "Calculus, a modern approach", publisher = "Ginn", year = 1955} @BOOK{metzner-decision, author = "John R. Metzner and Bruce H. Barnes", title = "Decision Table Languages and Systems", publisher = AP, series = "ACM Monograph Series", year = 1977} @BOOK{mignotte-mca, author = "Maurice Mignotte", title = "Mathematics for Computer Algebra", publisher = SV, year = 1991} @BOOK{mill-hamilton, author = "John Stuart Mill", title = "An examination of Sir William Hamilton's philosophy, and of the principal philosophical questions discussed in his writings", publisher = "Longmans Green", year = 1865} @BOOK{milner-commentary, author = "Robin Milner and Mads Tofte", title = "Commentary on {S}tandard {ML}", publisher = "The MIT Press", year = 1991} @BOOK{milner-def, author = "Robin Milner and Mads Tofte and Robert Harper", title = "The Definition of {S}tandard {ML}", publisher = "The MIT Press", year = 1990} @BOOK{minsky, author = "Marvin L. Minsky", title = "Computation: Finite and Infinite Machines", publisher = PH, year = 1967, series = "Prentice-Hall Series in Automatic Computation"} @BOOK{mints-intuitionistic, author = "Grigori Mints", title = "A Short Introduction to Intuitionistic Logic", publisher = "Kluwer", year = 2000} @BOOK{mishra-alal, author = "Bhubaneswar Mishra", title = "Algorithmic Algebra", publisher = SV, year = 1993} @BOOK{monk-logic, author = "James Donald Monk", title = "Mathematical logic", publisher = SV, series = GTM, volume = 37, year = 1976} @BOOK{moore-ac, author = "Gregory H. Moore", title = "Zermelo's axiom of choice: its origins, development, and influence", publisher = SV, series = "Studies in the history of mathematics and physical sciences", volume = 8, year = 1982} @BOOK{morse-sets, author = "A. P. Morse", title = "A theory of sets", publisher = AP, year = 1965} @BOOK{moschovakis-notes, author = "Yiannis Moschovakis", title = "Notes on Set Theory", publisher = SV, series = UTM, year = 1994, note = "Original edition published by Nefeli Publications, Athens, 1993"} @BOOK{moskowski-etlp, author = "Ben C. Moskowski", title = "Executing Temporal Logic Programs", publisher = CUP, year = 1986} @BOOK{muller-elementary, author = "Jean-Michel Muller", title = "Elementary functions: Algorithms and Implementation", publisher = BKH, year = 1997} @BOOK{mumford-redbook, author = "David Mumford", title = "The red book of varieties and schemes", edition = "2nd", publisher = SV, year = 1999} @BOOK{nathanson-additive1, author = "Melvyn B. Nathanson", title = "Additive Number Theory: The Classical Bases", publisher = SV, series = GTM, volume = 164, year = 1996} @BOOK{nemhauser-wolsey, author = "George L. Nemhauser and Laurence A. Wolsey", title = "Integer and Combinatorial Optimization", publisher = "Wiley", series = "Wiley-Interscience Series in Discrete Mathematics and Optimization", year = 1999} @BOOK{neumann-risks, author = "Peter G. Neumann", title = "Computer-related risks", publisher = AW, year = 1995} @BOOK{newborn-atp, author = "Monty Newborn", title = "Automated Theorem Proving: Theory and Practice", publisher = SV, year = 2001} @BOOK{nidditch, author = "P. H. Nidditch", title = "Introductory formal logic of mathematics", publisher = "University Tutorial Press, London", year = 1957} @BOOK{nidditch-development, author = "P. H. Nidditch", title = "The development of Mathematical Logic", publisher = "Thoemmes Press", year = 1962, note = "Newly reprinted, 1998"} @BOOK{nordstrom-etal, author = "Bengt Nordstr{\"o}m and Kent Peterson and Jan M. Smith", title = "Programming in {M}artin-{L}{\"o}f's Type Theory: An Introduction", publisher = OUP, year = 1990, series = "International Series of Monographs on Computer Science", volume = 7} @BOOK{odifreddi-crt, author = "Piergiorgio Odifreddi", title = "Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers", publisher = NH, series = SL, volume = 125, year = 1989} @BOOK{parker, author = "Francis D. Parker", title = "The Structure of Number Systems", series = "Teachers' Mathematics Reference series", publisher = PH, year = 1966} @BOOK{paulson-isabellebook, author = "Lawrence C. Paulson", title = "Isabelle: a generic theorem prover", publisher = SV, series = LNCS, volume = 828, year = 1994, note = "With contributions by Tobias Nipkow"} @BOOK{paulson-lcfbook, author = "Lawrence C. Paulson", title = "Logic and computation: interactive proof with Cambridge LCF", publisher = CUP, series = CTTCS, volume = 2, year = 1987} @BOOK{paulson-ml, author = "L. C. Paulson", title = "ML for the Working Programmer", publisher = CUP, year = 1991} @BOOK{peled-swr, author = "Doron A. Peled", title = "Software Reliability Methods", publisher = SV, year = 2001} @BOOK{pesin, author = "I. N. Pesin", title = "Classical and modern integration theories", publisher = AP, year = 1970} @BOOK{peterson-defect, author = "Ivars Peterson", title = "Fatal Defect : Chasing Killer Computer Bugs", publisher = "Arrow", year = 1996} @BOOK{petkovsek-ab, author = "Marki Petkov{\v{s}}ek and Herbert S. Wilf and Doron Zeilberger", title = "A = B", publisher = "A K Peters", year = 1996} @BOOK{pierce-tpl, author = "Benjamin C. Pierce", title = "Types and Programming Languages", publisher = MIT, year = 2002} @BOOK{poizat-model, author = "Bruno Poizat", title = "A Course in Model Theory: An Introduction to Contemporary Mathematical Logic", publisher = SV, year = 2000} @BOOK{polya-indan, author = "G. Polya", title = "Induction and Analogy in Mathematics", publisher = "Princeton University Press", year = 1954} @BOOK{post-iterative, author = "E. Post", title = "The two-valued iterative systems of mathematical logic", publisher = "Princeton University Press", year = 1941} @BOOK{pourel-richards, author = "Marian B. Pour-El and Jonathan I. Richards", title = "Computability in Analysis and Physics", publisher = SV, series = "Perspectives in Mathematical Logic", year = 1980} @BOOK{prawitz-book, author = "Dag Prawitz", title = "Natural deduction; a proof-theoretical study", series = "Stockholm Studies in Philosophy", volume = 3, publisher = "Almqvist and Wiksells", year = 1965} @BOOK{prestel-dalzell, author = "Alexander Prestel and Charles N. Dalzell", title = "Positive Polynomials: From {H}ilbert's 17th Problem to Real Algebra", publisher = SV, series = "Springer monographs in mathematics", year = 2001} @BOOK{quine-autobiog, author = "W. V. Quine", title = "The time of my life: an autobiography", publisher = MIT, series = "Bradford books", year = 1985} @BOOK{quine-methods, author = "W. V. Quine", title = "Methods of Logic", publisher = "Harvard University Press", year = 1950} @BOOK{quine-philog, author = "W. V. Quine", title = "Philosophy of Logic", publisher = "Prentice-Hall, Inc.", year = 1970, series = "Foundations of Philosophy Series"} @BOOK{rajwadi-squares, author = "A. R. Rajwade", title = "Squares", publisher = CUP, series = "London Mathematical Society Lecture Notes", volume = 171, year = 1993} @BOOK{rasiowa-sikorski, author = "Helena Rasiowa and Roman Sikorski", title = "The Mathematics of Metamathematics", edition = "3rd", publisher = "Polish Scientific Publishers", year = 1970, series = "Monografie Matematyczne, Instytut Matematyczny Polskiej Akademii Nauk", volume = 41} @BOOK{reade-efp, author = "Chris Reade", title = "Elements of Functional Programming", publisher = AW, year = 1989} @BOOK{reeves-clarke, author = "Steve Reeves and Michael Clarke", title = "Logic for Computer Science", publisher = AW, year = 1990} @BOOK{richards-bcpl, author = "M. Richards and C. Whitby-Strevens", title = "{BCPL} --- the language and its compiler", publisher = CUP, year = 1980} @BOOK{ritt-characteristic, author = "R. F. Ritt", title = "Differential Equations from Algebraic Standpoint", publisher = "American Mathematical Society", series = "AMS Colloquium Publications", volume = 14, year = 1938} @BOOK{ritt-differential, author = "R. F. Ritt", title = "Differential Algebra", publisher = "American Mathematical Society", series = "AMS Colloquium Publications", note = "Republished in 1966 by Dover", year = 1950} @BOOK{roberts, author = "J. B. Roberts", title = "The Real Number System in an Algebraic Setting", publisher = "W. H. Freeman and Company", year = 1962} @BOOK{robinson-complete, author = "Abraham Robinson", title = "Complete Theories", publisher = NH, series = SL, year = 1956} @BOOK{robinson-model, author = "Abraham Robinson", title = "Introduction to model theory and to the metamathematics of algebra", publisher = NH, year = 1963, series = SL} @BOOK{robinson-nsa, author = "Abraham Robinson", title = "Non-standard Analysis", publisher = NH, year = 1966, series = SL} @BOOK{rodriguez, author = "Francisco A. Rodriguez-Consuegra", title = "The Mathematical Philosophy of {B}ertrand {R}ussell: Origins and Development", publisher = "Birkh{\"a}user Verlag", year = 1991} @BOOK{rosser-ml, author = "J. Barkley Rosser", title = "Logic for Mathematicians", publisher = "McGraw-Hill", year = 1953} @BOOK{royden-analysis, author = "H. L. Royden", title = "Real analysis", publisher = "Macmillan", year = 1988, edition = "3rd"} @BOOK{rubin-ac2, author = "Herman Rubin and Jean E. Rubin", title = "Equivalents of the axiom of choice, {II}", publisher = NH, series = SL, volume = 116, year = 1985, note = "First edition in the same series, 1963"} @BOOK{rudin-analysis, author = "Walter Rudin", title = "Principles of Mathematical Analysis", publisher = "McGraw-Hill", edition = "3rd", year = 1976} @BOOK{russell-autobiog, author = "Bertrand Russell", title = "The autobiography of Bertrand Russell", publisher = "Allen \& Unwin", year = 1968} @BOOK{russell-external, author = "Bertrand Russell", title = "Our Knowledge of the External World", publisher = CUP, year = 1914} @BOOK{russell-mathphil, author = "Bertrand Russell", title = "Introduction to mathematical philosophy", publisher = "Allen {\&} Unwin", year = 1919} @BOOK{russell-principles, author = "Bertrand Russell", title = "The principles of mathematics vol. 1", publisher = CUP, year = 1903, note = "Volume 2 was never published, but rather transmuted into \cite{whitehead-principia}"} @BOOK{russell-problems, author = "Bertrand Russell", title = "The problems of philosophy", publisher = OUP, year = 1912} @BOOK{rydeheard-burstall, author = "David Rydeheard and Rod Burstall", title = "Computational Category Theory", publisher = PH, year = 1988} @BOOK{schenk-cca, author = "Hal Schenk", title = "Computational Algebraic Geometry", publisher = CUP, year = 2003} @BOOK{schneider-concurrent, author = "Fred B. Schneider", title = "On Concurrent Programming", series = "Graduate Texts in Computer Science", publisher = SV, year = 1997} @BOOK{schoenfeld-problem, author = "A. Schoenfeld", title = "Mathematical Problem Solving", publisher = AP, year = 1985} @BOOK{schumann-atpse, author = "Johann M. Schumann", title = "Automated Theorem Proving in Software Engineering", publisher = SV, year = 2001} @BOOK{schwabhauser-geom, author = "H. Schwabh{\"a}user and W. Szmielev and A. Tarski", title = "Metamathematische {M}ethoden in der {G}eometrie", publisher = SV, year = 1983} @BOOK{sergeyev-infinity, author = "Ya. D. Sergeyev", title = "Arithmetic of Infinity", publisher = "Edizioni Orizzonti Meridionali CS", year = 2003} @BOOK{severi-fondamenti, author = "Francesco Severi", title = "Fondamenti di Geometria Algebrica: lezioni tenute nell'anno accademico 1946-47", publisher = "Antonio Milani, Padova", series = "Quaderni Matematici, Scuola Normale Superiore di Pisa", volume = 2, year = 1948} @BOOK{shankar-book, author = "N. Shankar", title = "Metamathematics, Machines and {G}{\"o}del's Proof", series = CTTCS, volume = 38, publisher = CUP, year = 1994} @BOOK{shapiro, author = "Stewart Shapiro", title = "Foundations without Foundationalism: a case for second-order logic", publisher = "Clarendon Press", series = "Oxford Logic Guides", number = 17, year = 1991} @BOOK{siewiorek, author = "D. P. Siewiorek and C. G. Bell and A. Newell", title = "Computer Structures: Principles and Examples", publisher = "McGraw-Hill", year = 1982} @BOOK{simpson-subsystems, author = "Stephen G. Simpson", title = "Subsystems of Second Order Arithmetic", publisher = SV, year = 1998} @BOOK{smart-resolution, author = "Nigel P. Smart", title = "The Algorithmic Resolution of Diophantine Equations", publisher = CUP, series = "London Mathematical Society Student Texts", volume = 41, year = 2001} @BOOK{smorynski-lnt1, author = "Craig Smory{\'n}ski", title = "Logic Number Theory {I}: An Introduction", publisher = SV, year = 1980} @BOOK{smorynski-self, author = "C. Smory{\'n}ski", title = "Self-Reference and Modal Logic", publisher = SV, year = 1985} @BOOK{smullyan-diag, author = "Raymond M. Smullyan", title = "Diagonalization and Self-Reference", publisher = OUP, series = "Oxford Logic Guides", volume = 27, year = 1994} @BOOK{smullyan-godel, author = "Raymond M. Smullyan", title = "G{\"o}del's Incompleteness Theorems", publisher = OUP, series = "Oxford Logic Guides", volume = 19, year = 1992} @BOOK{spivey-understanding, author = "J. Michael Spivey", title = "Understanding Z: a specification language and its formal semantics", publisher = CUP, year = 1988, series = CTTCS, volume = 3} @BOOK{stenlund, author = "S{\"o}ren Stenlund", title = "Combinators, {$\lambda$}-terms and Proof Theory", publisher = "D. Reidel", year = 1972, series = "Synthese Library"} @BOOK{stewart-matrix1, author = "G. W. Stewart", title = "Matrix Algorithms, volume 1: Basic Decompositions", publisher = "SIAM", year = 1998} @BOOK{sterbenz, author = "Pat H. Sterbenz", title = "Floating-Point Computation", publisher = "Prentice-Hall", year = 1974} @BOOK{strang-linear, author = "Gilbert Strang", title = "Linear Algebra and its Applications", edition = "3rd", publisher = "Brooks/Cole", year = 1988} @BOOK{strawson-logical, author = "Peter Strawson", title = "Introduction to Logical Theory", publisher = "Methuen", year = 1952} @BOOK{tarski-intro, author = "Alfred Tarski", title = "Introduction to Logic, and to the methodology of deductive sciences", publisher = OUP, year = 1941, note = "Reprinted by Dover, 1995. Revised edition of the original Polish text {\em O logice matematycznej i metodzie dedukcyjnej}, published in 1936"} @BOOK{tarski-undecidable, author = "Alfred Tarski and Andrzej Mostowski and Raphael M. Robinson", title = "Undecidable Theories", publisher = NH, series = SL, year = 1953, note = "Three papers: `A General Method in Proofs of Undecidability', `Undecidability and Essential Undecidability in Arithmetic' and `Undecidability of the Elementary Theory of Groups'; all but the second are by Tarski alone."} @BOOK{tennant-anti, author = "Neil Tennant", title = "Anti-realism and logic: truth as eternal", publisher = "Clarendon Press", year = 1987} @BOOK{trefethen-nla, author = "Lloyd N. Trefethen and David Bau", title = "Numerical Linear Algebra", publisher = "SIAM", year = 1997} @BOOK{triebel-ia64, author = "Walter Triebel", title = "{IA-64} Architecture for Software Developers", publisher = "Intel Press", year = 2000} @BOOK{troelstra-con1, author = "A. S. Troelstra and Dalen, D. van", title = "Constructivism in mathematics, vol. 1", publisher = NH, series = SL, volume = 121, year = 1988} @BOOK{troelstra-schwichtenberg, author = "A. S. Troelstra and H. Schwichtenberg", title = "Basic Proof Theory", publisher = CUP, series = CTTCS, volume = 43, year = 1996} @BOOK{turing-worksmi, author = "Alan Turing", title = "Collected Works: Mechanical Intelligence", publisher = NH, year = 1992} @BOOK{upsenskii-mechanics, author = "V. A. Upsenskii", title = "Some Applications of Mechanics to Mathematics", publisher = "Pergamon", series = "Popular lectures in mathematics", volume = 3, year = 1961, note = "Translated from the Russian by Halina Moss; translation editor Ian N. Sneddon"} @BOOK{vangasteren-shape, author = "Gasteren, Antonetta Johana Maria van", title = "On the shape of mathematical arguments", publisher = SV, series = LNCS, volume = 445, year = 1990, note = "Foreword by E. W. Dijkstra."} @BOOK{vanstigt, author = "Stigt, Walter P. van", title = "{B}rouwer's Intuitionism", publisher = NH, year = 1990, series = "Studies in the History and Philosophy of Mathematics", volume = 2} @BOOK{stoll, author = "Robert Roth Stoll", title = "Set theory and logic", publisher = "Dover Publications", year = 1979, note = "Originally published by W.H. Freeman in 1963"} @BOOK{takeuti-uses, author = "Gaisi Takeuti", title = "Two applications of logic to mathematics", series = "Publications of the Mathematical Society of Japan", number = 13, publisher = "Iwanami Shoten, Tokyo", note = "Number 3 in Kan{\^o} memorial lectures", year = 1978} @BOOK{tarski-decision, author = "Alfred Tarski", title = "A Decision Method for Elementary Algebra and Geometry", publisher = "University of California Press", year = 1951, note = "Previous version published as a technical report by the RAND Corporation, 1948; prepared for publication by J. C. C. McKinsey. Reprinted in \cite{caviness-johnson}, pp. 24--84."} @BOOK{thompson-haskell, author = "Simon Thompson", title = "{H}askell: The Craft of Functional Programming", edition = "2nd", publisher = AW, year = 1999} @BOOK{thurston, author = "H. A. Thurston", title = "The number system", publisher = "Blackie", year = 1956} @BOOK{troelstra, author = "A. S. Troelstra", title = "Metamathematical Investigation of Intuitionistic Arithmetic and Analysis", publisher = SV, series = "Lecture Notes in Mathematics", number = 344, year = 1973, note = "Second, corrected edition available, as ILCC Prepublication Series number X-93-05, from the University of Amsterdam"} @BOOK{vickers-topology, author = "Steven Vickers", title = "Topology via Logic", publisher = CUP, series = CTTCS, volume = 5, year = 1989} @BOOK{wagon-btp, author = "Stan Wagon", title = "The Banach-Tarski paradox", publisher = CUP, series = "Encyclopedia of mathematics and its applications", volume = 24, year = 1985} @BOOK{wallis, author = "Peter J. L. Wallis", title = "Improving floating-point programming", publisher = "Wiley", year = 1990} @BOOK{watson-bessel, author = "G. N. Watson", title = "A treatise on the theory of {B}essel functions", publisher = CUP, year = 1922} @BOOK{watterson-drooling, author = "Bill Watterson", title = "Something under the bed is drooling", publisher = "Andrews McMeel", year = 1988} @BOOK{watterson-complete, author = "Bill Watterson", title = "The Complete {C}alvin and {H}obbes", publisher = "Andrews McMeel", year = 2005} @BOOK{waugh-autobiog, author = "Auberon Waugh", title = "Will this do? The first fifty years of Auberon Waugh: an autobiography", publisher = "Arrow Books", year = 1991} @BOOK{weil-algeom, author = "A. Weil", title = "Foundations of algebraic geometry", publisher = "American Mathematical Society", series = "AMS Colloquium Publications", volume = 29, year = 1946, note = "Revised edition 1962"} @BOOK{weil-numbertheory, author = "A. Weil", title = "Number Theory: An approach through history from {H}ammurapi to {L}egendre", publisher = BKH, year = 1983} @BOOK{weispfenning-becker, author = "V. Weispfenning and T. Becker", title = "Groebner bases: a computational approach to commutative algebra", publisher = SV, series = GTM, year = 1993} @BOOK{weiss-dmello, author = "William Weiss and Cherie D'Mello", title = "Fundamentals of Model Theory", publisher = "Online", year = 1997, note = "Available from \url{http://www.math.toronto.edu/~weiss/model_theory.html}"} @BOOK{whitehead-intro, author = "Alfred North Whitehead", title = "An Introduction to Mathematics", publisher = "Williams and Norgate", year = 1919} @BOOK{weiss-leroy, author = "Pierre Weis and Xavier Leroy", title = "Le langage {C}aml", publisher = "InterEditions", year = 1993, note = "See also the CAML Web page: {\verb+http://pauillac.inria.fr/caml/+}"} @BOOK{whitehead-principia, author = "Alfred North Whitehead and Bertrand Russell", title = "Principia Mathematica (3 vols)", publisher = CUP, year = 1910} @BOOK{wildberger-divine, author = "N. J. Wildberger", title = "Divine Proportions: Rational Trigonometry to Universal Geometry", publisher = "Wild Egg Books, Sydney", year = 2005} @BOOK{wiedijk-17, author = "Freek Wiedijk", title = "The Seventeen Provers of the World", publisher = SV, series = LNCS, volume = 3600, year = 2006} @BOOK{wilder-found, author = "Raymond Louis Wilder", title = "Introduction to the foundations of mathematics", publisher = "Wiley", year = 1965} @BOOK{wilkinson-reap, author = "J. H. Wilkinson", title = "Rounding Errors in Algebraic Processes", publisher = "Her Majesty's Stationery Office (HMSO), London", series = "National Physical Laboratory Notes on Applied Science", volume = 32, year = 1963} @BOOK{winskel-sem, author = "Glynn Winskel", title = "The formal semantics of programming languages: an introduction", publisher = "MIT Press", series = "Foundations of computing", year = 1993} @BOOK{wirth-systematic, author = "N. Wirth", title = "Systematic Programming: An Introduction", publisher = "Prentice-Hall", year = 1973} @BOOK{wolfram-book, author = "D. A. Wolfram", title = "The Clausal Theory of Types", publisher = CUP, year = 1993, series = CTTCS, volume = 21} @BOOK{wolfram-mathematica, author = "Stephen Wolfram", title = "Mathematica: a system for doing mathematics by computer", publisher = AW, year = 1991, edition = "2nd"} @BOOK{wos-ar, author = "Larry Wos and Ross Overbeek and Ewing Lusk and Jim Boyle", title = "Automated Reasoning: Introduction and Applications", publisher = "McGraw Hill", year = 1992} @BOOK{wos-fascinating, author = "Larry Wos and Gail W. Pieper", title = "A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning", publisher = "World Scientific", year = 1999} @BOOK{wu-geom, author = "Went Sun Wu and Xiso Fan Jin and Dong Ming Wang", title = "Mechanical Theorem Proving in Geometries: Basic Principles", publisher = SV, year = 1994} @BOOK{yap-algorithmic, author = "Chee Ken Yap", title = "Fundamental Problems of Algorithmic Algebra", publisher = OUP, year = 2000} %****************************************************************************% % THESES (PhD, Masters etc.) % %****************************************************************************% @PHDTHESIS{aichinger-thesis, author = "Erhard Aichinger", title = "Interpolation with Near-rings of Polynomial Functions", school = "Johannes Kepler Universit{\"a}t Linz", note = "Author's Diplomarbeit", year = 1994} @PHDTHESIS{barrett-thesis, author = "Craig Barrett", title = "Checking Validity of Quantifier-Free Formulas in Combinations of First-Order Theories", school = "Stanford University Computer Science Department", year = 2002} @PHDTHESIS{bayer-thesis, author = "D. Bayer", title = "The Division Algorithm and the {H}ilbert Scheme", school = "Harvard University", year = 1982} @PHDTHESIS{bennett-thesis, author = "J. H. Bennet", title = "On Spectra", school = "Princeton University", year = 1962} @PHDTHESIS{boldo-thesis, author = "Sylvie Boldo", title = "Preuves formelles en arithm{\'e}tiques {\`a} virgule flottante", school = "ENS Lyon", year = 2004, note = "Available on the Web from {\url{http://www.ens-lyon.fr/LIP/Pub/Rapports/PhD/PhD2004/PhD2004-05.pdf}}"} @PHDTHESIS{buchberger-thesis, author = "Bruno Buchberger", title = "Ein {A}lgorithmus zum {A}uffinden der {B}asiselemente des {R}estklassenringes nach einem nulldimensionalen {P}olynomideal", school = "Mathematisches Institut der Universit{\"a}t Innsbruck", year = 1965, note = "English translation to appear in Journal of Symbolic Computation, 2006"} @PHDTHESIS{cardelloliver-thesis, author = "Rachel Mary Cardell-Oliver", title = "The formal verification of hard real-time systems", school = CL, address = CLA, year = 1992, number = 255, type = CLT} @PHDTHESIS{dhingra-thesis, author = "Inderpreet Singh Dhingra", title = "Formalising an integrated circuit design style in higher order logic", school = CL, address = CLA, year = 1988, number = 151, type = CLT} @PHDTHESIS{fontaine-thesis, author = "Pascal Fontaine", title = "Techniques for verification of concurrent systems with invariants", school = "Institut Montefiore, Universit{\'e} de Li{\`e}ge", year = 2004} @PHDTHESIS{geser-thesis, author = "A. Geser", title = "Relative Termination", school = "University of Passau", year = 1990} @MASTERSTHESIS{goldschmidt-thesis, author = "R. E. Goldschmidt", title = "Applications of division by convergence", school = "Dept. of Electrical Engineering, MIT", address = "Cambridge, Mass.", year = 1964} @PHDTHESIS{good-thesis, author = "D. I. Good", title = "Toward a Man-Machine System for Proving Program Correctness", school = "University of Wisconsin", year = 1970} @PHDTHESIS{hindley-thesis, author = "J. R. Hindley", title = "The {C}hurch-{R}osser property and a result in combinatory logic", school = "University of Newcastle-upon-Tyne", year = 1964} @PHDTHESIS{holm-thesis, author = "John Erick Holm", title = "Floating-Point Arithmetic and Program Correctness Proofs", school = "Cornell University", year = 1980} @PHDTHESIS{huet-thesis, author = "G. Huet", title = "Constrained resolution: a complete method for higher order logic", school = "Case Western University", year = 1972} @PHDTHESIS{hunt-thesis, author = "W. A. Hunt", title = "{FM8501}: A Verified Micrprocessor", school = "University of Texas", year = 1985, note = "Published by Springer-Verlag as volume 795 of the {\em Lecture Notes in Computer Science} series, 1994"} @PHDTHESIS{hurd-thesis, author = "Joe Hurd", title = "Formal Verification of Probabilistic Algorithms", school = "University of Cambridge", year = 2001} @PHDTHESIS{jacobi-thesis, author = "C. Jacobi", title = "Formal Verification of a Fully {IEEE} Compliant Floating Point Unit", school = "University of the Saarland", year = 2002, note = "Available on the Web as {\url{http://engr.smu.edu/~seidel/research/diss-jacobi.ps.gz}}"} @PHDTHESIS{joyce-thesis, author = "Jeffrey John Joyce", title = "Multi-level verification of microprocessor-based systems", school = CL, address = CLA, year = 1990, number = 195, type = CLT} @PHDTHESIS{jutting-thesis, author = "Jutting, L. S. van Bentham", title = "Checking {L}andau's ``{G}rundlagen'' in the {AUTOMATH} System", school = "Eindhoven University of Technology", year = 1977, note = "Useful summary in \cite{nederpelt-automath}, pp. 701--732"} @PHDTHESIS{kamp-thesis, author = "J. A. W. Kamp", title = "Tense logic and the theory of order", school = "University of California at Los Angeles", year = 1968} @PHDTHESIS{king-thesis, author = "J. C. King", title = "A Program Verifier", school = "Carnegie-Mellon University", year = 1969} @PHDTHESIS{kowalski-thesis, author = "R. Kowalski", title = "Studies in the completeness and efficiency of theorem-proving by resolution", school = "University of Edinburgh", year = 1970} @PHDTHESIS{levitt-thesis, author = "Jeremy R. Levitt", title = "Formal Verification Techniques for Digital Systems", school = "Stanford University", year = 1999} @PHDTHESIS{melham-thesis, author = "Thomas Frederick Melham", title = "Formalizing abstraction mechanisms for hardware verification in higher order logic", school = CL, address = CLA, year = 1990, number = 201, type = CLT} @PHDTHESIS{menisse-thesis, author = "Val{\'e}rie M{\'e}nissier-Morain", title = "Arithm{\'e}tique exacte, conception, algorithmique et performances d'une impl{\'e}mentation informatique en pr{\'e}cision arbitraire", school = "Universit{\'e} Paris 7", type = "Th{\`e}se", year = 1994, month = "December"} @MASTERSTHESIS{murthy-thesis, author = "Chet Murthy", title = "Extracting Constructive Content from Classical Proofs", school = "Cornell University Department of Computer Science", address = "?", year = 1990, number = "?"} @PHDTHESIS{nivelle-thesis, author = "Hans de Nivelle", title = "Ordering Refinements of Resolution", school = "Technische Universiteit Delft", year = 1995} @PHDTHESIS{oheimb-thesis, author = "David von Oheimb", title = "Analyzing Java in {I}sabelle/{HOL}: Formalization, Type Safety and {H}oare Logic", school = "Technische Universit{\"a}t M{\"u}nchen", year = 2001} @PHDTHESIS{oostdijk-thesis, author = "Martijn Oostdijk", title = "Generation and Presentation of Formal Mathematical Documents", school = "Eindhoven University of Technology", year = 2001} @PHDTHESIS{persson-lic, author = "Henrik Persson", title = "Constructive Completeness of Intuitionistic Predicate Logic: A Formalisation in Type Theory", school = "Department of Computing Science, Chalmers University of Technology and University of G{\"o}teborg, Sweden", year = 1996, note = "Author's Licentiate Thesis"} @PHDTHESIS{pollack-thesis, author = "Robert Pollack", title = "The theory of {LEGO}: A Proof Checker for the Extended Calculus of Constructions", school = "University of Edinburgh", year = 1994} @PHDTHESIS{priest-thesis, author = "Douglas M. Priest", title = "On Properties of Floating Point Arithmetics: Numerical Stability and the Cost of Accurate Computations", school = "University of California, Berkeley", year = 1992, note = "Available on the Web as {\tt ftp://ftp.icsi.berkeley.edu/pub/theory/priest-thesis.ps.Z}"} @PHDTHESIS{reckhow-thesis, author = "R. A. Reckhow", title = "On the Lengths of Proofs in Propositional Calculus", school = "University of Toronto", year = 1976} @PHDTHESIS{robu-thesis, author = "Judit Robu", title = "Geometry Theorem Proving in the Frame of {T}heorema Project", school = "RISC-Linz", year = 2002} @PHDTHESIS{slind-phd, author = "Konrad Slind", title = "Reasoning about terminating functional programs", school = "Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen", year = 1999, note = "Available from {\url{http://tumb1.biblio.tu-muenchen.de/publ/diss/in/1999/slind.html}}"} @PHDTHESIS{smith-thesis, author = "Brian Cantwell Smith", title = "Reflection and Semantics in a Procedural Language", school = "Massachusetts Institute of Technology", address = "545 Technology Square, Cambridge MA, 02139", year = 1982, number = "MIT/LCS/TR-272", type = "Technical Report"} @PHDTHESIS{zammit-thesis, author = "Vincent Zammit", title = "On the Readability of Machine Checkable Formal Proofs", school = "Unoversity of Kent at Canterbury", year = 1999} %****************************************************************************% % TECHNICAL REPORTS % %****************************************************************************% @TECHREPORT{agerholm-dinf, author = "Sten Agerholm", title = "Formalising a Model of the {$\lambda$}-calculus in {HOL-ST}", institution = CL, address = CLA, year = 1994, number = 354, type = CLT} @TECHREPORT{agerholm-thesis, author = "Sten Agerholm", title = "A {HOL} Basis for Reasoning about Functional Programs", institution = "Centre of the Danish National Research Foundation", address = "Department of Computer Science, University of Aarhus, Ny Munkegade, DK-8000 Aarhus C, Denmark", year = 1994, number = "RS-94-44", type = "BRICS Report Series"} @TECHREPORT{andreka-guarded, author = "H. Andr{\'e}ka and J. van Bentham and I. N{\'e}meti", title = "Modal Languages and Bounded Fragments of Predicate Logic", institution = "Institute for Logic, Language and Computation, University of Amsterdam", type = "ILLC Research Report", number = "ML-96-03", year = 1996} @TECHREPORT{bachmair-ste, author = "L. Bachmair and H. Ganzinger and A. Voronkov", title = "Elimination of Equality via Transformations with Ordering Constraints", institution = "Max-Planck-Institut f{\"u}r Informatik", year = 1997, number = "MPI-I-97-2-012", type = "Technical report"} @TECHREPORT{back-scp, author = "Ralph Back and Jim Grundy and Wright, Joakim von", title = "Structured Calculational Proof", institution = "Turku Centre for Computer Science (TUCS)", address = "Lemmink{\"a}isenkatu 14 A, FIN-20520 Turku, Finland", year = 1996, number = 65, type = "Technical Report", note = "Also available as Technical Report {TR-CS-96-09} from the Australian National University"} @TECHREPORT{baumgartner-restart, author = "P. Baumgartner and U. Furbach", title = "Model Elimination without Contrapositives and its Application to {PTTP}", institution = "Institute for Computer Science, University of Koblenz", address = "Rheinau 1, 56075 Koblenz, Germany", year = 1993, number = "12-93", type = "Research report"} @TECHREPORT{bentham-lguarded, author = "J. van Benthem", title = "Dynamic bits and pieces", institution = "Institute for Logic, Language and Computation, University of Amsterdam", type = "ILLC Research Report", number = "LP-1997-01", year = 1997} @TECHREPORT{bjesse-formulas, author = "Per Bjesse", title = "Symbolic Model Checking with Sets of States Represented as Formulas", institution = "Department of Computer Science, Chalmers University of Technology", type = "Technical Report", number = "SC-1999-100", year = 1999} @TECHREPORT{boulton-ellareport, author = "Richard J. Boulton", title = "A {HOL} Semantics for a Subset of {ELLA}", institution = CL, address = CLA, year = 1992, number = 254, type = CLT} @TECHREPORT{boulton-thesis, author = "Richard John Boulton", title = "Efficiency in a fully-expansive theorem prover", institution = CL, address = CLA, year = 1993, number = 337, type = CLT, note = "Author's PhD thesis"} @TECHREPORT{bryant-srt, author = "Randal E. Bryant", title = "Bit-Level Analysis of an {SRT} Divide Circuit", institution = "School of Computer Science, Carnegie Mellon University", address = "Pittsburgh, PA 15213", type = "Technical Report", number = "CMU-CS-95-140", year = 1995} @TECHREPORT{burstall-goguen, author = "R. M. Burstall and J. A. Goguen", title = "Algebras, Theories and Freeness: an Introduction for Computer Scientists", institution = "Edinburgh University Computer Science Department", address = "James Clerk Maxwell Building, The King's Buildings, Edinburgh EH9 3JZ, UK", year = 1982, number = "CSR-101-82", type = "Internal Report"} @TECHREPORT{c99-standard, author = "ISO/IEC", title = "Programming languages -- {C}", institution = "International Standards Organization", type = "International Standard", number = "ISO/IEC 9899", year = 1999} @TECHREPORT{camilleri-melham, author = "Juanito Camilleri and Tom Melham", title = "Reasoning with inductively defined relations in the {HOL} theorem prover", institution = CL, address = CLA, year = 1992, number = 265, type = CLT} @TECHREPORT{clarke-zhao, author = "E. Clarke and X. Zhao", title = "Analytica --- a Theorem Prover for {M}athematica", institution = "School of Computer Science, Carnegie Mellon University", year = 1991, type = "Technical Report"} @TECHREPORT{cohn-gordon, author = "Avra Cohn and Mike Gordon", title = "A Mechanized Proof of Correctness of a Simple Counter", institution = CL, address = CLA, year = 1986, number = 94, type = CLT} @TECHREPORT{colmerauer-prolog, author = "A. Colmerauer and H. Kanoi and P. Roussel and R. Pasero", title = "Un syst{\`e}me de Communication Homme-Machine en fran{\c{c}}ais", institution = "Artificial Intelligence Group, University of Aix-Marseilles", address = "Luminay, France", year = 1973} @TECHREPORT{corella-thesis, author = "Francisco Corella", title = "Mechanizing set theory", institution = CL, address = CLA, year = 1990, number = 232, type = CLT, note = "Author's PhD thesis"} @TECHREPORT{cornea-1080, author = "Marius Cornea-Hasegan", title = "Merced Floating Point Algorithms --- Correctness Proofs", institution = "Intel Corporation, Processor Design Document Control", address = "RA2-366, 2501 NE 229th Ave., Hillsboro, OR 97124", number = "OR-1080", year = 1997, note = "Intel top secret document"} @TECHREPORT{curzon-microcode, author = "Paul Curzon", title = "A Structured Approach to the Verification of Low Level Microcode", institution = CL, address = CLA, year = 1991, number = 215, type = CLT, note = "Author's PhD thesis"} @TECHREPORT{dagostino-thesis, author = "Marcello D'Agostino", title = "Investigations into the Complexity of Some Propositional Calculi", institution = "Oxford University Computing Laboratory, Programming Research Group", address = "11 Keble Road, Oxford, OX1 3QD", year = 1990, number = "PRG-88", type = "Technical Monograph", note = "Author's PhD thesis"} @TECHREPORT{degtyarev-voronkov-undecidable, author = "Anatoli Degtyarev and Andrei Voronkov", title = "Simultaneous Rigid {E}-Unification is Undecidable", institution = "Computing Science Department, Uppsala University", address = "Box 311, S-751 05 Uppsala, Sweden", type = "Technical report", number = 105, year = 1995, note = "Also available on the Web as {\verb+ftp://ftp.csd.uu.se/pub/papers/reports/0105.ps.gz+}"} @TECHREPORT{detlefs-simplify, author = "David Detlefs and Greg Nelson and James B. Saxe", title = "Simplify: A Theorem Prover for Program Checking", institution = "HP Labs", type = "Technical Report", number = "HPL-2003-148", year = 2003} @TECHREPORT{dowek-s