%2345678901234567890123456789012345678901234567890123456789012345678901234567890
@book{Albers, editor = "Donald J. Albers and G. L. Alexanderson",
  title = "Mathematical People",
  publisher = "Contemporary Books, Inc.",
  address = "Chicago",
  note = "[QA28.M37]",
  year = 1985 }
@book{Anderson, author = "Alan Ross Anderson and Nuel D. Belnap",
  title = "Entailment",
  publisher = "Princeton University Press",
  address = "Princeton",
  volume = 1,
  note = "[QA9.A634 1975 v.1]",
  year = 1975}
@book{Barrow, author = "John D. Barrow",
  title = "Theories of Everything:  The Quest for Ultimate Explanation",
  publisher = "Oxford University Press",
  address = "Oxford",
  note = "[Q175.B225]",
  year = 1991 }
@book{Behnke,
  editor = "H. Behnke and F. Backmann and K. Fladt and W. S{\"{u}}ss",
  title = "Fundamentals of Mathematics",
  volume = "I",
  publisher = "The MIT Press",
  address = "Cambridge, Massachusetts",
  note = "[QA37.2.B413]",
  year = 1974 }
@book{Bell, author = "J. L. Bell and M. Machover",
  title = "A Course in Mathematical Logic",
  publisher = "North-Holland",
  address = "Amsterdam",
  note = "[QA9.B3953]",
  year = 1977 }
@inproceedings{Blass, author = "Andrea Blass",
  title = "The Interaction Between Category Theory and Set Theory",
  pages = "5--29",
  booktitle = "Mathematical Applications of Category Theory (Proceedings
     of the Special Session on Mathematical Applications
     Category Theory, 89th Annual Meeting of the American Mathematical
     Society, held in Denver, Colorado January 5--9, 1983)",
  editor = "John Walter Gray",
  year = 1983,
  note = "[QA169.A47 1983]",
  publisher = "American Mathematical Society",
  address = "Providence, Rhode Island"}
@proceedings{Bledsoe, editor = "W. W. Bledsoe and D. W. Loveland",
  title = "Automated Theorem Proving:  After 25 Years (Proceedings
     of the Special Session on Automatic Theorem Proving,
     89th Annual Meeting of the American Mathematical
     Society, held in Denver, Colorado January 5--9, 1983)",
  year = 1983,
  note = "[QA76.9.A96.S64 1983]",
  publisher = "American Mathematical Society",
  address = "Providence, Rhode Island" }
@book{Boolos, author = "George S. Boolos and Richard C. Jeffrey",
  title = "Computability and Log\-ic",
  publisher = "Cambridge University Press",
  edition = "third",
  address = "Cambridge",
  note = "[QA9.59.B66 1989]",
  year = 1989 }
@book{Campbell, author = "John Campbell",
  title = "Programmer's Progress",
  publisher = "White Star Software",
  address = "Box 51623, Palo Alto, CA 94303",
  year = 1991 }
@inproceedings{Chou, author = "Shang-Ching Chou",
  title = "Proving Elementary Geometry Theorems Using {W}u's Algorithm",
  pages = "243--286",
  booktitle = "Automated Theorem Proving:  After 25 Years (Proceedings
     of the Special Session on Automatic Theorem Proving,
     89th Annual Meeting of the American Mathematical
     Society, held in Denver, Colorado January 5--9, 1983)",
  editor = "W. W. Bledsoe and D. W. Loveland",
  year = 1983,
  note = "[QA76.9.A96.S64 1983]",
  publisher = "American Mathematical Society",
  address = "Providence, Rhode Island" }
@incollection{Courant, author = "Richard Courant and Herbert Robbins",
  title = "Topology",
  pages = "573--590",
  booktitle = "The World of Mathematics, Volume One",
  editor = "James R. Newman",
  publisher = "Simon and Schuster",
  address = "New York",
  note = "[QA3.W67 1988]",
  year = 1956 }
@book{Curry, author = "Haskell B. Curry",
  title = "Foundations of Mathematical Logic",
  publisher = "Dover Publications, Inc.",
  address = "New York",
  note = "[QA9.C976 1977]",
  year = 1977 }
@book{Davis, author = "Philip J. Davis and Reuben Hersh",
  title = "The Mathematical Experience",
  publisher = "Birkh{\"{a}}user Boston",
  address = "Boston",
  note = "[QA8.4.D37 1982]",
  year = 1981 }
@incollection{deMillo,
  author = "Richard de Millo and Richard Lipton and Alan Perlis",
  title = "Social Processes and Proofs of Theorems and Programs",
  pages = "267--285",
  booktitle = "New Directions in the Philosophy of Mathematics",
  editor = "Thomas Tymoczko",
  publisher = "Birkh{\"{a}}user Boston, Inc.",
  address = "Boston",
  note = "[QA8.6.N48 1986]",
  year = 1986 }
@book{Edwards, author = "Robert E. Edwards",
  title = "A Formal Background to Mathematics",
  publisher = "Springer-Verlag",
  address = "New York",
  note = "[QA37.2.E38 v.1a]",
  year = 1979 }
@book{Enderton, author = "Herbert B. Enderton",
  title = "Elements of Set Theory",
  publisher = "Academic Press, Inc.",
  address = "San Diego",
  note = "[QA248.E5]",
  year = 1977 }
@book{Goodstein, author = "R. L. Goodstein",
  title = "Development of Mathematical Logic",
  publisher = "Springer-Verlag New York Inc.",
  address = "New York",
  note = "[QA9.G6554]",
  year = 1971 }
@book{Guillen, author = "Michael Guillen",
  title = "Bridges to Infinity",
  publisher = "Jeremy P. Tarcher, Inc.",
  address = "Los Angeles",
  note = "[QA93.G8]",
  year = 1983 }
@book{Hamilton, author = "Alan G. Hamilton",
  title = "Logic for Mathematicians",
  edition = "revised",
  publisher = "Cambridge University Press",
  address = "Cambridge",
  note = "[QA9.H298]",
  year = 1988 }
@unpublished{Harrison, author = "John Robert Harrison",
  title = "Metatheory and Reflection in Theorem Proving:
    A Survey and Critique",
  note = "Technical Report
    CRC-053.
    SRI Cambridge,
    Millers Yard, Cambridge, UK,
    1995.
    Available on the Web as
{\verb+http:+}\-{\verb+//www.cl.cam.ac.uk/users/jrh/papers/reflect.dvi.gz+}"}
@TECHREPORT{Harrison-thesis,
        author          = "John Robert Harrison",
        title           = "Theorem Proving with the Real Numbers",
        institution   = "University of Cambridge Computer
                         Lab\-o\-ra\-to\-ry",
        address         = "New Museums Site, Pembroke Street, Cambridge,
                           CB2 3QG, UK",
        year            = 1996,
        number          = 408,
        type            = "Technical Report",
        note            = "Author's PhD thesis,
   available on the Web at
{\verb+http:+}\-{\verb+//www.cl.cam.ac.uk+}\-{\verb+/users+}\-{\verb+/jrh+}%
\-{\verb+/papers+}\-{\verb+/thesis.html+}"}
@book{Herrlich, author = "Horst Herrlich and George E. Strecker",
  title = "Category Theory:  An Introduction",
  publisher = "Allyn and Bacon Inc.",
  address = "Boston",
  note = "[QA169.H567]",
  year = 1973 }
@article{Hindley, author = "J. Roger Hindley and David Meredith",
  title = "Principal Type-Schemes and Condensed Detachment",
  journal = "The Journal of Symbolic Logic",
  volume = 55,
  year = 1990,
  note = "[QA.J87]",
  pages = "90--105" }
@book{Hofstadter, author = "Douglas R. Hofstadter",
  title = "G{\"{o}}del, Escher, Bach",
  publisher = "Basic Books, Inc.",
  address = "New York",
  note = "[QA9.H63 1980]",
  year = 1979 }
@article{Kalish, author = "D. Kalish and R. Montague",
  title = "On {T}arski's Formalization of Predicate Logic with Identity",
  journal = "Archiv f{\"{u}}r Mathematische Logik und Grundlagenfor\-schung",
  volume = 7,
  year = 1965,
  note = "[QA.A673]",
  pages = "81--101" }
@article{Kalman, author = "J. A. Kalman",
  title = "Condensed Detachment as a Rule of Inference",
  journal = "Studia Logica",
  volume = 42,
  number = 4,
  year = 1983,
  note = "[B18.P6.S933]",
  pages = "443-451" }
@book{Kline, author = "Morris Kline",
  title = "Mathematical Thought from Ancient to Modern Times",
  publisher = "Oxford University Press",
  address = "New York",
  note = "[QA21.K516 1990 v.3]",
  year = 1972 }
@book{Klinel, author = "Morris Kline",
  title = "Mathematics, The Loss of Certainty",
  publisher = "Oxford University Press",
  address = "New York",
  note = "[QA21.K525]",
  year = 1980 }
@book{Kramer, author = "Edna E. Kramer",
  title = "The Nature and Growth of Modern Mathematics",
  publisher = "Princeton University Press",
  address = "Princeton, New Jersey",
  note = "[QA93.K89 1981]",
  year = 1981 }
@book{Landau, author = "Edmund Landau",
  title = "Foundations of Analysis",
  publisher = "Chelsea Publishing Company",
  address = "New York",
  edition = "second",
  note = "[QA241.L2541 1960]",
  year = 1960 }
@article{Leblanc, author = "Hugues Leblanc",
  title = "On {M}eyer and {L}ambert's Quantificational Calculus {FQ}",
  journal = "The Journal of Symbolic Logic",
  volume = 33,
  year = 1968,
  note = "[QA.J87]",
  pages = "275--280" }
@article{Lejewski, author = "Czeslaw Lejewski",
  title = "On Implicational Definitions",
  journal = "Studia Logica",
  volume = 8,
  year = 1958,
  note = "[B18.P6.S933]",
  pages = "189--208" }
@book{Margaris, author = "Angelo Margaris",
  title = "First Order Mathematical Logic",
  publisher = "Blaisdell Publishing Company",
  address = "Waltham, Massachusetts",
  note = "[QA9.M327]",
  year = 1967}
@book{Manin, author = "Yu I. Manin",
  title = "A Course in Mathematical Logic",
  publisher = "Springer-Verlag",
  address = "New York",
  note = "[QA9.M29613]",
  year = "1977" }
@article{Mathias, author = "Adrian R. D. Mathias",
  title = "A Term of Length 4,523,659,424,929",
  journal = "Synthese",
  volume = 133,
  year = 2002,
  note = "[Q.S993]",
  pages = "75--86" }
@article{Megill, author = "Norman D. Megill",
  title = "A Finitely Axiomatized Formalization of Predicate Calculus
     with Equality",
  journal = "Notre Dame Journal of Formal Logic",
  volume = 36,
  year = 1995,
  note = "[QA.N914]",
  pages = "435--453" }
@unpublished{Megillc, author = "Norman D. Megill",
  title = "A Shorter Equivalent of the Axiom of Choice",
  month = "June",
  note = "Unpublished",
  year = 1991 }
@article{MegillBunder, author = "Norman D. Megill and Martin W.
    Bunder",
  title = "Weaker {D}-Complete Logics",
  journal = "Journal of the IGPL",
  volume = 4,
  year = 1996,
  pages = "215--225",
  note = "Available on the Web at
{\verb+http:+}\-{\verb+//www.mpi-sb.mpg.de+}\-{\verb+/igpl+}%
\-{\verb+/Journal+}\-{\verb+/V4-2+}\-{\verb+/#Megill+}"}
}
@book{Mendelson, author = "Elliott Mendelson",
  title = "Introduction to Mathematical Logic",
  edition = "second",
  publisher = "D. Van Nostrand Company, Inc.",
  address = "New York",
  note = "[QA9.M537 1979]",
  year = 1979 }
@article{Meredith, author = "David Meredith",
  title = "In Memoriam {C}arew {A}rthur {M}eredith (1904-1976)",
  journal = "Notre Dame Journal of Formal Logic",
  volume = 18,
  year = 1977,
  note = "[QA.N914]",
  pages = "513--516" }
@article{CAMeredith, author = "C. A. Meredith",
  title = "Single Axioms for the Systems ({C},{N}), ({C},{O}) and ({A},{N})
      of the Two-Valued Propositional Calculus",
  journal = "The Journal of Computing Systems",
  volume = 3,
  year = 1953,
  pages = "155--164" }
@article{Monk, author = "J. Donald Monk",
  title = "Provability With Finitely Many Variables",
  journal = "The Journal of Symbolic Logic",
  volume = 27,
  year = 1971,
  note = "[QA.J87]",
  pages = "353--358" }
@article{Monks, author = "J. Donald Monk",
  title = "Substitutionless Predicate Logic With Identity",
  journal = "Archiv f{\"{u}}r Mathematische Logik und Grundlagenfor\-schung",
  volume = 7,
  year = 1965,
  pages = "103--121" }
  %% Took out this from above to prevent LaTeX underfull warning:
  % note = "[QA.A673]",
@book{Moore, author = "A. W. Moore",
  title = "The Infinite",
  publisher = "Routledge",
  address = "New York",
  note = "[BD411.M59]",
  year = 1989}
@book{Munkres, author = "James R. Munkres",
  title = "Topology: A First Course",
  publisher = "Prentice-Hall, Inc.",
  address = "Englewood Cliffs, New Jersey",
  note = "[QA611.M82]",
  year = 1975}
@article{Nemesszeghy, author = "E. Z. Nemesszeghy and E. A. Nemesszeghy",
  title = "On Strongly Creative Definitions:  A Reply to {V}. {F}. {R}ickey",
  journal = "Logique et Analyse (N.\ S.)",
  year = 1977,
  volume = 20,
  note = "[BC.L832]",
  pages = "111--115" }
@unpublished{Nemeti, author = "N{\'{e}}meti, I.",
  title = "Algebraizations of Quantifier Logics, an Overview",
  note = "Version 11.4, preprint, Mathematical Institute, Budapest,
    1994.  A shortened version without proofs appeared in
    ``Algebraizations of quantifier logics, an introductory overview,''
   {\em Studia Logica}, 50:485--569, 1991 [B18.P6.S933]"}
@article{Pavicic, author = "M. Pavi{\v{c}}i{\'{c}}",
  title = "A New Axiomatization of Unified Quantum Logic",
  journal = "International Journal of Theoretical Physics",
  year = 1992,
  volume = 31,
  note = "[QC.I626]",
  pages = "1753 --1766" }
@book{Penrose, author = "Roger Penrose",
  title = "The Emperor's New Mind",
  publisher = "Oxford University Press",
  address = "New York",
  note = "[Q335.P415]",
  year = 1989 }
@book{PetersonI, author = "Ivars Peterson",
  title = "The Mathematical Tourist",
  publisher = "W. H. Freeman and Company",
  address = "New York",
  note = "[QA93.P475]",
  year = 1988 }
@article{Peterson, author = "Jeremy George Peterson",
  title = "An automatic theorem prover for substitution and detachment systems",
  journal = "Notre Dame Journal of Formal Logic",
  volume = 19,
  year = 1978,
  note = "[QA.N914]",
  pages = "119--122" }
@book{Quine, author = "Willard Van Orman Quine",
  title = "Set Theory and Its Logic",
  edition = "revised",
  publisher = "The Belknap Press of Harvard University Press",
  address = "Cambridge, Massachusetts",
  note = "[QA248.Q7 1969]",
  year = 1969 }
@article{Robinson, author = "J. A. Robinson",
  title = "A Machine-Oriented Logic Based on the Resolution Principle",
  journal = "Journal of the Association for Computing Machinery",
  year = 1965,
  volume = 12,
  pages = "23--41" }
@article{RobinsonT, author = "T. Thacher Robinson",
  title = "Independence of Two Nice Sets of Axioms for the Propositional
    Calculus",
  journal = "The Journal of Symbolic Logic",
  volume = 33,
  year = 1968,
  note = "[QA.J87]",
  pages = "265--270" }
@book{Rucker, author = "Rudy Rucker",
  title = "Infinity and the Mind:  The Science and Philosophy of the
    Infinite",
  publisher = "Bantam Books, Inc.",
  address = "New York",
  note = "[QA9.R79 1982]",
  year = 1982 }
@book{Russell, author = "Bertrand Russell",
  title = "Mysticism and Logic, and Other Essays",
  publisher = "Barnes \& Noble Books",
  address = "Totowa, New Jersey",
  note = "[B1649.R963.M9 1981]",
  year = 1981 }
@article{Russell2, author = "Bertrand Russell",
  title = "Recent Work on the Principles of Mathematics",
  journal = "International Monthly",
  volume = 4,
  year = 1901,
  pages = "84"}
@book{Shoenfield, author = "Joseph R. Shoenfield",
  title = "Mathematical Logic",
  publisher = "Addison-Wesley Publishing Company, Inc.",
  address = "Reading, Massachusetts",
  year = 1967,
  note = "[QA9.S52]" }
@book{Smullyan, author = "Raymond M. Smullyan",
  title = "Theory of Formal Systems",
  publisher = "Princeton University Press",
  address = "Princeton, New Jersey",
  year = 1961,
  note = "[QA248.5.S55]" }
@book{Solow, author = "Daniel Solow",
  title = "How to Read and Do Proofs:  An Introduction to Mathematical
    Thought Process",
  publisher = "John Wiley \& Sons",
  address = "New York",
  year = 1982,
  note = "[QA9.S577]" }
@book{Stark, author = "Harold M. Stark",
  title = "An Introduction to Number Theory",
  publisher = "Markham Publishing Company",
  address = "Chicago",
  note = "[QA241.S72 1978]",
  year = 1970 }
@article{Swart, author = "E. R. Swart",
  title = "The Philosophical Implications of the Four-Color Problem",
  journal = "American Mathematical Monthly",
  year = 1980,
  volume = 87,
  month = "November",
  note = "[QA.A5125]",
  pages = "697--707" }
@book{Takeuti, author = "Gaisi Takeuti and Wilson M. Zaring",
  title = "Introduction to Axiomatic Set Theory",
  edition = "second",
  publisher = "Springer-Verlag New York Inc.",
  address = "New York",
  note = "[QA248.T136 1982]",
  year = 1982}
@inproceedings{Tarski, author = "Alfred Tarski",
  title = "What is Elementary Geometry",
  pages = "16--29",
  booktitle = "The Axiomatic Method, with Special Reference to Geometry and
     Physics (Proceedings of an International Symposium held at the University
     of California, Berkeley, December 26, 1957 --- January 4, 1958)",
  editor = "Leon Henkin and Patrick Suppes and Alfred Tarski",
  year = 1959,
  publisher = "North-Holland Publishing Company",
  address = "Amsterdam"}
@article{Tarski1965, author = "Alfred Tarski",
  title = "A Simplified Formalization of Predicate Logic with Identity",
  journal = "Archiv f{\"{u}}r Mathematische Logik und Grundlagenforschung",
  volume = 7,
  year = 1965,
  note = "[QA.A673]",
  pages = "61--79" }
@book{Tymoczko,
  title = "New Directions in the Philosophy of Mathematics",
  editor = "Thomas Tymoczko",
  publisher = "Birkh{\"{a}}user Boston, Inc.",
  address = "Boston",
  note = "[QA8.6.N48 1986]",
  year = 1986 }
@incollection{Wang,
  author = "Hao Wang",
  title = "Theory and Practice in Mathematics",
  pages = "129--152",
  booktitle = "New Directions in the Philosophy of Mathematics",
  editor = "Thomas Tymoczko",
  publisher = "Birkh{\"{a}}user Boston, Inc.",
  address = "Boston",
  note = "[QA8.6.N48 1986]",
  year = 1986 }
@manual{Webster,
  title = "Webster's New Collegiate Dictionary",
  organization = "G. \& C. Merriam Co.",
  address = "Springfield, Massachusetts",
  note = "[PE1628.W4M4 1977]",
  year = 1977 }
@manual{Whitehead, author = "Alfred North Whitehead",
  title = "An Introduction to Mathematics",
  year = 1911 }
@book{PM, author = "Alfred North Whitehead and Bertrand Russell",
  title = "Principia Mathematica",
  edition = "second",
  publisher = "Cambridge University Press",
  address = "Cambridge",
  year = "1927",
  note = "(3 vols.) [QA9.W592 1927]" }
@book{Wolfram,
  author = "Stephen Wolfram",
  title = "Mathematica:  A System for Doing Mathematics by Computer",
  edition = "second",
  publisher = "Addison-Wesley Publishing Co.",
  address = "Redwood City, California",
  note = "[QA76.95.W65 1991]",
  year = 1991 }
@book{Wos, author = "Larry Wos and Ross Overbeek and Ewing Lusk and Jim Boyle",
  title = "Automated Reasoning:  Introduction and Applications",
  edition = "second",
  publisher = "McGraw-Hill, Inc.",
  address = "New York",
  note = "[QA76.9.A96.A93 1992]",
  year = 1992 }

%
%
%[1] Church, Alonzo, Introduction to Mathematical Logic,
% Volume 1, Princeton University Press, Princeton, N. J., 1956.
%
%[2] Cohen, Paul J., Set Theory and the Continuum Hypothesis,
% W. A. Benjamin, Inc., Reading, Mass., 1966.
%
%[3] Hamilton, Alan G., Logic for Mathematicians, Cambridge
% University Press,
% Cambridge, 1988.

%[6] Kleene, Stephen Cole, Introduction to Metamathematics, D.  Van
% Nostrand Company, Inc., Princeton (1952).

%[13] Tarski, Alfred, "A simplified formalization of predicate
% logic with identity," Archiv fur Mathematische Logik und
% Grundlagenforschung, vol. 7 (1965), pp. 61-79.

%[14] Tarski, Alfred and Steven Givant, A Formalization of Set
% Theory Without Variables, American Mathematical Society Colloquium
% Publications, vol. 41, American Mathematical Society,
% Providence, R. I., 1987.

%[15] Zeman, J. J., Modal Logic, Oxford University Press, Oxford, 1973.