@comment{Remarks for future users: - The string commands at the start define frequently-used strings, and may be used (without quotes) anywhere. For example: journal=jar, instead of journal="Journal of Automated Reasoning", These strings may be concatenated using the # operator. See the definition of bams or the booktitle for ijcai5 for examples. - Proceedings are now defined using the proceedings object type, and linked to by using the Crossref command. For example, Crossref="cade15" works more or less like \cite{cade15}. The crossreferenced item (like the proceedings of the conference) must come after the items (like papers in that proceedings) that refer to it. Therefore: - The proceedings are all listed at the end of this file. - The Key= command is not used in (La)TeX, except for alphabetizing entries which have no editor or author. Please omit it, to save space.} @string{aarn="Association for Automated Reasoning Newsletter"} @string{ai="Artificial Intelligence"} @string{amlg="Archiv f{\"{u}}r Mathematische Logik und Grundlagenforschung"} @string{amm="American Mathematical Monthly"} @string{ams="American Mathematical Society"} @string{bams="Bulletin of the " # ams} @string{bsl="Bulletin of Symbolic Logic"} @string{cade="International Conference on Automated Deduction"} @string{cacm="Communications of the ACM"} @string{cmu="Carnegie Mellon University"} @string{mathcmu="Department of Mathematics, " # cmu} @string{mathscicmu="Department of Mathematical Sciences, " # cmu} @string{fm="Fundamenta Mathematicae"} @string{ieeep="IEEE Computer Society Press, Los Alamitos, California, USA"} @string{ieeet="IEEE Transactions on Computers"} @string{ijcai="International Joint Conference on Artificial Intelligence"} @string{jal="Journal of Applied Logic"} @string{jar="Journal of Automated Reasoning"} @string{jacm="Journal of the ACM"} @string{jcss="Journal of Computer and System Sciences"} @string{jlp="The Journal of Logic Programming"} @string{jlc="Journal of Logic and Computation"} @string{jsc="Journal of Symbolic Computation"} @string{jsl="Journal of Symbolic Logic"} @string{lics="IEEE Symposium on Logic in Computer Science"} @string{lncs="Lecture Notes in Computer Science"} @string{lnai="Lecture Notes in Artificial Intelligence"} @string{ma="Mathematische Annalen"} @string{mscs="Mathematical Structures in Computer Science"} @string{nams="Notices of the " # ams} @string{ndjfl="Notre Dame Journal of Formal Logic"} @string{ncai="National Conference on Artificial Intelligence"} @string{proc="Proceedings of the "} @string{tams="Transactions of the " # ams} @string{tcs="Theoretical Computer Science"} @string{tphols="Theorem Proving in Higher Order Logics."} @string{sv="Springer-Verlag"} @string{zml="Zeitschrift fur Mathematische Logic und Grundlagen der Mathematik"} @Book(Ackermann54, Author="W. Ackermann", Title="Solvable Cases of the Decision Problem", Publisher="North-Holland Publishing Co.", Year=1954, Address="Amsterdam") @Article(Ackermann35, Author="Wilhelm Ackermann", Title="Zum {E}liminationsproblem der mathematischen {L}ogik", Journal=ma, Year=1935, Volume=111, Pages="61--63") @Article(Ackermann34, Author="Wilhelm Ackermann", Title="{U}ntersuchungen {\"{u}}ber das {E}liminationsproblem der mathematischen {L}ogik", Journal=ma, Year=1934, Volume=110, Pages="390--413") @InProceedings(Allen88, Author="P. E. Allen and S. Bose and E. M. Clarke and S. Michaylov", Title="Parthenon: A Parallel Theorem Prover for Non-{H}orn Clauses", Crossref="cade9", Pages="764--765") @Book(Anderson75, Author="Anderson, Alan Ross and Belnap, Nuel D. Jr.", Title="Entailment: The Logic of Relevance and Necessity", Publisher="Princeton University Press", Year=1975) @Article(Anderson70, Author="Robert Anderson and W. W. Bledsoe", Title="A Linear Format for Resolution with Merging and a New Technique for Establishing Completeness", Journal=jacm, Year=1970, Volume=17, Pages="525--534") @Misc(AndrewsG, Author="George Andrews", Title="Personal communication") @manual(AndrewsTPS88a1, Title="{{\sc TPS}} User's Manual", Author="Peter B. Andrews and Chad E. Brown and Matthew Bishop and Sunil Issar and Dan Nesmith and Frank Pfenning and Hongwei Xi and Mark Kaminski", Year=2007, url="http://gtps.math.cmu.edu/tps-mans.html", Note="133+vi pp.") @manual(AndrewsTPS88a, Title="{{\sc TPS}} User's Manual", Author="Peter B. Andrews and Matthew Bishop and Chad E. Brown and Sunil Issar and Dan Nesmith and Frank Pfenning and Hongwei Xi", Year=2004, url="http://gtps.math.cmu.edu/tps-mans.html", Note="112+iv pp.") @manual(AndrewsTPS88a-nodate, Title="{{\sc TPS}} User's Manual", Author="Peter B. Andrews and Matthew Bishop and Chad E. Brown and Sunil Issar and Dan Nesmith and Frank Pfenning and Hongwei Xi", url="http://gtps.math.cmu.edu/tps-mans.html") @manual(AndrewsTPS88b, Title="{{\sc ETPS}} User's Manual", Author="Frank Pfenning and Sunil Issar and Dan Nesmith and Peter B. Andrews and Hongwei Xi and Matthew Bishop and Chad E. Brown", Year=2004, url="http://gtps.math.cmu.edu/tps-mans.html", Note="64+ii pp.") @manual(AndrewsTPS88c, Title="{GRADER} Manual", Author="Sunil Issar and Peter B. Andrews and Frank Pfenning and Dan Nesmith", Year=2004, url="http://gtps.math.cmu.edu/tps-mans.html", Note="24+i pp.") @manual(AndrewsTPS88d, Title="{{\sc TPS3}} Facilities Guide for Programmers and Users", Author="Peter B. Andrews and Sunil Issar and Dan Nesmith and Frank Pfenning and Hongwei Xi and Matthew Bishop and Chad E. Brown", Year=2004, Note="364+x pp.", url="http://gtps.math.cmu.edu/tps-mans.html") @manual(AndrewsTPS88e, Title="{{\sc TPS3}} Facilities Guide for Users", Author="Peter B. Andrews and Sunil Issar and Dan Nesmith and Frank Pfenning and Hongwei Xi and Matthew Bishop and Chad E. Brown", Year=2004, url="http://gtps.math.cmu.edu/tps-mans.html", Note="199+vi pp.") @manual(AndrewsTPS88f, Title="{{\sc TPS3}} Programmer's Guide", Author="Peter B. Andrews and Dan Nesmith and Frank Pfenning and Sunil Issar and Hongwei Xi and Matthew Bishop and Chad E. Brown", Year=2004, Note="260+x pp.") @InCollection{Andrews2006, author = "Peter Andrews", title = "Church's Type Theory", booktitle = "The Stanford Encyclopedia of Philosophy", editor = "Edward N. Zalta", url = "http://plato.stanford.edu/archives/fall2006/entries/type-theory-church/", note = "\newline http://plato.stanford.edu/archives/fall2006/entries/type-theory-church/", year = "2006"} @Article{AndrewsBrown2005, Author="Peter B. Andrews and Chad E. Brown", Title="TPS: A Hybrid Automatic-Interactive System for Developing Proofs", Journal=jal, Volume=4, Year=2006, Note="\newline http://dx.doi.org/10.1016/j.jal.2005.10.002", Pages="367--395"} @inproceedings{Andrews2005b, Author="Peter B. Andrews", Title="Proving Theorems of Type Theory Automatically with TPS", Booktitle="Proceedings of the Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference (AAAI-05 / IAAI-05)", Publisher= "AAAI Press", Year="2005", Pages="1676--1677"} @Article(AndrewsBrown2005a, Author="Peter B. Andrews and Chad E. Brown", Title="Proving theorems and teaching logic with TPS and ETPS", Journal=bsl, Year=2005, Pages="108--109", Volume=11, Note="(abstract of contributed talk to the 2004 annual meeting of the Association for Symbolic Logic)") @inproceedings(Andrews2004c, Author="Peter B. Andrews", Title="Some Reflections on Proof Transformations", Booktitle="Mechanizing Mathematical Reasoning: Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday", Editor="D. Hutter and W. Stephan", Publisher= sv, Series = lnai, Volume = 2605, Year="2005", url="http://www.springeronline.com/sgw/cda/frontpage/0,11855,4-102-22-42171167-0,00.html?changeHeader=true", Note="\newline http://www.springeronline.com/sgw/cda/frontpage/0,11855,4-102-22-42171167-0,00.html?changeHeader=true", Pages="14-29") @Article(Andrews2004b, Author="Peter B. Andrews and Chad E. Brown and Frank Pfenning and Matthew Bishop and Sunil Issar and Hongwei Xi", Title="ETPS: A System to Help Students Write Formal Proofs", Journal=jar, Year=2004, Volume=32, url="http://journals.kluweronline.com/article.asp?PIPS=5264938", Note="\newline http://journals.kluweronline.com/article.asp?PIPS=5264938", Pages="75--92") @Article(Andrews2003d, Author="Peter B. Andrews", Title="Herbrand Award Acceptance Speech", Journal=jar, Volume=31, Year=2003, Note="\newline http://journals.kluweronline.com/article.asp?PIPS=5256402", Pages="169--187") @InProceedings(Andrews2003c, Author="Peter B. Andrews", Title="A Universal Automated Information System for Science and Technology", Booktitle="Proceedings of the Cade-19 Workshop: Challenges and Novel Applications for Automated Reasoning", Editor="Simon Colton and Jeremy Gow and Volker Sorge and Toby Walsh", Address="Miami, USA", Year="28th July 2003", Note="Available through www.colognet.org; access Colognet, then Publications and Documents, then Grand Challenges.", Pages="13--18") @TechReport(Andrews2003b, Author="Peter B. Andrews", Title="Herbrand Award Acceptance Speech", Institution=mathscicmu, Number="03-003", Year=2003) @TechReport(Andrews2003a, Author="Peter B. Andrews and Matthew Bishop and Chad E. Brown and Sunil Issar and Frank Pfenning and Hongwei Xi", Title="ETPS: A System to Help Students Write Formal Proofs", Institution=mathscicmu, Number="03-002", Year=2003) @Article(Andrews2002b, Author="Peter B. Andrews", Title="Proving theorems automatically and interactively with TPS", Journal="Abstracts of Papers Presented to the American Mathematical Society", Year=2002, Volume=23, Number=2, Pages="322", Note="Abstract. \newline http://www.math.gatech.edu/$\sim$ belinfan/research/vitae/2081\underline{ }session/2081\underline{ }abstracts/975-03-86.pdf.") @Book(Andrews2002a, Author="Peter B. Andrews", Title="An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof", Edition="second", Publisher="Kluwer Academic Publishers", Year=2002) @InCollection(Andrews00c, Author="Peter B. Andrews", Title="Classical Type Theory", Editor="Alan Robinson and Andrei Voronkov", BookTitle="Handbook of Automated Reasoning", Publisher="Elsevier Science", Address="Amsterdam", Chapter="15", Volume="2", Pages="965--1007", Year="2001") @InProceedings(Andrews00b, Author="Peter B. Andrews and Chad E. Brown", Title="Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic", Note="\newline http://dx.doi.org/10.1007/10721959\underline{ }44", Crossref="cade17", Pages="511--512") @InProceedings(Andrews00a, Author="Peter B. Andrews and Matthew Bishop and Chad E. Brown", Title="System Description: TPS: A Theorem Proving System for Type Theory", Crossref="cade17", Note="\newline http://dx.doi.org/10.1007/10721959\underline{ }11", Pages="164--169") @InCollection(Andrews99, Author="Peter B. Andrews", Title="Classical Type Theory", Editor="Alan Robinson and Andrei Voronkov", BookTitle="Handbook of Automated Reasoning", Publisher="Elsevier Science", Chapter="15", Volume="2", Pages="965--1007", Year="2001") ;;This is identical to Andrews00c, but both labels are used in papers. @inproceedings(Andrews97, Author="Peter B. Andrews and Matthew Bishop", Title="{{\sc TPS}}: A Tool for Proving Theorems", Booktitle="Supplementary " # proc # "10th International Conference on Theorem Proving in Higher Order Logics: TPHOLs'97", Editor="Elsa L. Gunter and Amy Felty", Address="Murray Hill, NJ, USA", Year=1997, Pages="11--15") @InProceedings(Andrews96, Author="Peter B. Andrews and Matthew Bishop", Title="On Sets, Types, Fixed Points, and Checkerboards", Crossref="tableaux96", url="http://dx.doi.org/10.1007/3-540-61208-4\underline{ }1", Note="\newline http://dx.doi.org/10.1007/3-540-61208-4\underline{ }1", Pages="1--15") @Article(Andrews95b, Author="Peter B. Andrews and Matthew Bishop and Sunil Issar and Dan Nesmith and Frank Pfenning and Hongwei Xi", Title="{{\sc TPS}}: A Theorem Proving System for Classical Type Theory", Journal=jar, Volume=16, Year=1996, Pages="321--353", Note="\newline http://dx.doi.org/10.1007/BF00252180") @inproceedings(Andrews95a, Author="Peter B. Andrews", Title="An Example of Proof Search in {{\sc TPS}}: A Theorem Proving System for Classical Type Theory", Booktitle="4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Poster Sessions and Short Papers", Editor="P. Baumgartner and R. H{\"{a}}hnle and J. Posegga", Year=1995, Pages="1--6") @Techreport(Andrews94e, Author="Peter B. Andrews and Matthew Bishop and Sunil Issar and Dan Nesmith and Frank Pfenning and Hongwei Xi", Title="{{\sc TPS}}: A Theorem Proving System for Classical Type Theory", Institution=mathcmu, Number="94-166A", Year=1995) @inproceedings(Andrews94d, Author="Peter B. Andrews", Title="Induction in {{\sc TPS}}: A Theorem Proving System for Classical Type Theory", Booktitle="CADE-12 Workshop on The Automation of Proof by Mathematical Induction", Editor="Alan Bundy and Michael Rusinowitch and Toby Walsh", Year=1994, Pages="2--3", Note="(abstract)") @inproceedings(Andrews94c, Author="Peter B. Andrews", Title="Proof Search in {{\sc TPS}}: A Theorem Proving System for Classical Type Theory", Booktitle="CADE-12 Workshop on Proof-search in type-theoretic languages", Editor="Didier Galmiche and Lincoln Wallen", Year=1994, Pages="3--8", Note="(abstract)") @Techreport(Andrews94b, Author="Peter B. Andrews and Matthew Bishop and Sunil Issar and Dan Nesmith and Frank Pfenning and Hongwei Xi", Title="{{\sc TPS}}: A Theorem Proving System for Classical Type Theory", Institution=mathcmu, Number="94-166", Year=1994) @InProceedings(Andrews94a, Author="Peter B. Andrews and Matthew Bishop and Sunil Issar and Dan Nesmith and Frank Pfenning and Hongwei Xi", Title="{{\sc TPS}}: An Interactive and Automatic Tool for Proving Theorems of Type Theory", Crossref="hug93", url="http://dx.doi.org/10.1007/3-540-57826-9\underline{ }148", Note="\newline http://dx.doi.org/10.1007/3-540-57826-9\underline{ }148", Pages="366--370") @Misc(Andrews92, Author="Peter B. Andrews and Matthew Bishop and Sunil Issar and Dan Nesmith and Frank Pfenning and Hongwei Xi", Title="{{\sc TPS}}: A Theorem Proving System for Classical Type Theory", Date=1993, Note="1993, unpublished.") @Article(Andrews91b, Author="Peter B. Andrews and Sunil Issar and Dan Nesmith and Frank Pfenning", Title="The {{\sc TPS}} Theorem Proving System", Journal=jsl, Year=1992, Pages="353--354", Volume=57, Note="(abstract)") @Article(Andrews91a, Title="More on the Problem of Finding a Mapping Between Clause Representation and Natural-Deduction Representation", Author="Peter B. Andrews", Journal=jar, Year=1991, Pages="285--286", Volume=7) @InProceedings(Andrews90, Author="Peter B. Andrews and Sunil Issar and Dan Nesmith and Frank Pfenning", Crossref="cade10", Title="The {{\sc TPS}} Theorem Proving System", Pages="641--642") @Article(Andrews89, Author="Peter B. Andrews", Title="On Connections and Higher-Order Logic", Journal=jar, Year=1989, Pages="257--291", Volume=5) @InProceedings(Andrews88, Author="Peter B. Andrews and Sunil Issar and Daniel Nesmith and Frank Pfenning", Title="The {{\sc TPS}} Theorem Proving System", Crossref="cade9", Pages="760--761") @Book(Andrews87b, Author="Peter B. Andrews", Title="An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof", Publisher="Japanese translation by Shinako Ogawara, Maruzen Co.", Year=1987) @InProceedings(Andrews87, Author="Peter B. Andrews", Title="Typed $\lambda$-calculus and Automated Mathematics", Booktitle="Mathematical Logic and " # tcs, Editor="David W. Kueker and Edgar G. K. Lopez-Escobar and Carl H. Smith", Series="Lecture Notes in Pure and Applied Mathematics, vol.\ 106", Publisher="Marcel Dekker", Year=1987, Pages="1--14") @Book(Andrews86, Author="Peter B. Andrews", Title="An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof", Publisher="Academic Press", Year=1986) @InProceedings(Andrews86c, Author="Peter B. Andrews", Title="Connections and Higher-Order Logic", Crossref="cade8", Note="abstract", Pages="1--4") @InProceedings(Andrews86d, Author="Peter B. Andrews and Frank Pfenning and Sunil Issar and C. P. Klapper", Title="The {{\sc TPS}} Theorem Proving System", Crossref="cade8", Pages="663--664") @InProceedings(Andrews84, Author="Peter B. Andrews and Dale A. Miller and Eve Longini Cohen and Frank Pfenning", Title="Automating Higher-Order Logic", BookTitle="Automated Theorem Proving: After 25 Years", Publisher=ams, Editor="W. W. Bledsoe and D. W. Loveland", Series="Contemporary Mathematics series, vol.\ 29", Year=1984, Note="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", Pages="169--192") @Article(Andrews81, Title="Theorem Proving via General Matings", Author="Peter B. Andrews", Journal=jacm, Year=1981, Pages="193--214", Volume=28) @InProceedings(Andrews80, Title="Transforming Matings into Natural Deduction Proofs", Author="Peter B. Andrews", Crossref="cade5", Pages="281--292") @Article(Andrews79a, Key="Andrews79a", Author="Peter B. Andrews and Eve Longini Cohen", Title="An approach to theorem proving in type theory", Journal="Journal of Symbolic Logic", Year="1979", Pages="477-478", Volume="44", Note="(abstract)" ) @InProceedings(Andrews79, Author="Peter B. Andrews", Title="General Matings", BookTitle=proc # "Fourth Workshop on Automated Deduction", Publisher="Austin, Texas", Year=1979, Pages="19--25") @Inproceedings(Andrews77, Author="Peter B. Andrews and Eve Longini Cohen", Title="Theorem Proving in Type Theory", Crossref="ijcai5", Pages="566") @Inproceedings(Andrews77b, Author="Peter B. Andrews and Eve Longini Cohen", Title="Theorem Proving in Type Theory", Booktitle="Workshop on Automatic Deduction", Address="Cambridge, Mass.", Organization="MIT", Year=1977, Note="5 pp") @Article(Andrews76, Author="Peter B. Andrews", Title="Refutations by Matings", Journal=ieeet, Volume="C-25", Year=1976, Pages="801--807") @Article(Andrews74a, Author="Peter B. Andrews", Title="Resolution and the Consistency of Analysis", Journal=ndjfl, Year=1974, Volume=15, Number=1, Pages="73--84") @Article(Andrews74b, Author="Peter B. Andrews", Title="Provability in Elementary Type Theory", Journal=zml, Year=1974, Volume=20, Pages="411--418") @Article(Andrews72a, Author="Peter B. Andrews", Title="General Models, Descriptions, and Choice in Type Theory", Journal=jsl, Volume=37, Year=1972, Pages="385--394") @Article(Andrews72b, Author="Peter B. Andrews", Title="General Models and Extensionality", Journal=jsl, Volume=37, Year=1972, Pages="395--397") @Article(Andrews71, Title="Resolution in Type Theory", Author="Peter B. Andrews", Journal=jsl, Year=1971, Pages="414--432", Volume=36) @Article(Andrews71*, Title="Resolution in Type Theory", Author="Peter B. Andrews", Journal=jsl, Year=1971, Pages="414--432", Note="Reprinted in \cite{SiekmannWrightson83b}", Volume=36) @Article(Andrews68a, Author="Peter B. Andrews", Title="On Simplifying the Matrix of a Wff", Journal=jsl, Volume=33, Year=1968, Pages="180--192") @Article(Andrews68a*, Author="Peter B. Andrews", Title="On Simplifying the Matrix of a Wff", Journal=jsl, Volume=33, Year=1968, Note="Reprinted in \cite{SiekmannWrightson83b}", Pages="180--192") @Article(Andrews68b, Author="Peter B. Andrews", Title="Resolution with Merging", Journal=jacm, Volume=15, Year=1968, Pages="367--381") @Article(Andrews68b*, Author="Peter B. Andrews", Title="Resolution with Merging", Journal=jacm, Volume=15, Year=1968, Note="Reprinted in \cite{SiekmannWrightson83b}", Pages="367--381") @Book(Andrews65, Author="Peter B. Andrews", Title="A Transfinite Type Theory with Type Variables", Series="Studies in Logic and the Foundations of Mathematics", Publisher="North-Holland", Year=1965) @article(Andrews63, Author="Peter B. Andrews", Title="A Reduction of the Axioms for the Theory of Propositional Types", Journal=fm, Volume=52, Year=1963, Pages="345--350") @Article(Andrews63b, Author="Burton Dreben and Peter Andrews and St{{\aa}}l Aanderaa", Title="False Lemmas in {H}erbrand", Journal=bams, Volume=69, Year=1963, Pages="699--706") @misc(Andrews62, Author="Peter B. Andrews", Title="A Survey of Artificial Learning and Intelligence", Note="IBM Research Report RC-612, International Business Machines Research Center, Yorktown Heights, New York, 1962") @InProceedings(Anonymous-qed94, Key="QED", Title="The {QED} Manifesto", Crossref="cade12", Pages="238--251") @Article(Appel76, Author="K. Appel and W. Haken", Title="Every Planar Map is Four Colorable", Journal=bams, Year=1976, Volume=82, Pages="711--712") @inproceedings(Asperti2001, Author="Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena", Title="HELM and the Semantic Math-Web", Crossref="tphols01", Pages="59--74") @incollection(BaaderSiekmann94, author="Franz Baader and J{\"{o}}rg Siekmann", year=1994, title="Unification theory", editor="Dov M. Gabbay and C.J. Hogger and J.A. Robinson", booktitle="Handbook of Logic in Artificial Intelligence and Logic Programming", publisher="Oxford University Press", pages="41--125") @InCollection(BaaderSnyder00, Author="Franz Baader and Wayne Snyder", Title="Unification theory", Editor="Alan Robinson and Andrei Voronkov", BookTitle="Handbook of Automated Reasoning", Publisher="Elsevier Science", pages="445--533", Year="2001") @article(Baas94, author="M. Baas and A. Leitsch", title="On Skolemisation and Proof Complexity", journal="Fundamenta Informatic{{\ae}}", year=1994, volume=20, pages="353--379") @Article(Bachmair2003, Author="Leo Bachmair and Ashish Tiwari and Laurent Vigneron", Title="Abstract Congruence Closure", Journal=jar, Volume=31, Year=2003, Pages="129--168") @inproceedings(Bachmair92, author="L. Bachmair and H. Ganzinger and H. Lynch and W. Snyder", title="Basic Paramodulation and Superposition", crossref="cade11", pages="462--476") @Book(Bachmair91, Author="Leo Bachmair", Title="Canonical Equational Proofs", Publisher="Birkh{\"{a}}user", Year=1991, Address="Boston") @inproceedings(Bachmair86, Author="Leo Bachmair and Nachum Dershowitz and Jieh Hsiang", Title="Orderings for Equational Proofs", Crossref="lics1", Pages="346--357") @inproceedings(Bachmair87, Author="Leo Bachmair and Nachum Dershowitz and David Plaisted", Title="Completion Without Failure", Booktitle=proc # "Colloquium on the Resolution of Equations in Algebraic Structures (CREAS)", address="Lakeway, Texas", Year=1987) @Article(Bailin93, Author="Sidney C. Bailin and Dave Barker-Plummer", Title="{Z}-match: An Inference Rule for Incrementally Elaborating Set Instantiations", Journal=jar, Year=1993, Pages="391--428", Volume=11, Note="Errata: JAR 12 (1994), 411--412.") @Article(Bailin88, Author="Sidney C. Bailin", Title="A $\lambda$-Unifiability Test for Set Theory", Journal=jar, Year=1988, Pages="269--286", Volume=4) @inproceedings(Bancerek95, Author="Grzegorz Bancerek", Title="The Mutilated Chessboard Problem --- Checked by {M}izar", Booktitle="The QED Workshop II", Editor="Roman Matuszewski", Year=1995, Pages="43--45", Note="http://www.mcs.anl.gov/qed/index.html") @book(Barendregt84, Author="H. P. Barendregt", Title="The $\lambda$-Calculus", Publisher="Studies in logic and the foundations of mathematics, North-Holland", Year=1984) @Article(Barker-Plummer92, Author="Dave Barker-Plummer", Title="Gazing: An Approach to the Problem of Definition and Lemma Use", Journal=jar, Year=1992, Pages="311--344", Volume=8) @TechReport{BDvH+96, author = "F. Bartels and A. Dold and F. W. v. Henke and H. Pfeifer and H. Rue{\ss}", title = "{Formalizing Fixed-Point Theory in PVS}", institution = "Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik", year = "1996", number = "96-10", type = "Ulmer Informatik-Berichte" } @inproceedings(BarwiseEtchemendy91, Author="Jon Barwise and John Etchemendy", Title="Visual Information and Valid Reasoning", Crossref="ZimmermannCunningham", Pages="9--24") @Article(Bauer98, Author="Andrej Bauer and Edmund Clarke and Xudong Zhao", Title="Analytica --- An Experiment in Combining Theorem Proving and Symbolic Computation", Journal=jar, Volume=21, Year=1998, Pages="295--325") @inproceedings(Baumgartner96, author="Peter Baumgartner and Ulrich Furbach and Ilkka Niemel{\"{a}}", title="Hyper Tableaux", booktitle="Proceedings of JELIA-96, European Workshop on Logic in AI", series=lnai, volume=1126, publisher=sv, year=1996) @techreport(Baumgartner97, author="Peter Baumgartner", title="Hyper Tableaux --- The Next Generation", institution="Fachbereich Informatik, Universit{\"{a}}t Koblenz-Landau", number="32/97", year=1997) @PhdThesis(Baxter77, Author="Lewis D. Baxter", Title="The Complexity of Unification", School="Dept.\ of Math.\ Univ.\ of Waterloo", Note="CS-77-25", Year=1977) @Article(BBK04, Author="Christoph Benzm{\"{u}}ller and Chad E. Brown and Michael Kohlhase", Title="Higher-Order Semantics and Extensionality", Journal=jsl, Volume=69, Year=2004, Pages="1027--1088") @TechReport(BBK03, Author="Christoph Benzm{\"{u}}ller and Chad E. Brown and Michael Kohlhase", Title="Higher Order Semantics and Extensionality", Institution=mathscicmu, Number="03-001", Year=2003) @InProceedings(Beckert94, Author="Bernhard Beckert", Title="A Completion-Based Method for Mixed Universal and Rigid {$E$}-Unification", Crossref="cade12", Pages="678--692") @InProceedings(Beeson2004, author="Michael Beeson", title="Lambda Logic", crossref="ijcar2004", Pages="460--474") @InProceedings(Beeson98, author="Michael Beeson", title="Unification in Lambda-Calculi with if-then-else", crossref="cade15", Pages="103--118") @Article(Behmann22, Author="Heinrich Behmann", Title="Beitrage zur Algebra der {L}ogik, insbesondere zum {E}ntscheidungsproblem", Journal=ma, Year=1922, Volume=86, Pages="163--229") @InProceedings(Belinfante00, Author="Johan Gijsbertus Frederik Belinfante", Title="{G\"{o}}del's Algorithm for Class Formation", Crossref="cade17", Pages="132--147") @article(Belinfante99b, title="On Computer-Assisted Proofs in Ordinal Number Theory", author="J. G. F. Belinfante", journal=jar, year=1999, pages="341--378", volume=22) @article(Belinfante99a, title="{Computer Proofs in G\"{o}}del's Class Theory with Equational Definitions for Composite and Cross", author="J. G. F. Belinfante", journal=jar, year=1999, pages="311--339", volume=22) @article(Belinfante96, title="On a Modification of {G\"{o}}del's Algorithm for Class Formation", author="Johan G. F. Belinfante", journal=aarn, year=1996, month=oct, pages="10--15", volume=34) @Book{BellSlomson71, author = {John Lane Bell and A. B. Slomson}, title = {Models and Ultraproducts: An Introduction}, year = {1971}, publisher = {North-Holland}, address = {Amsterdam} } @incollection(Bentham83, author="Johan {van Benthem} and Kees Doets", year=1983, title="Higher-Order Logic", editor="D. M. Gabbay and F. G{\"{u}}nthner", booktitle="Handbook of Philosophical Logic", volume="I", publisher="Reidel", address="Dordrecht", pages="275--329") @InProceedings(Benzmuller2008c26, author = {Christoph Benzm{\"u}ller and Frank Theiss and Lawrence C. Paulson and Arnaud Fietzke}, title = {{LEO-II} - A Cooperative Automatic Theorem Prover for Higher-Order Logic}, editor = {Alessandro Armando and Peter Baumgartner and Gilles Dowek}, booktitle = {Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings}, url = {www.ags.uni-sb.de/~chris/papers/C26.pdf}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, pages = {162-170}, year = 2008, volume = 5195 ) @InProceedings{Benzmuller2006c23, author = {Christoph Benzm{\"u}ller and Chad E. Brown and Michael Kohlhase}, title = {Cut-Simulation in Impredicate Logics}, booktitle = {Third International Joint Conference on Automated Reasoning (IJCAR'06)}, url = {www.ags.uni-sb.de/~chris/papers/C23.pdf}, publisher = {Springer}, series = {LNAI}, volume = {4130}, pages = {220-234}, year = 2006 } @InProceedings{Benzmuller2006c22, author = {Christoph Benzm{\"u}ller and Helmut Horacek and Henri Lesourd and Ivana Kruijff-Korbayova and Marvin Schiller and Magdalena Wolska}, title = {DiaWOz-II - A Tool for Wizard-of-Oz Experiments in Mathematics}, booktitle = {KI 2006: Advances in Artificial Intelligence: 29th Annual German Conference on AI}, url = {www.ags.uni-sb.de/~chris/papers/C22.pdf}, publisher = {Springer}, series = {LNAI}, year = 2006, note = {To appear} } @InProceedings{Benzmuller2006c21, author = {Mark Buckley and Christoph Benzm{\"u}ller}, title = {An Agent-based Architecture for Dialogue Systems}, booktitle = {Proceedings of the Sixth International Andrei Ershov Memorial Conference 'Perspectives of System Informatics' (PSI'06)}, year = 2006, url = {www.ags.uni-sb.de/~chris/papers/C21.pdf}, publisher = {Springer}, volume = {4837}, pages = {135-147}, series = {lncs}, } @InProceedings{Benzmuller2005c18, author = {C.E. Benzm{\"u}ller and Q.B. Vo}, editor = {M. Veloso and S. Kambhampati}, title = {Mathematical Domain Reasoning Tasks in Natural Language Tutorial Dialog on Proofs}, booktitle = {Proceedings of the Twentieth National Conference on Artificial Intelligence (AAAI-05)}, year = 2005, pages = {516-522}, publisher = {AAAI Press / The MIT Press}, address = {Pittsburgh, Pennsylvania, USA}, url = {www.ags.uni-sb.de/~chris/papers/C18.pdf}, } @InProceedings{Benzmuller2005c17, author = {C.E. Benzm{\"u}ller and C.E. Brown}, editor = {J. Hurd and T. Melham}, title = {A Structured Set of Higher-Order Problems}, booktitle = {Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005)}, year = 2005, number = 3606, pages = {66-81}, series = {LNAI}, publisher = {Springer}, url = {www.ags.uni-sb.de/~chris/papers/C17.pdf}, } @InProceedings{Benzmuller2005w31, author = {Christoph Benzm{\"u}ller}, title = {System Description: LEO -- A Resolution based Higher-Order Theorem Prover}, booktitle = {Proceedings of the LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL)}, year = 2005, pages = {25-44}, address = {Wexford Hotel, Montego Bay, Jamaica}, publisher = {Available from http://arxiv.org/abs/cs/0601042}, } @InProceedings{Benzmuller2005c16, author = {C. Benzm{\"u}ller and V. Sorge and M. Jamnik and M. Kerber}, editor = {F. Baader and A. Voronkov}, title = {Can a Higher-Order and a First-Order Theorem Prover Cooperate?}, booktitle = {Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2004)}, year = 2005, series = {LNAI}, pages = {415-431}, volume = 3452, publisher = {Springer}, url = {www.ags.uni-sb.de/~chris/papers/C16.pdf} } @unpublished{Benzmuller2004a, author = {Christoph Benzm{\"u}ller}, title = {Case for Support. A$\lambda$onzo: Higher-order Reasoning Agents for Mathematics}, year = 2004, note = {Available in German from www.ags.uni-sb.de/~chris/papers/R23.pdf} } @Article{Benzmuller2002, author = {Christoph Benzm{\"u}ller}, title = {Comparing Approaches to Resolution based Higher-Order Theorem Proving}, journal = {Synthese, An International Journal for Epistemology, Methodology and Philosophy of Science}, publisher = {Kluwer}, volume = 133, number = {1-2}, issn = {0039-7857}, pages = {203--235}, year = 2002, url = {www.ags.uni-sb.de/~chris/papers/J5.pdf}, abstract = {We investigate several approaches to resolution based automated theorem proving in classical higher-order logic (based on Church's simply typed lambda calculus) and discuss their requirements with respect to Henkin completeness and full extensionality. In particular we focus on Andrews' higher-order resolution [Andrews71], Huet's constrained resolution [Huet72], higher-order $E$-resolution, and extensional higher-order resolution [BenzmuellerKohlhase98]. With the help of examples we illustrate the parallels and differences of the extensionality treatment of these approaches and demonstrate that extensional higher-order resolution is the sole approach that can completely avoid additional extensionality axioms.} } @InProceedings{Benzmuller2000a, author = {Christoph Benzm{\"u}ller and Volker Sorge}, title = {{OANTS} -- An open approach at combining Interactive and Automated Theorem Proving}, booktitle = {Symbolic Computation and Automated Reasoning}, editor = {Manfred Kerber and Michael Kohlhase}, year = 2000, pages = {81--97}, publisher = {A.K.Peters}, url = {www.ags.uni-sb.de/~chris/papers/C8.pdf}, abstract = {We present the O-ANTS theorem prover that is built on top of an agent-based command suggestion mechanism. The theorem prover inherits beneficial properties from the underlying suggestion mechanism such as run-time extendibility and resource adaptability. Moreover, it supports the distributed integration of external reasoning systems. We also discuss how the implementation and modeling of a calculus in our agent-based approach can be investigated wrt. the inheritance of properties such as completeness and soundness.} } @InProceedings(Benzmuller99b, author="Christoph Benzm{\"{u}}ller", title="Extensional Higher-Order Paramodulation and RUE-Resolution", crossref="cade16", Pages="399--413") @PhdThesis(Benzmuller99a, Author="Christoph Benzm{\"{u}}ller", Title="Equality and Extensionality in Automated Higher-Order Theorem Proving", School="Universit{\"{a}}t des Saarlandes", Year=1999) @article(Benzmuller99, Author="Christoph Benzm{\"{u}}ller and Matthew Bishop and Volker Sorge", Title="Integrating {{\sc TPS}} and {{\sc {$\Omega$}mega}}", journal="Journal of Universal Computer Science", month=mar, Year=1999, pages="188-207", volume=5, number=3, publisher="Springer", note="http://www.iicm.edu/jucs\underline{ }5\underline{ }3/integrating\underline{ }tps\underline{ }and\underline{ }omega") % not url= because that doesn't get printed. @TechReport(Benzmuller98b, Author="Christoph Benzm{\"{u}}ller and Volker Sorge", Title="Integrating {{\sc TPS}} with {{\sc {$\Omega$}mega}}", Institution="Universit{\"{a}}t des Saarlandes", Year=1998) @TechReport(Benzmuller98d, Author="Christoph Benzm{\"{u}}ller", Title="An Adaptation of Paramodulation and {RUE}-resolution to Higher-Order Logic", Institution="Universit{\"{a}}t des Saarlandes", Type="SEKI Report", Number="SR-98-07", Year=1998) @InProceedings(Benzmuller98c, author="Christoph Benzm{\"{u}}ller and Michael Kohlhase", title="System Description: {LEO} --- A Higher-Order Theorem Prover", crossref="cade15", Pages="139--143") @InProceedings(Benzmuller98a, author="Christoph Benzm{\"{u}}ller and Michael Kohlhase", title="Extensional Higher-Order Resolution", crossref="cade15", Pages="56--71") @InProceedings(Benzmuller97, author="C. Benzm{\"{u}}ller and L. Cheikhrouhou and D. Fehrer and A. Fiedler and X. Huang and M. Kerber and M. Kohlhase and K. Konrad and E. Melis and A. Meier and W. Schaarschmidt and J. Siekmann and V. Sorge", title="{{\sc {$\Omega$}mega}}: Towards a Mathematical Assistant", Crossref="cade14", Pages="252--255") @TechReport(Benzmuller97a, Author="Christoph Benzm{\"{u}}ller", Title="A Calculus and a System Architecture for Extensional Higher-Order Resolution", Institution="Department of Mathematical Sciences, " # cmu, Number="97-198", Month=jun, Year=1997) @TechReport{Benzmuller97b, author = {Christoph Benzm{\"u}ller and Michael Kohlhase}, title = {Model Existence for Higher-Order Logic}, institution = {Department of Computer Science, Saarland University}, type = {Seki-Report}, number = {SR-97-09}, year = 1997, pages = {1--34}, url = {www.ags.uni-sb.de/~chris/papers/R5.pdf} } @misc(Bernays36, Author="Paul Bernays", Title="Logical Calculus, lecture notes 1935-36", Howpublished="The Institute for Advanced Study, Princeton, N.J.", Year=1936) @Article(Bernays28, Author="P. Bernays and M. Sch{\"{o}}nfinkel", Title="Zum {E}ntscheidungsproblem der mathematischen {L}ogik", Journal=ma, Year=1928, Volume=99, Pages="342--372") @Book(Beth59, Author="E. W. Beth", Title="The Foundations of Mathematics", Publisher="North-Holland Publishing Co.", Year=1959) @Article(Beth53, Author="Evert W. Beth", Title="On {P}adoa's Method in the Theory of Definition", Journal="Indag.\ Math.", Year=1953, Volume=15, Pages="330--339") % Bibel98a is at the end of the file so it can be used as a crossreference @InProceedings{Bibel97, author = {W. Bibel}, title = {Let's plan it deductively!}, crossref = {IJCAI97}, pages = "1549--1562", } @InProceedings(Bibel95, Author="W. Bibel and S. Bruning and U. Egly and D. Korn and T. Rath", Title="Issues in Theorem Proving Based on the Connection Method", Crossref="tableaux95", Pages="1--16") @InProceedings(Bibel94, Author="W. Bibel and S. Bruning and U. Egly and T. Rath", Title="{KOMET}", Crossref="cade12", Pages="783--787") @book(Bibel93, Author="Wolfgang Bibel", Title="Deduction: Automated Logic", Publisher="Academic Press", Year=1993) @inproceedings(Bibel87a, author="W. Bibel and R. Letz and J. Schumann", title="Bottom-up Enhancements of Deductive Systems", booktitle="Proceedings of 4th International Conference on Artificial Intelligence and Information-Control Systems of Robots", editor="I. Plander", address="Smolenice, CSSR", month=oct, pages="1--10", year=1987, publisher="North-Holland") @Book(Bibel87, Author="Wolfgang Bibel", Title="Automated Theorem Proving", Publisher="Vieweg, Braunschweig", Edition="second", Year=1987) @Article(Bibel84, Author="Wolfgang Bibel and Bruno Buchberger", Title="Towards a Connection Machine for Logical Inference", Journal="Future Generations Computer Systems", Year="1984--1985", Volume=1, Pages="177--185") @Article(Bibel83, Author="Wolfgang Bibel", Title="Matings in Matrices", Journal=cacm, Year=1983, Volume=26, Pages="844--852") @Article(Bibel82a, Author="Wolfgang Bibel", Title="A Comparative Study of Several Proof Procedures", Journal=ai, Year=1982, Volume=18, Pages="269--293") @Book(Bibel82, Author="Wolfgang Bibel", Title="Automated Theorem Proving", Publisher="Vieweg, Braunschweig", Year=1982) @Article(Bibel81, Author="Wolfgang Bibel", Title="On Matrices with Connections", Journal=jacm, Year=1981, Month=oct, Volume=28, Number=4, Pages="633--645") @InProceedings(Bibel80, Author="Wolfgang Bibel", Title="A Theoretical Basis for the Systematic Proof Method", Booktitle="Mathematical Foundations of Computer Science 1980, " # proc # "9th Symposium", Address="Rydzyna, Poland", Editor="P. Dembinski", Series=lncs, Volume=88, Publisher=sv, Year=1980, Pages="154--167") @Article(Bibel79, Author="Wolfgang Bibel", Title="Tautology Testing with a Generalized Matrix Reduction Method", Journal=tcs, Year=1979, Volume=8, Pages="31--44") @InProceedings(Bibel75, Author="Wolfgang Bibel and J. Schreiber", Title="Proof Search in a {G}entzen-like System of First-Order Logic", Booktitle="International Computing Symposium 1975", Editor="E. Gelenbe and D. Potier", Publisher="North-Holland, Amsterdam", Year=1975, Pages="205--212") @inproceedings(Billon96, author="Jean-Paul Billon", title="The Disconnection Method", crossref="tableaux96") @article(Birkhoff34, Author="G. Birkhoff", Title="Applications of Lattice Algebra", Journal="Proc.\ Camb.\ Phil.\ Soc.", Year=1934, Volume=30, Pages="115--122") @PhdThesis(Bishop99a, Author="Matthew Bishop", Title="Mating Search Without Path Enumeration", School="Department of Mathematical Sciences, Carnegie Mellon University", Year=1999, Month=apr, Note="Department of Mathematical Sciences Research Report No.\ 99--223", URL="http://gtps.math.cmu.edu/tps.html") @InProceedings(Bishop99, Author="Matthew Bishop", Title="A Breadth-First Strategy for Mating Search", Crossref="cade16", Pages="359--373") @InProceedings(Bishop98, Author="Matthew Bishop and Peter B. Andrews", Title="Selectively Instantiating Definitions", Crossref="cade15", Note="\newline http://dx.doi.org/10.1007/BFb0054272", Pages="365--380") @Book(Blasius89, Author="K. H. Blasius and H. J. Burckert, editors", Title="Deduction Systems in Artificial Intelligence", Publisher="Ellis Horwood Series in AI", Year=1989) @InProceedings(Blasius88, Author="K. H. Blasius and J. Siekmann", Title="Partial Unification for Graph Based Equational Reasoning", Crossref="cade9", Pages="397--414") @InProceedings(Blasius81, Author="K. Blasius and N. Eisinger and J. Siekmann and G. Smolka and A. Herold and C. Walther", Title="The {M}arkgraph {K}arl Refutation Procedure", Crossref="ijcai7", Pages="511--518") @Article(Bledsoe93, Author="W. W. Bledsoe and Guohui Feng", Title="Set-{V}ar", Journal=jar, Year=1993, Volume=11, Pages="293--314") @InProceedings(Bledsoe83, Author="W. W. Bledsoe", Title="Using Examples to Generate Instantiations of Set Variables", Crossref="ijcai8", Pages="892--901", Annote="ATP-67, University of Texas at Austin, July 1982, 44 pp") @InCollection(Bledsoe79, Author="W. W. Bledsoe", Title="A Maximal Method for Set Variables in Automatic Theorem Proving", Editor="J. E. Hayes and Donald Michie and L. I. Mikulich", BookTitle="Machine Intelligence 9", Publisher="Ellis Harwood Ltd., Chichester, and John Wiley \& Sons", Year=1979, Pages="53--100") @inproceedings(Bledsoe77, author="W. W. Bledsoe", title="Set Variables", crossref="ijcai5", annote="(subsumed by Bledsoe79)", pages="501--510") @Article(Bledsoe77b, Author="W. W. Bledsoe", Title="Non-Resolution Theorem Proving", Journal=ai, Year=1977, Volume=9, Number=1, Pages="1--35") @Article(Bledsoe74, Author="W. W. Bledsoe and Peter Bruell", Title="A Man-Machine Theorem-Proving System", Journal=ai, Year=1974, Volume=5, Number=1, Pages="51--72") @InProceedings(Bohm74, Author="C. Bohm and M. Dezani-Cancaglini", Title="Combinatorial Problems, Combinator Equations, and Normal Forms", Booktitle="Automata, Languages, and Programming", Series=lncs, Volume=14, Publisher=sv, Editor="J. Loeckx", Year=1974, Pages="185--199") @article(Bol91, author="R.N. Bol and K.R. Apt and J.W. Klop", title="An Analysis of Loop Checking Mechanisms for Logic Programming", journal=tcs, volume=85, pages="35--79", year=1991) @Book(Boolos98, Author="George Boolos", Title="Logic, logic, and logic", Publisher="Harvard University Press", Year="1998") @InProceedings(Bose89, Author="Soumitra Bose and Edmund M. Clarke and David E. Long, and S. Michaylov", Title="Parthenon: A Parallel Theorem Prover for Non-{H}orn Clauses", Crossref="lics4", Pages="80--89") @Book(Bourbaki66, Author="Nicolas Bourbaki", Title="Elements of mathematics", Publisher="Hermann", Year="1966", Note="10 volumes. Translation of {\it Elements de mathematique}.") @Article(Bowen73, Author="Kenneth A. Bowen", Title="Cut Elimination in Transfinite Type Theory", Journal=zml, Year=1973, Volume=19, Pages="141--162") @Article(Boyer86, Author="Robert Boyer and Ewing Lusk and William McCune and Ross Overbeek and Mark Stickel and Lawrence Wos", Title="Set Theory in First-Order Logic: Clauses for {G\"{o}}del's Axioms", Journal=jar, Year=1986, Pages="287--327", Volume=2) @Book(BrownARHO, Author="Chad E. Brown", Title="{Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church's Type Theory}", Publisher={College Publications}, series={Studies in Logic: Logic and Cognitive Systems}, volume=10, ISBN="978-1-904987-57-4", Year="2007") @Article(Brown2005a, Author="Chad E. Brown", Title="Set Comprehension in {C}hurch's Type Theory", Journal=bsl, Year=2005, Pages="109", Volume=11, Note="(abstract of contributed talk to the 2004 annual meeting of the Association for Symbolic Logic)") @PhdThesis(Brown2004a, Author="Chad E. Brown", Title="Set Comprehension in {C}hurch's Type Theory", School="Department of Mathematical Sciences, Carnegie Mellon University", Year=2004) @InProceedings(Brown2002, Author="Chad E. Brown", Title="Solving for Set Variables in Higher-Order Theorem Proving", Crossref="cade18", Pages="408--422") @phdthesis(Bruning94, title="Techniques for Avoiding Redundancy in Theorem Proving Based on the Connection Method", author="S. Br{\"{u}}ning", school="TH Darmstadt", year=1994) @incollection(Bruynooghe84, author="M. Bruynooghe and L. M. Pereira", title="Deduction Revision by Intelligent Backtracking", booktitle="Implementations of Prolog", publisher="Ellis Horwood", year=1984, pages="194-215", editor="J. A. Campbell") @article(Bryant86, Author="R.E. Bryant", Title="Graph-Based Algorithms for Boolean Function Manipulation", Journal=ieeet, Year=1986, Pages="677-691", Volume="C-35(8)") @Article(Buchi53, Author={J. Richard B\"{u}chi}, Title="Investigation of the Equivalence of the Axiom of Choice and Zorn's Lemma from the Viewpoint of the Hierarchy of Types", Journal=jsl, Volume=18, Year=1953, Pages="125--135") @Article(Buss94, Author="Samuel R. Buss", Title="On {G\"{o}}del's Theorem on Lengths of Proofs {I}: Number of Lines and Speedup for Arithmetic", Journal=jsl, Volume=59, Year=1994, Pages="737-756") @InProceedings(Cantone97, Author="Domenico Cantone", Title="A Fast Saturation Strategy for Set-Theoretic Tableaux", Crossref="tableaux97", Pages="122-137") @InProceedings(Cantone99, Author="Domenico Cantone and Calogero G. Zarba", Title="A Tableau-Based Decision Procedure for a Fragment of Set Theory Involving a Restricted Form of Quantification", Crossref="tableaux99", Pages="97-112") @InProceedings(Cantone00, Author="Domenico Cantone and Calogero G. Zarba", Title="A tableau calculus for integrating first-order reasoning with elementary set theory reasoning", Crossref="tableaux00", Pages="143-159") @book(Chang73, author="C. Chang and R.C. Lee", title="Symbolic Logic and Mechanical Theorem Proving", publisher="Academic Press", year="1973") @Article(Chester76, Author="Daniel Chester", Title="The Translation of Formal Proofs into {E}nglish", Journal=ai, Year=1976, Volume=7, Pages="261-278") @PhdThesis(Chester73, Author=" Daniel Chester", Title="Formal Logic and the Representation of Lingistic Deep Structure", School="University of California, Berkeley", Year=1973) @Article(Church76, Author="Alonzo Church", Title="Comparison of Russell's resolution of the semantical antinomies with that of Tarski", Journal=jsl, Year=1976, Volume=41, Pages="747-760") @Book(Church56, Author="Alonzo Church", Title="Introduction to Mathematical Logic", Publisher="Princeton University Press", Year=1956, FullAuthor="Alonzo Church", Address="Princeton, N.J.") @Book(Church41, Author="Alonzo Church", Title="The Calculi of Lambda-Conversion", Publisher="Princeton University Press", Series="Annals of Mathematics Studies", Number=6, Year=1941, Note="77 pp.") @Article(Church40, Author="Alonzo Church", Title="A Formulation of the Simple Theory of Types", Journal=jsl, Year=1940, Volume=5, Pages="56-68") @Article(Church36a, Author="Alonzo Church", Title="An Unsolvable Problem of Elementary Number Theory", Journal="Amer.\ J. Math.", Year=1936, Volume=58, Note="Reprinted in \cite{Davis65}", Pages="345-363") @Article(Church36b, Author="Alonzo Church", Title="A Note on the {E}ntscheidungsproblem", Journal=jsl, Year=1936, Volume=1, Pages="40-41", Note="Correction ibid., 101--102") @Article(ChurchRosser36, Author="Alonzo Church and J.B. Rosser", Title="Some Properties of Conversion", Journal=tams, Year=1936, Volume=3, Pages="472--482") @Article(Church33, Author="Alonzo Church", Title="A set of postulates for the foundation of logic (2)", Journal="Annals of Mathematics", Year=1933, Volume=34, Pages="839--864") @Article(Church32, Author="Alonzo Church", Title="A set of postulates for the foundation of logic (1)", Journal="Annals of Mathematics", Year=1932, Volume=33, Pages="346--366") @InProceedings(Clarke94, Author="Edmund Clarke and Xudong Zhao", Title="Combining Symbolic Computation and Theorem Proving: Some Problems of {R}amanujan", Crossref="cade12", Pages="758-763") @misc(Clarke92, Author="Edmund Clarke and Xudong Zhao", Title="Analytica --- A Theorem Prover for Mathematica", Year=1991, Note="unpublished") @Book(Cohen66, FullAuthor="Paul Cohen", Author="P. Cohen", Title="Set Theory and the Continuum Hypothesis", Publisher="W. A. Benjamin, Inc.", Year=1966, Address="New York") @book(Constable86, key="Constable86", Author="R. L. Constable et al", Title="Implementing Mathematics with the {N}uprl Proof Development System", Publisher="Prentice Hall", Year=1986) @Article(CookReckhow79, Author="Stephen A. Cook and Robert A. Reckhow", Title="The Relative Efficiency of Propositional Proof Systems", Journal=jsl, Year=1979, Volume=44, Pages="36-50") @Misc(Coq, Key="Coq", Title="The {C}oq proof assistant", Note="http://coq.inria.fr/") @Article(Coquand88, Author="Thierry Coquand and G\'{e}rard Huet", Title="The Calculus of Constructions", Journal="Information and Computation", Volume=76, Pages="95--120", Year=1988) @InProceedings(Coquand85, Author="Thierry Coquand and G\'{e}rard Huet", Title="Constructions: A Higher Order Proof System for Mechanizing Mathematics", BookTitle="EUROCAL '85: European Conference on Computer Algebra", Address="Linz, Austria", Month=apr, Series=lncs, Volume=203, Publisher=sv, Editor="Bruno Buchberger", Year=1985, Pages="151--184") @inproceedings(Coscoy95, Author="Yann Coscoy and Gilles Kahn and Laurent Th\'{e}ry", Title="Extracting Text from Proofs", Booktitle="Typed Lambda Calculi and Applications : Second International Conference on Typed Lambda Calculi and Applications, TLCA '95", Editor="Mariangiola Dezani-Ciancaglini and Gordon Plotkin", Series=lncs, Volume=902, Publisher=sv, Address="Edinburgh, United Kingdom", Year=1995, Pages="109--123") %511.3 I613T at CMU @InProceedings(Cosmo99, author="Roberto Di Cosmo and Stefano Guerrini", title="Strong Normalization of Proof Nets Modulo Structural Congruences", Crossref="rta99", pages="75--91") @book(CourantRobbins, author="Richard Courant and Herbert Robbins", title="What is Mathematics?", publisher="Oxford University Press", year="1941") @article(Cox81, author="Philip T. Cox and Tomasz Pietrzykowski", title="Deduction Plans: A Basis for Intelligent Backtracking", journal="IEEE Transactions on Pattern Analysis and Machine Intelligence", volume=3, year=1981, pages="52--65") @phdthesis(Cox77, author="Philip T. Cox", title="Deduction Plans: A Graphical Proof Procedure for the First-Order Predicate Calculus", school="University of Waterloo", year=1977) @Article(Craig57, Author="W. Craig", Title="Linear Reasoning. A New Form of the {H}erbrand-{G}entzen Theorem", Journal=jsl, Year=1957, Volume=22, Pages="250-268") @book(Curry58, Author="Haskell B. Curry and Robert Feys", Title="Combinatory Logic", Publisher="Studies in logic and the foundations of mathematics, North-Holland", Year=1958) @InProceedings{Dahn97, author = "B. I. Dahn and J. Gehne and T. Honigmann and A. Wolf", title = "Integration of Automated and Interactive Theorem Proving in {ILF}", pages = "57--60", Crossref= "cade14", } @InProceedings{Dahn96, author = "Bernd I. Dahn and Andreas Wolf", title = "Natural Language Representation and Combination of Automatically Generated Proofs", editor = "F. Baader and K. U. Schulz", booktitle = "Frontiers of Combining Systems: Proceedings of the 1st International Workshop, Munich (Germany)", publisher = "Kluwer Academic Publishers", series = "Applied Logic", month = mar, year = "1996", pages = "175--192", } @Article(Dahn94, Author = "Bernd I. Dahn and Andreas Wolf", Title= "A Calculus Supporting Structured Proofs", Journal= "Journal for Information Processing and Cybernetics (EIK)", Year= 1994, Volume= 30, Pages= "261--276") @Book(Davis77, FullAuthor="Martin Davis", Author="M. Davis", Title="Applied Nonstandard Analysis", Publisher="John Wiley & Sons", Year=1977, Address="New York") @Inproceedings(Davis76, Author="M. Davis and Y. Matijasevic and J. Robinson", Title="{H}ilbert's Tenth Problem {D}iophantine Equations: Positive Aspects of a Negative Solution", Booktitle="Proc.\ Sympos.\ Pure Math", Publishers=ams, Year=1976, Volume=28, Pages="323-378") @Book(Davis65, FullAuthor="Martin Davis", Author="M. Davis", Title="The Undecidable", Publisher="Raven Press", Year=1965, Address="Hewlett, N. Y.") @InProceedings(Davis63, Author="Martin Davis", Title="Eliminating the Irrelevant from Mechanical Proofs", booktitle="Experimental Arithmetic, High Speed Computing and Mathematics", Series="Proceedings of Symposia in Applied Mathematics XV", Publisher=ams, Year=1963, Pages="15-30") @article(Davis60, author="M. Davis and H. Putnam", title="A Computing Procedure for Quantification Theory", journal=jacm, volume=7, year=1960, pages="201--215") @InCollection(deBruijn80, Author="N .G. de Bruijn", Title="A Survey of the Project {AUTOMATH}", Editor="J. P. Seldin and J. R. Hindley", BookTitle="To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism", Publisher="Academic Press", Year=1980, Pages="579-606") @article(Dedekind00, author="R. Dedekind", title="{\"U}ber die von drei {M}oduln erzeugte {D}ualgruppe", Journal=ma, Year=1900, Volume=53, Pages="371--403") @InProceedings(deGroote99, author="Philippe de Groote", title="On the Strong Normalization of Natural Deduction with Permutation-Conversions", Crossref="rta99", pages="45--59") @InProceedings{Degtyarev98b, author = "Anatoli Degtyarev and Yuri Gurevich and Paliath Narendran and Margus Veanes and Andrei Voronkov", title = "The Decidability of Simultaneous Rigid {E}-Unification with One Variable", Crossref="rta98", pages = "181--195"} @article(Degtyarev98, author="Anatoli Degtyarev and Andrei Voronkov", title="What You Always Wanted to Know About Rigid E-Unification", Journal=jar, Year=1998, Volume=20, Pages="47--80") @techreport(Degtyarev97b, author="Anatoli Degtyarev and Andrei Voronkov", title="What You Always Wanted to Know About Rigid {$E$}-Unification", institution="Computing Science Department, Uppsala University, Sweden", number="UPMAIL-143", year=1997) @techreport(Degtyarev97, author="Anatoli Degtyarev and Yuri Gurevich and Paliath Narendran and Margus Veanes and Andrei Voronkov", title="The Decidability of Simultaneous Rigid {$E$}-Unification with One Variable", institution="Computing Science Department, Uppsala University, Sweden", number="UPMAIL-139", note="(to appear in " # tcs # ")", year=1997) @article(Degtyarev96, author="Anatoli Degtyarev and Andrei Voronkov", title="The Undecidability of Simultaneous Rigid E-Unification", Journal=tcs, Year=1996, Volume=166, Pages="291--300") @incollection(Degtyarev95a, author="Anatoli Degtyarev and Andrei Voronkov", title="General Connections via Equality Elimination", editor="M. De Glas and Z. Pawlak", BookTitle="Second World Conference on the Fundamentals of Artificial Intelligence", Address="Paris, France", year=1995, pages="109--120") %WOCFAI'95 @techreport(Degtyarev95, author="Anatoli Degtyarev and Andrei Voronkov", title="General Connections via Equality Elimination", institution="Computing Science Department, Uppsala University, Sweden", number="UPMAIL-93", year=1995) @techreport(Degtyarev95b, author="Anatoli Degtyarev and Andrei Voronkov", title="Simultaneous Rigid {$E$}-Unification is Undecidable", institution="Computing Science Department, Uppsala University, Sweden", number="UPMAIL-105", year=1995) @phdthesis{DeMarco99, author = {Mary DeMarco}, school = {Wesleyan University}, title = {Intuitionistic Semantics for Heriditarily Harrop Logic Programming}, year = {1999} } @misc{demarco-uniform, author = "Mary DeMarco and James Lipton", title = "Uniform Algebras: A Complete semantics for Higher Order Logic programming with {HOHH} Formulae.", year = 2001, url = "citeseer.ist.psu.edu/497979.html" } @incollection(Dershowitz93, author="Nachum Dershowitz", title="A Taste of Rewriting", editor="P.E. Lauer", BookTitle="Functional Programming, Concurrency, Simulation and Automated Reasoning. International Lecture Series 1991--92", year=1993, pages="199--228", Publisher=sv) @InProceedings(Digricoli79, Author="Vincent J. Digricoli", Title="Resolution by Unification and Equality", Booktitle="4th Workshop on Automated Deduction", Editor="William H. Joyner", Address="Austin, Texas", Year=1979) @Article(Dowek2003a, Author="Gilles Dowek and Benjamin Werner", Title="Theorem Proving Modulo", Journal=jsl, Volume=68, Year=2003, Pages="1289--1316") @Article(Dowek2003, Author="Gilles Dowek and Th\'{e}r\`{e}se Hardin and Claude Kirchner", Title="Proof Normalization Modulo", Journal=jar, Volume=31, Year=2003, Pages="32--72") @InCollection(Dowek2001, Author="Gilles Dowek", Title="Higher-Order Unification and Matching", Editor="Alan Robinson and Andrei Voronkov", BookTitle="Handbook of Automated Reasoning", Publisher="Elsevier Science", Address="Amsterdam", Chapter="16", Volume="2", pages="1009--1062", Year="2001") @Book(DrebenGoldfarb79, Author="Dreben, Burton and Goldfarb, Warren D.", Title="The Decision Problem: Solvable Classes of Quantificational Formulas", Publisher="Addison-Wesley Publishing Company", Address="Reading, Massachusetts", Year=1979) @Article(Dreben66, Author="Burton Dreben and John Denton", Title="A Supplement to {H}erbrand", Journal=jsl, Year=1966, Volume=31, Pages="393-398") @Article(Dreben63, Author="Burton Dreben and Peter Andrews and St{{\aa}}l Aanderaa", Title="False Lemmas in {H}erbrand", Journal=bams, Volume=69, Year=1963, Pages="699-706") @Book(Eder90, Author="Elmar Eder", Title="Relative Complexities of First Order Calculi", Publisher="Vieweg Verlag, Braunschweig", Year=1992) @InProceedings(Eder89, Author="Elmar Eder", Title="A Comparison of the Resolution Calculus and the Connection Method, and a New Calculus Generalizing Both Methods", BookTitle="CSL'88 --- 2nd Workshop on Computer Science Logic", Series=lncs, Volume=385, Publisher=sv, Year=1989, Address="Berlin", Editor="E. Borger and H. Kleine Buning and M. M. Richter", Pages="80-98") @InProceedings{Edgar93, author = "A. Edgar and F.J. Pelletier", title = "Natural Language Explanations of Natural Deduction Proofs", pages = "269--278", booktitle = "Proceedings of the First Pacific Rim Conference on Computational Linguistics", address = "Vancouver", year = "1993", } @InProceedings{Egli98, author = "Uwe Egli and Stephan Schmitt", title = "Intuitionistic Proof Transformations and Their Application to Constructive Program Synthesis", pages = "132--144", ISBN = "3-540-64960-3", editor = "Jaques Calmet and Jan Plaza", booktitle = "Proceedings of the International Conference on Artificial Intelligence and Symbolic Computation ({AISC}-98)", series=lnai, volume = "1476", publisher=sv, address = "Berlin", year = "1998", } @article(Egly99, author="Uwe Egly and Stephan Schmitt", title="On Intuitionistic Proof Transformations, their Complexity, and Application to Constructive Program Synthesis", journal="Fundamenta Informaticae", volume=39, year=1999, pages="59--83") @InProceedings(Egly94, author = "Uwe Egly", title = "On the Value of Antiprenexing", Booktitle="Logic programming and automated reasoning : 5th International Conference, LPAR '94, Kiev, Ukraine", Editor="Frank Pfenning", Series=lncs, Volume=822, Publisher=sv, Year=1994, Pages="69--83") %005.11 I613L 1994 at CMU @article(Eisinger91, author="Norbert Eisinger and Hans-J{\"{u}}rgen Ohlbach and Axel Pr{\"{a}}cklein", title="Reduction Rules for Resolution-Based Systems", journal=ai, volume=50, number=2, year=1991, pages="141--181") @InProceedings(Eisinger86, Author="N. Eisinger and H. J. Ohlbach", Title="The {M}arkgraph {K}arl Refutation Procedure {(MKRP)}", Crossref="cade8", Pages="681--682") @InProceedings(Eisinger86b, Author="N. Eisinger", Title="What You always Wanted to Know About Clause Graph Resolution", Crossref="cade8", Pages="316--336") @InProceedings(Ernst73, Author="G.W. Ernst", Title="A Definition-Driven Theorem Prover", Crossref="ijcai3", Pages="51-55") @InProceedings(Farmer00, Author="William M. Farmer", Title="An Infrastructure for Intertheory Reasoning", Crossref="cade17", Pages="115--131") @Article(Farmer93b, author="W. M. Farmer", title="A Simple Type Theory with Partial Functions and Subtypes", journal="Annals of Pure and Applied Logic", year=1993, volume=64, pages="211--240") @Article(Farmer93, Author="William M. Farmer and Joshua D. Guttman and F. Javier Thayer", Title="{IMPS}: An Interactive Mathematical Proof System", Journal=jar, Year=1993, Pages="213--248", Volume=11) @inproceedings(Farmer92, Author="William M. Farmer and Joshua D. Guttman and F. Javier Thayer", title="Little theories", crossref="cade11", pages="567--581") @InProceedings(Farmer90, Author="William M. Farmer and Joshua D. Guttman and F. Javier Thayer", Title="{IMPS}: An Interactive Mathematical Proof System", Crossref="cade10", Pages="653--654") @Article(Farmer90a, author="W. M. Farmer", title="A Partial Functions Version of {C}hurch's Simple Theory of Types", journal=jsl, year=1990, volume=55, pages="1269--91") @InProceedings(Fay79, Author="M. Fay", Title="First-Order Unification in an Equational Theory", Booktitle="4th Workshop on Automated Deduction", Editor="William H. Joyner", Address="Austin, Texas", Year=1979) @Article(Feferman64, Author="Solomon Feferman", Title="Systems of Predicative Analysis", Journal=jsl, Volume=29, Year=1964, Pages="1--30") @InProceedings{FehrerHoracek97, author = {Detlef Fehrer and Helmut Horacek}, title = {Exploiting the Addressee's Inferential Capabilities in Presenting Mathematical Proofs}, crossref = {IJCAI97}, pages = "959--964", } @Article(Felty2000, Author ="Amy Felty", Title = "The Calculus of Constructions as a Framework for Proof Search with Set Variable Instantiation", Journal=tcs, Volume=232, Pages="187--229", Year=2000) @inproceedings{Felty96, AUTHOR = {Amy Felty}, TITLE= {Proof Search with Set Variable Instantiation in the Calculus of Constructions}, EDITOR = {McRobbie, M. A. and Slaney, J. K.}, BOOKTITLE = {Automated Deduction: CADE-13}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {1104}, PUBLISHER = {Springer}, YEAR = {1996}, PAGES = {658--672}} @Techreport(Felty86, Author="Amy P. Felty", Title="Using Extended Tactics to Do Proof Transformations", Institution="Department of Computer and Information Science, University of Pennsylvania", Number="MS-CIS--86--89", Year=1986) @PhdThesis(Fiedler01c, author = {Armin Fiedler}, title = {User-Adaptive Proof Explanation}, school = {Naturwissenschaftlich-Technische Fakult{\"a}t I, Universit{\"a}t des Saarlandes}, address = {Saarbr{\"u}cken, Germany}, year = 2001) @InProceedings(Fiedler01b, Author="Armin Fiedler", Title="P.rex: An Interactive Proof Explainer", Crossref="ijcar2001", Pages="416--420") @InProceedings{Fiedler01a, author = {Armin Fiedler}, title = {Dialog-driven Adaptation of Explanations of Proofs}, booktitle = {Proceedings of the 17th {I}nternational {J}oint {C}onference on {A}rtificial {I}ntelligence ({IJCAI})}, pages = {1295--1300}, year = 2001, editor = "Bernhard Nebel", publisher = "Morgan Kaufmann", address = "Seattle, WA" } @InProceedings{Fiedler99, author = {Armin Fiedler}, title = {Using a Cognitive Architecture to Plan Dialogs for the Adaptive Explanation of Proofs}, crossref = {IJCAI99}, pages = {358--363} } @Book(Fitting2002, Author="M. Fitting", Title={Types, Tableaus, and G\"{o}del's God}, Publisher="Kluwer Academic Publishers", Year=2002) @Book(Fitting90, Author="M. Fitting", Title="First-Order Logic and Automated Theorem Proving", Publisher=sv, Year=1990) @InProceedings(Franke99, author="Andreas Franke and Michael Kohlhase", title="System Description: MATHWEB, an Agent-Based Communication Layer for Distributed Automated Theorem Proving", crossref="cade16", Pages="217--221") @Book(Frege1879, Author="Gottlob Frege", Title="Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens", Publisher="Halle", note="Translated in \cite[pp. 1-82]{Heijenoort67}", Year=1879) @Misc(FreydP, Author="Peter Freyd", Title="Personal communication") @Article(Gallier92, Author="Jean H. Gallier and Paliath Narendran and Stan Raatz and Wayne Snyder", Title="Theorem Proving Using Equational Matings and Rigid {$E$}-Unification", Journal=jacm, Volume=39, Pages="377--429", Year=1992) @inproceedings{GaOh92c, author = "Dov M. Gabbay and Hans J{\"u}rgen Ohlbach", title = "Quantifier elimination in second--order predicate logic", booktitle = "Principles of Knowledge Representation and Reasoning (KR92)", year = 1992, editor = "Bernhard Nebel and Charles Rich and William Swartout", pages = "425--435", publisher = "Morgan Kaufmann", note = "Also published as a Technical Report MPI-I-92-231, Max-Planck-Institut f{\"u}r Informatik, Saarbr{\"u}cken, and in the {\it South African Computer Journal}, 1992", abstract = {An algorithm is presented which eliminates second-order quantifiers over predicate variables in formulae of type $\exists P_1 ,..., P_n\ F$ where $F$ is an arbitrary formula of first--order predicate logic. The resulting formula is equivalent to the original formula - if the algorithm terminates. The algorithm can for example be applied to do interpolation, to eliminate the second--order quantifiers in circumscription, to compute the correlations between structures and power structures, to compute semantic properties corresponding to Hilbert axioms in non classical logics and to compute model theoretic semantics for new logics.}, keywords = {Quantifier Elimination, Resolution}, source = "ftp://pub/guide/staff/ohlbach/publications/conferences/scan.dvi.gz"} @misc(Gallier89c, Author="Jean H. Gallier and Paliath Narendran, David Plaisted and Stan Raatz and Wayne Snyder", Title="An Algorithm for Finding Canonical Sets of Ground Rewrite Rules in Polynomial Time", Note="Submitted to " # jacm) @Article(Gallier89a, Author="Jean H. Gallier and Wayne Snyder", Title="Complete Sets of Transformations for General {$E$}-Unification", Journal=tcs, Volume=67, Pages="203--260", Year=1989) @Article(Gallier89b, Author="Jean H. Gallier and P. Narendran and David Plaisted and Wayne Snyder", Title="Rigid {$E$}-Unification: {NP}-Completeness and Applications to Theorem Proving", Journal="Information and Computation", Volume=87, Pages="129--195", Year=1990) @InProceedings(Gallier88, Author="Jean H. Gallier and Stan Raatz and Wayne Snyder", Title="Rigid {$E$}-Unification and its Applications to Equational Matings", BookTitle="Resolution of Equations in Algebraic Structures: Vol.\ 1, Algebraic Techniques", Editor="Nivat and A{\"{\i}}t-Kaci", Year=1989, Publisher="Academic Press, San Diego", Pages="151--216") @InProceedings(Gallier87a, Author="Jean H. Gallier and Stan Raatz and Wayne Snyder", Title="Theorem Proving Using Rigid {$E$}-Unification: Equational Matings", Crossref="lics2", Pages="338--346", Annote="Computer Science Dept.\ Technical Report File, MS-CIS--87--28, LINC LAB 56, PUMC 87--28") @InProceedings(Gallier87b, Author="Jean H. Gallier and Wayne Snyder", Title="A General Complete {$E$}-Unification Procedure", BookTitle="RTA '87", Address="Bordeaux, France", Year=1987, Pages="216--227") @Book(Gallier86, Author="Jean H. Gallier", Title="Logic for Computer Science. Foundations of Automatic Theorem Proving", Publisher="Harper \& Row", Year=1986) @Book(Gallin75, Author="Daniel Gallin", Title="Intensional and Higher-Order Modal Logic", Publisher="North Holland", Year=1975) @InCollection(Gandy80b, Author="R. O. Gandy", Title="Proofs of Strong Normalization", Editor="J. P. Seldin and J. R. Hindley", BookTitle="To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism", Publisher="Academic Press", Pages="457--477", Year=1980) @InCollection(Gandy80a, Author="R. O. Gandy", Title="An Early Proof of Normalization by {A.M.} {T}uring", Editor="J. P. Seldin and J. R. Hindley", BookTitle="To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism", Publisher="Academic Press", Pages="453--455", Year=1980) @Article(Gandy56, Author="R. O. Gandy", Title="On the Axiom of Extensionality - Part I", Journal=jsl, Volume=21, Year=1956, Pages="36--48") @Article(Garson80, Author="James W. Garson and Paul Mellema", Title="Computer-Assisted Instruction in Logic: {EMIL}", Journal="Teaching Philosophy", Volume=3, Year=1980, Pages="453--478") @Book(Gentzen69, Author="Gerhard Gentzen", Title="The Collected Papers of {G}erhard {G}entzen", Publisher="North-Holland Publishing Co.", Year=1969, Address="Amsterdam", Note="Edited by M. E. Szabo") @InCollection(Gentzen36, FullAuthor="Gerhard Gentzen", Author="G. Gentzen", Title="The Consistency of Elementary Number Theory", BookTitle="The Collected Papers of Gerhard Gentzen", Publisher="North-Holland Publishing Co.", Year=1969, Address="Amsterdam", Editor="M. E. Szabo", Pages="132--213") @Article(Gentzen35a, author="G.~Gentzen", title="{U}ntersuchungen {\"{u}}ber das {L}ogische {S}chlie{{\ss}}en {I} und {II}", journal="Mathematische Zeitschrift", year=1935, volume=39, note="Translated in \cite{Gentzen35}", pages="176--210,405--431") @InCollection(Gentzen35, FullAuthor="Gerhard Gentzen", Author="G. Gentzen", Title="Investigations into Logical Deductions", BookTitle="The Collected Papers of Gerhard Gentzen", Publisher="North-Holland Publishing Co.", Year=1969, Address="Amsterdam", Editor="M. E. Szabo", Pages="68--131") @InCollection(Geuvers95, Author="J. H. Geuvers", Title="The Calculus of Constructions and Higher Order Logic", Editor="Ph. de Groote", BookTitle="The Curry-Howard Isomorphism", Publisher="Academia, Louvain-la-Neuve (Belgium)", Pages="139--191", Year="1995") @article(Gilmore60, author="P.C. Gilmore", title="A Proof Method for Quantification Theory", journal="IBM Journal of Research and Development", volume=4, pages="28--35", year=1960) @Book(Girard87, FullAuthor="Jean-Yves Girard", Author="J. Y. Girard", Title="Proof Theory and Logical Complexity", Publisher="Bibliopolis", Year=1987) @Inproceedings(Giunch89, Author="Fausto Giunchiglia and Toby Walsh", Title="Theorem Proving with Definitions", Booktitle="Proceedings of AISB 89", Series="Society for the Study of Artificial Intelligence and Simulation of Behaviour", Year=1989) @Article(Giunch90, Author="Fausto Giunchiglia and Toby Walsh", Title="A Theory of Abstraction", Journal=ai, Volume="57(2--3)", Year=1992, Pages="323--389") @InProceedings(Giunch96, Author="Fausto Giunchiglia and Adolfo Villafiorita", Title="{ABSFOL}: a Proof Checker with Abstraction", Crossref="cade13", Pages="136--140") @Article(Glanz95, Author="James Glanz", Title="Computer Scientists Rethink Their Discipline's Foundations", Journal="Science", Volume=269, Month=sep, Year=1995, Pages="1363--1364") @Book(Gleason66, Author="Andrew M. Gleason", Title="Fundamentals of Abstract Analysis", Publisher="Addison Wesley", Year=1966) @PhdThesis(Goad80, Author="Goad, Christopher Alan", Title="Computational Uses of the Manipulation of Formal Proofs", School="Stanford", Month=aug, Year=1980) @Book(Godel2003, Author="Kurt {G\"{o}}del", Title="Collected Works, Volume {IV}", Note="Edited by Solomon Feferman, John W. Dawson, Jr., Warren Goldfarb, Charles Parsons, and Wilfried Sieg", Publisher="Clarendon Press", Year=2003) @Book(Godel86, Author="Kurt {G\"{o}}del", Title="Collected Works, Volume {I}", Publisher="Oxford University Press", Year=1986) @Book(Godel40, Author="Kurt {G\"{o}}del", Title="The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory", Publisher="Princeton University Press", Year=1940, Address="Princeton") @Article(Godel36, Author="Kurt {G\"{o}}del", Title="{\"{U}}ber die {L\"{a}}nge von {B}eweisen", Journal="Ergebnisse eines Mathematischen Kolloquiums", Volume=7, Year=1936, Pages="23--24", Note="Translated in \cite{Godel86}, pp.\ 396--399.") @Article(Godel31, Author="Kurt {G\"{o}}del", Title="{\"{U}}ber formal unentscheidbare {S\"{a}}tze der {P}rincipia {M}athematica und verwandter {S}ysteme {I}", Journal="Monatsh.\ Math.\ Phys.", Year=1931, Volume=38, Pages="173--198") @Article(Godel30, Author="Kurt {G\"{o}}del", Title="Die {V}ollstandigkeit der {A}xiome des logischen {F}unktionenkalk{\"{u}}ls", Journal="Monatsh.\ Math.\ Phys.", Year=1930, Volume=37, Pages="349--360") @Article(Goldfarb81, Author="Warren D. Goldfarb", Title="The Undecidability of the Second-Order Unification Problem", Journal=tcs, Volume=13, Year=1981, Pages="225--230") @Article(Goldfarb93, Author="Warren D. Goldfarb", Title={Herbrand's error and G\"{o}del's correction}, Journal="Modern Logic", Volume=3, Number=2, Year=1993, Month="February", Pages="103--118") @Article(Goldson93b, Author="Douglas Goldson and Steve Reeves and Richard Bornat", Title="A Review of Several Programs for the Teaching of Logic", Journal="The Computer Journal", Volume=36, Year=1993, Pages="373--386") @Article(Goldson93, Author="Doug Goldson and Steve Reeves", Title="Using Programs to Teach Logic to Computer Scientists", Journal=nams, Volume=40, Year=1993, Pages="143--148") @misc(Goldson92, Author="Douglas Goldson and Steve Reeves and Richard Bornat", Title="A Review of Several Programs for the Teaching of Logic", Note="Department of Computer Science, Queen Mary and Westfield College, University of London, 1992.") @InProceedings(Goller94, Author="Chr.\ Goller and R. Letz and K. Mayr and J. Schumann", Title="{SETHEO} {V3.2}: Recent Developments", Crossref="cade12", Pages="778--782") @inproceedings(Gordon96, Author="Mike Gordon", Title="Set Theory, Higher Order Logic or Both?", Crossref="tphols9", Pages="191--201") @Book(GordonMelham93, Author="M.J. Gordon and T.F. Melham", Title="Introduction to {HOL}: A Theorem-Proving Environment for Higher-Order Logic", Publisher="Cambridge University Press", Year=1993) @InCollection(Gordon88, Author="Michael J. C. Gordon", Title="{HOL}: A Proof Generating System for Higher-Order Logic", Editor="Graham Birtwistle and P.A. Subrahmanyam", BookTitle="VLSI Specification, Verification, and Synthesis", Publisher="Kluwer Academic Publishers", Year=1988, Pages="73--128") @InCollection(Gordon86, Author="Mike Gordon", Title="Why higher-order logic is a good formalism for specifying and verifying hardware", Editor="G. J. Milne and P. A. Subrahmanyam", BookTitle="Formal Aspects of VLSI Design", Publisher="North-Holland", Pages="153--177", Year=1986) @book(GORDON79, author="Michael J. Gordon and Arthur J. Milner and Christopher P. Wadsworth", title="{E}dinburgh {LCF}. A Mechanised Logic of Computation", series=lncs, volume=78, publisher=sv, year=1979) @book(Graf95, author="Peter Graf", title="Term Indexing", series=lnai, volume=1053, publisher=sv, year=1995) @InProceedings(Goubault94, author = "Jean Goubault", title = "Higher-Order Rigid {E}-Unification", Booktitle="Logic programming and automated reasoning : 5th International Conference, LPAR '94, Kiev, Ukraine", Editor="Frank Pfenning", Series=lncs, Volume=822, Publisher=sv, Year=1994, Pages="129--143") %005.11 I613L 1994 at CMU @PhdThesis(Gould66, Author="William Eben Gould", Title="A Matching Procedure for $\omega$-order Logic", School="Princeton University", Year=1966) @inproceedings(Green69b, Author="Cordell Green", Title="Application of Theorem Proving to Problem Solving", Booktitle="Proceedings of the International Joint Conference on Artificial Intelligence", Editor="Donald E. Walker and Lewis M. Norton", Address="Washington, D.C.", Year=1969, Pages="219--239") @inproceedings(Gurevich97, author="Yuri Gurevich and Andrei Voronkov", title="Monadic Simultaneous Rigid {$E$}-Unification and Related Problems", booktitle="ICALP '97: 24th International Colloquium on Automata, Languages and Programming, Bologna, Italy", publisher=sv, series=lncs, volume=1256, pages="154--165", year=1997, month=jul, note="(to appear in " # tcs # ")") @techreport(Hahnle95, author="Reiner H{\"{a}}hnle and Stefan Klingenbeck", title="{A}-Ordered Tableaux", institution="Universit{\"{a}}t Karlsruhe, Fakult{\"{a}}t f{\"{u}}r Informatik", type="Interner Bericht", number="26/95", year=1995) @Book(Halmos60, FullAuthor="Paul R. Halmos", Author="P. R. Halmos", Title="Naive Set Theory", Publisher="D. Van Nostrand Company Ltd.", Year=1960, Address="Princeton, N.J.") @Book(Hammer95, Author="Eric M. Hammer", Title="Logic and Visual Information", Publisher="CSLI Publications \& FoLLI", Address="Stanford, California", Year="1995") @InCollection(Hanna86, Author="F. K. Hanna and N. Daeche", Title="Specification and Verification Using Higher-Order Logic: A Case Study", Editor="G. J. Milne and P. A. Subrahmanyam", BookTitle="Formal Aspects of VLSI Design", Publisher="North-Holland", Pages="179--213", Year=1986) @inproceedings{Hanna85, author = {F. K. Hanna and N. Daeche}, title = {Specification and Verification using Higher-Order Logic}, year = {1985}, pages = {418--433}, keywords = {}, note = {}, url = {http://www.cs.ukc.ac.uk/pubs/1985/416}, booktitle = {Computer Hardware Description Languages and their Applications}, editor = {Koomen and Moto-oka}, publisher = {North Holland}, } @phdthesis(Harrison96, author="John Robert Harrison", title="Theorem Proving with the Real Numbers", school="Churchill College, Cambridge", year=1996, note="Revised version available as Technical Report TR408, Computer Laboratory, Cambridge University") @Book(Hatcher68, Author="William S. Hatcher", Title="Foundations of Mathematics", Publisher="W. B. Saunders Co.", Year=1968) @incollection(Hazen83, author="A.P. Hazen", year=1983, title="Predicative Logics", editor="D.M. Gabbay and F. Guenthner", booktitle="Handbook of Philosophical Logic", volume="I", pages="331--407", publisher="Reidel", address="Dordrecht") @Book(Heijenoort67, Author="Jean van Heijenoort", Title="From {F}rege to {G\"{o}}del. A Source Book in Mathematical Logic 1879--1931", Publisher="Harvard University Press", Year=1967, Address="Cambridge, Massachusetts") @inproceedings(HELMINK91, author="Leen Helmink and Rene Ahn", title="Goal Directed Proof Construction in Type Theory", booktitle="Logical Frameworks", editor="G\'{e}rard Huet and Gordon Plotkin", publisher="Cambridge University Press", pages="120--148", year=1991) @Article(Henkin96, Author="Leon Henkin", Title="The discovery of my completeness proofs", Journal=bsl, Year=1996, Volume=2, Pages="127--158") @Article(Henkin75, Author="Leon Henkin", Title="Identity as a logical primitive", Journal="Philosophia", Year=1975, Volume=5, Pages="31--45") @Article(Henkin63b, Author="Leon Henkin", Title="A Theory of Propositional Types", Journal=fm, Year=1963, Volume=52, Pages="323--344") @Article(Henkin63a, Author="Leon Henkin", Title="An Extension of the {C}raig-{L}yndon Interpolation Theorem", Journal=jsl, Year=1963, Volume=28, Pages="201--216") @Article(Henkin52, Author="Leon Henkin", Title="A Problem Concerning Provability", Journal=jsl, Year=1952, Volume=17, Pages="160") @Article(Henkin60, Author="Leon Henkin", Title="On Mathematical Induction", Journal=amm, Year=1960, Volume=67, Pages="323--338") @Article(Henkin50, Tag="Henkin50", Author="Leon Henkin", Title="Completeness in the Theory of Types", Journal=jsl, Volume=15, Year=1950, Pages="81--91") @Article(Henkin49, Author="Leon Henkin", Title="The Completeness of the First-Order Functional Calculus", Journal=jsl, Year=1949, Volume=14, Pages="159--166") @inproceedings(Henschen72, Author="Lawrence J. Henschen", Title="N-Sorted Logic for Automated Theorem Proving in Higher-Order Logic", Booktitle=proc # "ACM Conference, Boston", Year=1972, Pages="71--81") @Article(Herbrand30, Author="Jacques Herbrand", Title="Recherches sur la th{\'{e}}orie de la d{\'{e}}monstration", Journal="Travaux de la Soci{\'{e}}t{\'{e}} des Sciences et des Lettres de Varsovie, Classe III Sciences Mathematiques et Physiques", Year=1930, Note="Translated in \cite{Herbrand71}.", Volume=33) @Book(Herbrand71, Author="Jacques Herbrand", Title="Logical Writings", Publisher="Harvard University Press", Year=1971, Note="Edited by Warren D. Goldfarb") @Book(HilbertBernays39, Author="David Hilbert and Paul Bernays", Title="Grundlagen der Mathematik", Publisher="Springer", Volume=2, Year=1939) @Article(Hilbert1927, Author="David Hilbert", Title="Die Grundlagen der Mathematik", Journal="Abhandlungen aus dem mathematischen Seminar der Hamburgischen Universit{\"a}t", Year=1928, Volume=6, note="Translated in \cite[pp. 464--479]{Heijenoort67}", Pages="65--85") @Book(Hindley97, Author="J. Roger Hindley", Title="Basic Simple Type Theory", Publisher="Cambridge University Press", Year=1997) @Book(HindleyLercher72, Author="J. R. Hindley and B. Lercher and J. P. Seldin", Title="Introduction to Combinatory Logic", Publisher="Cambridge University Press", Year=1972, Address="London") @Book(HindleySeldin86, Author="J. R. Hindley and J. P. Seldin", Title="An Introduction to Combinators and the $\lambda$-Calculus", Publisher="Cambridge University Press", Year=1986) @Article(Hintikka55, Author="K. J. J. Hintikka", Title="Notes on Quantification Theory", Journal="Soc.\ Sci.\ Fenn.\ Comment.\ Phys.\ Math", Year=1955, Volume=17) @Book(Hodges1993, Author="Wilfrid Hodges", Title="Model theory", Publisher="Cambridge University Press", Year=1993) @InProceedings{HollandMinkley99, author = {Amanda M. Holland-Minkley and Regina Barzilay and Robert L. Constable}, title = {Verbalization of High-Level Formal Proofs}, crossref = {AAAI99}, pages = {277--284} } @Article{HonsellLenisa99, author = "Furio Honsell and Marina Lenisa", title = "Coinductive Characterizations of Applicative Structures", journal = mscs, year = 1999, volume = 9, pages = "403-435" } @InProceedings{HonsellSannella99, author = "Furio Honsell and Donald Sannella", title = "Pre-logical relations", booktitle = "Proceedings of Computer Science Logic (CSL'99)", pages = "546-561", year = 1999, volume = 1683, Series = lncs, Editor = "J{\"{o}}rg Flum and Mario Rodr{\'{i}}guez-Artalejo", Publisher = sv } @InProceedings(Horacek99, author="Helmut Horacek", title="Presenting Proofs in a Human-Oriented Way", crossref="cade16", Pages="142--156") @Article{Horacek97, author = {Helmut Horacek}, title = {A Model for Adapting Explanations to the User's Likely Inferences}, journal = {User Modeling and User-Adapted Interaction}, year = 1997, volume = 7, pages = {1--55} } @InProceedings{Horacek92, author = {Helmut Horacek}, title = {An Integrated View of Text Planning}, crossref = {DaleEtAl:aoanlg92}, pages = "29--44", } @InProceedings(Hornig82, Author="K.M. H{\"{o}}rnig and W. Bibel", Title="Improvements of a Tautology-Testing Algorithm", Crossref="cade6", Pages="326--341") @InCollection(Howard80, Author="W. A. Howard", Title="The Formula-As-Types Notion of Construction", Editor="J. P. Seldin and J. R. Hindley", BookTitle="To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism", Publisher="Academic Press", Pages="480--490", Year=1980) @InProceedings{HuangFiedler97, author = {Xiaorong Huang and Armin Fiedler}, title = {Proof Verbalization as an Application of {NLG}}, crossref = {IJCAI97}, pages = "965--971", } @InProceedings(Huang96, Author="Xiaorong Huang and Armin Fiedler", Title="Presenting Machine-Found Proofs", Crossref="cade13", Pages="221--225") @InProceedings{Huang96a, author = "Xiaorong Huang", title = "Translating Machine-Generated Resolution Proofs into {ND-Proofs} at the Assertion Level", pages = "399--410", ISBN = "3-540-61532-6", editor = "Norman Foo and Randy Goebel", booktitle = "Proceedings of the Fourth Rim International Conference on Artificial Intelligence ({PRICAI}-96)", series = lnai, volume = "1114", publisher = sv, address = "Berlin", year = "1996", } % month = aug # "~26--30", @PhdThesis{huang94tr, author = "Xiaorong Huang", title = "Human Oriented Proof Presentation: {A} Reconstructive Approach", school = "Fachbereich Informatik, Universit{\"a}t des Saarlandes", year = "1994", address = "Saarbr{\"u}cken, Germany", url = "http://js-sfbsun.cs.uni-sb.de/pub/www/deduktion.html", } @InProceedings{huang94cade, author = "Xiaorong Huang", editor = "Alan Bundy", title = "Reconstructing Proofs at the Assertion Level", Crossref="cade12", pages = "738--752", annote = "ISBN 3-540-58156-1", url = "http://js-sfbsun.cs.uni-sb.de/pub/www/deduktion.html", } @InProceedings{huang94dcss, author = "Xiaorong Huang", editor = "Ashwin Ram and Kurt Eiselt", title = "Proverb: {A} System Explaining Machine-Found Proofs", booktitle = "Proceedings of Sixteenth Annual Conference of the Cognitive Science Society", publisher = "Lawrence Erlbaum Associates", pages = "427--432", address = "Atlanta, USA", year = "1994", annote = "ISBN 0-8058-1803-0,ISSN 1047-1316", url = "http://js-sfbsun.cs.uni-sb.de/pub/www/deduktion.html", } %153.44 C67692PA OVRSZQ-2 at CMU @Article{HuangKerber94, author = "Xiaorong Huang and Manfred Kerber and J{\"o}rn Richts and Arthur Sehn", title = "Planning Mathematical Proofs with Methods", journal = "Journal of Information Processing and Cybernetics, EIK", year = "1994", url = "http://www.ags.uni-sb.de/publications/deduktion/papers/HuKeRiSe-EIK94.ps.gz", volume = "30", number = "5-6", pages = "277--291", } @InProceedings(Huang94b, Author="Xiaorong Huang and Manfred Kerber and Michael Kohlhase and Erica Melis and Dan Nesmith and Jorn Richts and J{\"{o}}rg Siekmann", Title="{KEIM}: A Toolkit for Automated Deduction", Crossref="cade12", Pages="807--810") @InProceedings(Huang94a, Author="Xiaorong Huang and Manfred Kerber and Michael Kohlhase and Erica Melis and Dan Nesmith and Jorn Richts and J{\"{o}}rg Siekmann", Title="$\Omega$-{MKRP}: A Proof Development Environment", Crossref="cade12", Pages="788--792") @InProceedings(Huang90, Author="Xiaorong Huang", Title="Reference Choices in Mathematical Proofs", BookTitle=proc # "9th European Conference on Artificial Intelligence", Editor="Luigia Carlucci Aiello", Publisher="Pitman Publishing", Year=1990, Pages="720--725") @InProceedings(Huang89, Author="Xiaorong Huang", Title="Proof Transformation Towards Human Reasoning Style", BookTitle=proc # "13th German Workshop on Artificial Intelligence", Series="Informatik-Fachberichte 216", Publisher=sv, Editor="D. Metzing", Year=1989, Pages="37--42") @Techreport(Huang89a, Author="Xiaorong Huang", Title="A Human Oriented Proof Presentation Model", Institution="Kaiserslautern University", Type="SEKI Report", Number="SR--89--11", Year=1989) @Book(Huet90, Editor="G\'{e}rard Huet", Title="Logical Foundations of Functional Programming", Publisher="Addison Wesley", Year=1990) @InCollection(HuetOppen80, Author="G\'{e}rard Huet and D. C. Oppen", Title="Equations and Rewrite Rules: a Survey", Booktitle="Formal Language Theory: Perspectives and Open Problems", Publisher="Academic Press", Editor="Ronald V. Book", Year=1980, Pages="349--405") @Book(Huet76, Author="G\'{e}rard Huet", Title="Resolution d'Equations dans les Languages d'Ordre 1,2,...,$\omega$", Publisher="These de Doctorat D'Etat, Universite Paris VII", Year=1976) @COMMENT(Dale --- Huet is classified as a book because we do not want references to say "Phd thesis") @Article(Huet81, Author="G\'{e}rard P. Huet", Title="A Complete Proof of Correctness of the {K}nuth and {B}endix Completion Algorithm", Journal=jcss, Year=1981, Volume=23, Pages="11--21") @Article(Huet75, Author="G\'{e}rard P. Huet", Title="A Unification Algorithm for Typed $\lambda$-Calculus", Journal=tcs, Year=1975, Volume=1, Pages="27--57") @Article(Huet75acc, Author="G\'{e}rard P. Huet", Title="A Unification Algorithm for Typed $\lambda$-Calculus", Journal=tcs, Year=1975, Volume=1, Pages="27--57") @InProceedings(Huet73, Author="G\'{e}rard P. Huet", Title="A Mechanization of Type Theory", Crossref="ijcai3", Pages="139--146") @Article(Huet73b, Author="G\'{e}rard P. Huet", Title="The Undecidability of Unification in Third-order Logic", Journal="Information and Control", Volume=22, Year=1973, Pages="257--267") @PhdThesis(Huet72, Author="G\'{e}rard P. Huet", Title="Constrained Resolution: A Complete Method for Higher Order Logic", School="Case Western Reserve University", Year=1972) @Book(HughesCresswell68, Author="G. E. Hughes and M. J. Cresswell", Title="An Introduction to Modal Logic", Publisher="Methuen & Co., Ltd.", Address="New York", Year=1968) @Book(Hungerford74, author="Thomas W. Hungerford", title="Algebra", year=1974, publisher=sv # " New York, Inc.") @Article{Hutter99, author = {Dieter Hutter and Michael Kohlhase}, title = {Managing Structural Information by Higher-Order Colored Unification}, journal = jar, year = 2000, volume = 25, pages = "123--164" } @inproceedings{Hutter97, AUTHOR = {Dieter Hutter and Michael Kohlhase}, TITLE = {A Coloured Version of the $\lambda$-Calculus}, crossref = {CADE14}, pages = {291--305} } @PhdThesis(Issar91, author="Sunil Issar", Title="Operational Issues in Automated Theorem Proving Using Matings", School=cmu, Year=1991, Note="147 pp.") @inproceedings(Issar90, author="Sunil Issar", title="Path-Focused Duplication: A Search Procedure for General Matings", booktitle="AAAI--90. " # proc # "Eighth " # ncai, year=1990, volume=1, pages="221--226", publisher="AAAI Press/The MIT Press") @Book(Jacobs99, Author="Bart Jacobs", Title="Categorical Logic and Type Theory", Publisher="Elsevier", Year=1999) @inproceedings(Janicic97, author="Predrag Jani{\v{c}}i{\'{c}} and Ian Green and Alan Bundy", title="A Comparison of Decision Procedures in Presburger Arithmetic", booktitle="Proceedings of the VIII International Conference on Logic and Computer Science (LIRA 97)", pages="99-101", address="Novi Sad, Yugoslavia", month=sep, year=1997, note="Also available as Research Report 872, Department of AI, University of Edinburgh") @Article(JensenPietrzykowski76, Author="D.C. Jensen and T. Pietrzykowski", Title="Mechanizing $\omega$-Order Type Theory Through Unification", Journal=tcs, Volume=3, Year=1976, Pages="123--171") @InProceedings(Johann94a, Author="Patricia Johann and Michael Kohlhase", Title="Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading", Crossref="cade12", Pages="620--634") @InProceedings(Johnson94, Author="R. Johnson", Title="A Blackboard Approach to Parallel Temporal Tableaux", Booktitle="Artificial Intelligence, Methodologies, Systems and Applications (AIMSA '94)", Editor="P. Jorrand and V. Sgurev", Address="Sofia, Bulgaria", Publisher="World Scientific, Singapore", Year=1994, Pages="183--192") @article(JonesMiddelburg94, author="C.B. Jones and C.A. Middelburg", title="A Typed Logic of Partial Functions Reconstructed Classically", journal="Acta Informatica", volume=31, number=5, pages="399--430", year=1994) @article(Jordan49, title="Zum {D}edekindschen Axiom in der {T}heorie der {V}erb{\"a}nde", author="P. Jordan", journal="Abhandl.\ Hamburg", year=1949, volume=16, pages="71--73") @incollection(Jouannaud91, author="J.-P. Jouannaud and C. Kirchner", year=1991, title="Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification", editor="J.-L. Lassez and G. Plotkin", booktitle="Computational logic : essays in honor of Alan Robinson", publisher="MIT Press", address="Cambridge, MA") @Article(Kamareddine2002, Author=" Fairouz Kamareddine and Twan Laan and Rob Nederpelt", Title="Types in Logic and Mathematics before 1940", Journal=bsl, Volume=8, Year=2002, Pages="185--245") @Article(Kapur95, Author="D. Kapur and H. Zhang", Title="An Overview of {RRL} ({R}ewrite {R}ule {L}aboratory)", Journal="Computers and Mathematics with Applications", Volume=29, Year=1995, Pages="91--114") @Article(Kemeny50, Author="John G. Kemeny", Title="Type theory vs. set theory", Journal=jsl, Volume=15, Year=1950, Note="(abstract)", Pages="78") @PhdThesis(Kemeny49, Author="John G. Kemeny", Title="Type Theory vs. Set Theory", School="Princeton University", Note="(abstract in \cite{Kemeny50})", Year=1949) @Article(Kerber98, Author="Manfred Kerber and Michael Kohlhase and Volker Sorge", Title="Integrating Computer Algebra into Proof Planing", Journal=jar, Volume=21, Year=1998, Pages="327--355") @Book(Kleene52, Author="S. C. Kleene", Title="Introduction to Metamathematics", Publisher="Van Nostrand", Year=1952) @article(Knaster27, author="B. Knaster", title="Une Th{\'e}or{\`e}me sur les Fonctions d'Ensembles", journal="Annales Soc.\ Polonaise Math.", year=1927, volume=6, pages="133--134") @Book(Kneebone63, Author="G. T. Kneebone", Title="Mathematical Logic and the Foundation of Mathematics", Publisher="D. Van Nostrand Company Ltd.", Year=1963, Address="London") @InProceedings(Knuth70, Author="D.E. Knuth and P.B. Bendix", Title="Simple Word Problems in Universal Algebra", Booktitle="Computational Word Problems in Abstract Algebra", Editor="J. Leech", Publisher="Pergamon Press", Year=1970, Pages="263--297") @InProceedings{Kohlhase2000, author = {Michael Kohlhase}, title = {OMDoc: Towards an Internet Standard for the Administration, Distribution, and Teaching of Mathematical Knowledge}, editor = {John A. Campbell and Eugenio Roanes-Lozano}, booktitle = {Artificial Intelligence and Symbolic Computation: International Conference AISC 2000}, year = 2001, publisher = sv, series = lnai, volume = 1930, pages = "32--52" } @InCollection{Kohlhase98, author = {Michael Kohlhase}, title = {Higher-Order Automated Theorem Proving}, booktitle="Automated Deduction -- A Basis for Applications", publisher="Kluwer", year=1998, editor="Wolfgang Bibel and Peter Schmitt", volume = 1, pages = {431--462} } @InProceedings(Kohlhase95, Author="Michael Kohlhase", Title="Higher-Order Tableaux", Crossref="tableaux95", Pages="294--309") @PhdThesis(Kohlhase94, Author="Michael Kohlhase", Title="A Mechanization of Sorted Higher-Order Logic Based on the Resolution Principle", School="Universit{\"{a}}t des Saarlandes", Year=1994) @TECHREPORT(KohlhaseSR-94-01, AUTHOR="Michael Kohlhase", TITLE="Higher-Order Order-Sorted Resolution", INSTITUTION="Fachbereich Informatik, Universit{\"{a}}t des Saarlandes", YEAR=1994, TYPE="SEKI Report", NUMBER="SR--94-01") @TechReport(Kohlhase93a, Author="Michael Kohlhase", Title="A Unifying Principle for Extensional Higher-Order Logic", Institution=mathcmu, Number="93--153", Month=jan, Year=1993) @Article(Kolodner64, Author="Ignace I. Kolodner", Title="Fixed Points", Journal=amm, Volume=71, Year=1964, Pages="906") @inproceedings(Konrad98b, AUTHOR="Karsten Konrad", Title="{{\sc HOT}}: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux", Crossref="tphols98", Pages="245--261") @TECHREPORT(Konrad98a, AUTHOR="Karsten Konrad", TITLE="{{\sc HOT}}: Implementing Higher-Order Tableaux", INSTITUTION="Fachbereich Informatik, Universit{\"a}t Saarbr{\"u}cken", YEAR=1998, TYPE="SEKI Report", NUMBER="SR--98-03", URL="http://www.ags.uni-sb.de/~konrad/papers/hot.ps.gz", PAGES="15") @Book(Konrad04, author="Karsten Konrad", title="Model Generation for Natural Language Interpretation and Analysis", series=lnai, volume=2953, publisher=sv, year=2004) @InProceedings(Kurfess90, Author="F. Kurfe{\ss}", Title="Potentiality of Parallelism in Logic", Booktitle="Parallelization in Inference Systems: International Workshop Proceedings", Editor="B. Fronh{\"{o}}fer and G. Wrightson", Address="Dagstuhl Castle, Germany", Series=lnai, Volume=590, Publisher=sv, Year=1990, Pages="3--25") @Article(Kowalski75, Author="Robert Kowalski", Title="A Proof Procedure Using Connection Graphs", Journal=jacm, Volume=22, Year=1975, Pages="572--595") @Article{KreitzSchmitt00a, author = "Christoph Kreitz and Stephan Schmitt", title = "A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems", journal = "Information and Computation", year = "2000", volume = "162", number = "1--2", pages = "226--254", } @Article(Kryvyi98, Author="S.L. Kryvyi", Title="Unification Problem in Equational Theories", Journal="Cybernetics and Systems Analysis", Volume=33, Number=6, Year=1998, Pages="874--899") @Techreport(Kozen76, Author="Dexter Kozen", Title="Finitely Presented Algebras", Institution="Computer Science Department, Cornell University", Number="TR 76--294", Year=1976) @Misc(logosphere, Key="logosphere", Title="Logosphere", Note="http://www.logosphere.org/") @InProceedings(Lacey00, Author = "David Lacey and Julian Richardson and Alan Smaill", Title = "Logic Program Synthesis in a Higher-Order Setting", crossref="cl2000", Pages = "87--100") @Book{LambScot86, Author = {J. Lambek and P. Scott}, Title = {{I}ntroduction to {H}igher {O}rder {C}ategorial {L}ogic}, Publisher = {Cambridge University Press, Cambridge, UK}, Year = 1986, Topics = {Category Theory} } @Techreport(Lankford75, Author="D.S. Lankford", Title="Canonical Inference", Institution="University of Texas", Number="ATP--32", Year=1975) @Article(Lee92, Author="Shie-Jue Lee and David A. Plaisted", Title="Eliminating Duplication with the Hyper-Linking Strategy", Journal=jar, Volume=9, Year=1992, Pages="25--42") @phdthesis(Lee90, Author="Shie-Jue Lee", Title="{CLIN}: An Automated Reasoning System Using Clause Linking", school="University of North Carolina at Chapel Hill", year=1990) @Article(Lee89, Author="Shie-Jue Lee and David A. Plaisted", Title="Theorem Proving Using Hyper-Matching Strategy", Journal="Methodologies for Intelligent Systems", Volume=4, Year=1989, Pages="467--476") @Misc(LEGO, Key="LEGO", Title="The {LEGO} {P}roof {A}ssistant", Note="http://www.dcs.ed.ac.uk/home/lego/") @incollection(Leivant94, author="Daniel Leivant", year=1994, title="Higher Order Logic", editor="Dov M. Gabbay and C.J. Hogger and J.A. Robinson", booktitle="Handbook of Logic in Artificial Intelligence and Logic Programming", volume=2, publisher="Oxford University Press", pages="229--321") @techreport(Letz92a, author="Reinhold Letz", institution="TU Munich", month=jun, number="FKI--169--92", title="Connection Tableaux and their Relation with Linear Resolution", type="Forschungsberichte {KI}", year=1992) @InProceedings(Letz98, author="Letz, Reinhold", title="Using Matings for Pruning Connection Tableaux", crossref="cade15", pages="381--396") @Article(Letz92, Author="R. Letz and J. Schumann and S. Bayerl and W. Bibel", Title="{SETHEO}: A High-Performance Theorem Prover", Journal=jar, Year=1992, Pages="(183--212)", Volume=8) @Book(LewisLangford51, Author="Lewis, Clarence Irving and Langford, Cooper Harold", Title="Symbolic Logic", Publisher="Dover Publications", Year=1951) @PhdThesis(lingenfelder90, Author="Christoph Lingenfelder", Title="Transformation and Structuring of Computer Generated Proofs", School="University of Kaiserslautern", Year=1990, Note="115 pp.") @techreport(lingenfelder86, Author="Christoph Lingenfelder", Title="Transformation of Refutation Graphs into Natural Deduction Proofs", Institution="SEKI", Number="SR--86--10", Year=1986) @techreport(lingenfelder88, Author="Christoph Lingenfelder", Title="Structuring Computer Generated Proofs", Institution="SEKI", Number="SR--88--19", Year=1988) @inproceedings(lingenfelder89, author="Christoph Lingenfelder", title="Structuring Computer Generated Proofs", crossref="ijcai11", pages="378--383") @InCollection(Loader94, Author="R. Loader", Title="The Undecidability of Lambda Definability", Editor="M.Zeleny", BookTitle="Festschrift for A. Church", Publisher="University of Chicago Press", Year=1994) @Article(Lloyd95, Author="Seth Lloyd", Title="Quantum-Mechanical Computers", Journal="Scientific American", Volume=273, Month=oct, Year=1995, Pages="140--145") @Article(Lob55, Author="M.H. L{\"{o}}b", Title="Solution to a Problem of {L}eon {H}enkin", Journal=jsl, Year=1955, Volume=20, Pages="115--118") @Article(Loveland99, Author="Donald W. Loveland", Title="Automated Deduction: Looking Ahead", Journal="AI Magazine", Volume=20, Year=1999, Note="Slightly modified version of \cite{Loveland97}", Pages="77--98") @Misc(Loveland97, Author="Donald W. Loveland", Title="Automated Deduction. Some Achievements and Future Directions", Note="Report to the National Science Foundation of a Workshop on the Future Directions of Automated Deduction, April 20-21, 1996, Chicago.") @Article(Loveland68, Author="Donald W. Loveland", Title="Mechanical Theorem Proving by Model Elimination", Journal=jacm, Volume=15, Year=1968, Pages="236--251") @Article(Lowenheim15, Author="Leopold L{\"{o}}wenheim", Title="{\"{U}}ber {M\"{o}}glichkeiten im {R}elativkalk{\"{u}}l", Journal=ma, Year=1915, Volume=76, Pages="xque447--470") @Article(Lyndon59, Author="Roger C. Lyndon", Title="An Interpolation Theorem in the Predicate Calculus", Journal="Pacific J. Math", Year=1959, Volume=9, Pages="129--142") @Book(MacLane98, Author="Saunders MacLane", Title="Categories for the Working Mathematician", Edition="second", Publisher=sv, Year=1998, ISBN="0-387-98403-8") @Book(MacLane92, Author="Saunders MacLane and Ieke Moerdijk", Title="Sheaves in Geometry and Logic: A First Introduction to Topos Theory", Publisher=sv, Year=1992) @Article(Mairson92, Author="H. Mairson", Title="A Simple Proof of a Theorem of {S}tatman", Journal=tcs, Year=1992, Volume=103, Pages="387--394") @Book(Manna77, Author="Zohar Manna and Richard Waldinger", Title="Studies in Automatic Programming Logic", Publisher="North-Holland", Address="New York", Year=1977) @Book(Manna74, Author="Zohar Manna", Title="Mathematical Theory of Computation", Publisher=" McGraw-Hill", Year=1974, Note="448 pp.") @Article(Marshall91, Author="M. Victoria Marshall and Rolando Chuaqui", Title="Sentences of type theory: the only sentences preserved under isomorphisms", Journal=jsl, Year=1991, Volume=56, Pages="932--948") @Article(Martin-Lof73, Author="P. Martin-Lof", Title="Hauptsatz for Intuitionistic Simple Type Theory", Journal=zml, Year=1973, Volume=19, Pages="279") @Article{Marti-Oliet96, title = "Inclusions and Subtypes {II}: Higher-order Case", author = "Narciso Mart{\'\i}-Oliet and Jos{\'e} Meseguer", pages = "541--572", journal = jlc, year = "1996", month = aug, volume = "6", number = "4", } @Article(Maslov67, Author="S. Ju. Maslov", Title="An Inverse Method for Establishing Deducibility of Nonprenex Formulas of Predicate Calculus", Journal="Soviet Mathematics Doklady", Year=1967, Volume=8, Pages="16--19") @Misc(MathWeb, Key="MathWeb", Title="MathWeb.org: supporting mathematics on the web!", Note="http://www.mathweb.org/") @Article(Mayr97, Author="R. Mayr and T. Nipkow", Title="Higher-Order Rewrite Systems and Their Confluence", Journal=tcs, Year=1997) @inproceedings(McCarthy95b, Author="John McCarthy", Title="The Mutilated Checkerboard in Set Theory", Booktitle="The QED Workshop II", Editor="Roman Matuszewski", Year=1995, Pages="25--26", Note="Available from http://www.mcs.anl.gov/qed/index.html.") @misc(McCarthy95a, Author="John McCarthy", Title="http://www-formal.stanford.edu/jmc/nut.html.") @misc(McCarthy64, Author="John McCarthy", Title="A Tough Nut for Proof Procedures", Note="Stanford Artificial Intelligence Project Memo No.\ 16, 1964. Available from {{\tt http://www-formal.stanford.edu/jmc/}}.") @incollection(McCune97, author="William McCune", title="33 Basic Test Problems: A Practical Evaluation of Some Paramodulation Strategies", booktitle="Automated Reasoning and its Applications: Essays in Honor of Larry Wos", editor="Robert Veroff", pages="71--114", publisher="MIT Press", year=1997) @Article(McCune95, Author="William McCune", Title="Another Crack in a Tough Nut", Journal=aarn, Volume=31, Year=1995, Pages="1--3") @Article(McCune92, Author="William McCune", Title="Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval", Journal=jar, Volume=9, Number=2, Year=1992, Pages="147--167") @Book(McLarty95, Author="Colin McLarty", Title="Elementary Categories, Elementary Toposes", Publisher="Oxford University Press", Year=1995, ISBN="0-19-851473-5") @InProceedings{Meier00, author = {Andreas Meier}, title = {System Description: {\sc Tramp}: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level}, booktitle = {{A}utomated {D}eduction -- CADE-17}, crossref = {cade17}, pages = {460--464} } @Book(MelhamCamilleri94, Author="T. F. Melham and J. Camilleri, eds.", Title="Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop", address="Valletta, Malta", series=lncs, volume=859, publisher=sv, Year=1994) @Book(Mendelson87, Author="Elliott Mendelson", Title="Introduction to Mathematical Logic", Publisher="Wadsworth \& Brooks/Cole Advanced Books \& Software", Year=1987, Edition="third") @Book(Mendelson64, FullAuthor="Elliott Mendelson", Author="E. Mendelson", Title="Introduction to Mathematical Logic", Publisher="D. Van Nostrand Company Ltd.", Year=1964, Address="Princeton, N.J.") @Techreport(Mendler86, Author="Mendler", Title="Recursive Types and Strong Normalization", Institution="Computer Science Department, Cornell University", Number="TR 86--764", Year=1986) @Article(Meredith53, Author="Carew A. Meredith", Title="Single Axioms for the Systems $(C,\ N),(C,\ O),$ and $(A,\ N)$ of the Two-Valued Propositional Calculus", Journal="J. Comput.\ Systems", Year=1953, Volume=1, Pages="155--164") @InProceedings(MeyerWand, Author="A. R. Meyer and M. Wand", Title="Continuation Semantics in Typed Lambda-Calculi", Booktitle="Logics of Programs", Series=lncs, volume=193, Publisher=sv, Year=1985, Editor="Rohit Parikh", Pages="219--224") @article(Middeldorp94, Author="A. Middeldorp and E. Hamoen", Title="Completeness Results for Basic Narrowing", Journal="Journal of Applicable Algebra in Engineering, Communication and Computing", Volume=5, Year=1994, Pages="213--253") @article{Miller91, AUTHOR ="Dale A. Miller", Title="A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification", Journal=jlc, Volume=1, Number=4, Year=1991, Pages="497--536" } @Article(Miller87, Author="Dale A. Miller", Title="A Compact Representation of Proofs", Journal="Studia Logica", Year=1987, Volume=46, Number=4, Pages="347--370") @InProceedings(Miller84, Author="Dale A. Miller", Title="Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs", Crossref="cade7", Pages="375--393") @PhdThesis(Miller83, Author="Dale A. Miller", Title="Proofs in Higher-Order Logic", School=cmu, Address="Department of Mathematics", Year=1983, Note="81 pp.") @InProceedings(millerfelty86, Title="An Integration of Resolution and Natural Deduction Theorem Proving", Author="Dale Miller and Amy Felty", Booktitle="AAAI--86. Fifth " # ncai, Address="Philadelphia, PA", Month=aug, Year=1986, Editor="Tom Kehler and Stan Rosenschein and Robert Filman and Peter F. Patel-Schneider", Pages="198--202") @manual(MillerPfenning83a, Title="{{\sc TPS}} User Manual", Author="Dale A. Miller and Frank Pfenning", Edition="11th", Year=1983, Note="99 pp.") @manual(MillerPfenning83b, Title="{{\sc TPS}} Software Manual", Author="Peter Andrews and Sunil Issar and Dale Miller and Frank Pfenning", Year=1984, Note="107 pp.") @InProceedings(Miller82, Author="Dale A. Miller and Eve Longini Cohen and Peter B. Andrews", Title="A Look at {{\sc TPS}}", Crossref="cade6", Pages="50--69") @Article(Milner78, author="Robin Milner", title="A Theory of Type Polymorphism in Programming", journal=jcss, volume=17, month=aug, year=1978, pages="348--375") @PhdThesis(Minor79, Author="John Minor", Title="Proving a Subset of Second-Order Logic with First-Order Proof Procedures", School="University of Texas at Austin", Month=aug, Year=1979) @Book{Mitchell96, Author = "John C. Mitchell", Title = "Foundations for Programming Languages", Publisher = "MIT Press", Year = 1996, Series = "Foundations of Computing", ISBN = "0-262-13321-0", } @Book(Moore82, Author="Gregory H. Moore", Title="Zermelo's Axiom of Choice : Its Origins, Development, and Influence", Publisher="Springer-Verlag", Year=1982) @Book(Mostowski66, FullAuthor="Andrzej Mostowski", Author="A. Mostowski", Title="Thirty Years of Foundational Studies", Publisher="Barnes & Noble, Inc.", Year=1966, Address="New York") @InProceedings(Muller94, Author="Olaf M{\"{u}}ller and Franz Weber", Title="Theory and Practice of Minimal Modular Higher-Order {$E$}-Unification", Crossref="cade12", Pages="650--664") @Book{Munkres75, Author = "James R. Munkres", Year = "1975", Title = "{Topology: A First Course}", Publisher = "Prentice-Hall", } @article(Murray93, author="Neil V. Murray and Erik Rosenthal", title="Dissolution: Making Paths Vanish", journal=jacm, volume=40, number=3, month=jul, year=1993, pages="504--535") @InProceedings(MurrayRosenthal90, Author="Neil V. Murray and Eric Rosenthal", Title="{DISSOLVER}: A Dissolution-Based Theorem Prover", Crossref="cade10", Pages="665--666") @InProceedings(MurrayRosenthal88, Author="Neil V. Murray and Eric Rosenthal", Title="An Implementation of a Dissolution-Based System Employing Theory Links", Crossref="cade9", Pages="658--674") @Article(MurrayRosenthal87, Author="Neil V. Murray and Eric Rosenthal", Title="Inference with Path Resolution and Semantic Graphs", Journal=jacm, Volume=34, Year=1987, Pages="225--254") @Article(Muskens2007, Author="Reinhard Muskens", Title="Intensional Models for the Theory of Types", Journal=jsl, Volume=72, Year=2007, Pages="98--118") @Article(Myers90, Author="Brad A. Myers and Dario A. Giuse and Roger B. Dannenberg and Brad Vander Zanden and David S. Kosbie and Edward Pervin and Andrew Mickish and Philippe Marchal", Title="Garnet: Comprehensive Support for Graphical, Highly-Interactive User Interfaces", Journal=ieeet, year=1990, Volume=23, number=11, month=nov, Pages="71--85") @Article(Narendran97, Author="P. Narendran and F. Pfenning and R. Statman", Title="On the Unification Problem for {C}artesian Closed Categories", Journal=jsl, Volume=62, Year=1997, Pages="636--647") @InProceedings(Narendran93, Author="P. Narendran and F. Pfenning and R. Statman", Title="On the Unification Problem for {C}artesian Closed Categories", Crossref="lics8", Pages="57--63") @misc(Narendran92, Author="P. Narendran and F. Pfenning and R. Statman", Title="On the Unification Problem for {CCC}'s", Year=1992, Note="unpublished") @book(Nilsson80, author="Nils J. Nilsson", title="Principles of Artificial Intelligence", publisher="Tioga Publishing Company", year=1980) @InCollection{Nipkow98, author = {Tobias Nipkow and Christian Prehofer}, title = {Higher-Order Rewriting and Equational Reasoning}, crossref = {Bibel98a}, volume = 1, pages = {399--430} } @Article{Nipkow95, author = "Tobias Nipkow", title = "Higher-Order Rewrite Systems", journal = "Lecture Notes in Computer Science", volume = "914", pages = "256", year = "1995", coden = "LNCSD9", ISSN = "0302-9743", } %one page abstract for invited address %Rewriting techniques and applications : 6th International Conference, %RTA-95, Kaiserslautern, Germany, April 5-7, 1995 : proceedings / Jieh %Hsiang, ed. %005.131 R454 @Article(NipkowQian94, Author="Tobias Nipkow and Zhenyu Qian", Title="Reduction and Unification in Lambda Calculi with a General Notion of Subtype", Journal=jar, Year=1994, Pages="389--406", Volume=12) @InProceedings(Nipkow93, Author="Tobias Nipkow", Title="Functional Unification of Higher-Order Patterns", Crossref="lics8") @InProceedings(Nipkow92, Author="Tobias Nipkow and Zhenyu Qian", Title="Reduction and Unification in Lambda Calculi with Subtypes", Crossref="cade11", Pages="66--78") @InProceedings(Nipkow91, Author="Tobias Nipkow and Zhenyu Qian", Title="Modular Higher-Order {$E$}-Unification", Booktitle=proc # "4th International Conference on Rewriting Techniques and Applications", Editor="Ronald V. Book", Series=lncs, Volume=488, Publisher=sv, Year=1991, Pages="200--214") @INPROCEEDINGS{Ohlbach96, AUTHOR = {Ohlbach, H. J.}, YEAR = {1996}, TITLE = {{\sc SCAN}---Elimination of Predicate Quantifiers}, EDITOR = {McRobbie, M. A. and Slaney, J. K.}, BOOKTITLE = {Automated Deduction: CADE-13}, SERIES = {Lecture Notes in Artificial Intelligence}, VOLUME = {1104}, PUBLISHER = {Springer}, PAGES = {161--165}, } @InCollection(Ohlbach90, Author="Hans Jurgen Ohlbach and J{\"{o}}rg H. Siekmann", Title="The {M}arkgraf {K}arl Refutation Procedure", Editor="J. L. Lassez", BookTitle="Festschrift of A. Robinson's 60th Birthday", Publisher="Oxford University Press", Year=1990, Pages="(to appear)") @Phdthesis(OHLBACH88a, author="Hans Jurgen Ohlbach", title="A Resolution Calculus for Modal Logics", school="Department of Computer Science, University of Kaiserslautern", year=1988) @TechReport(Ohlbach88, Author="H. J. Ohlbach and J. Siekmann", Title="Using Automated Reasoning Techniques for Deductive Databases", Type="SEKI Report", Number="SR--88--06", Institution="Fachbereich Informatik, University of Kaiserslautern", Year=1988) @TechReport(Ohlbach82, Author="H. J. Ohlbach", Title="The Logic Engine", Institution="MEMO-SEKI--82-II, FB Informatik, University of Karsruhe", Year=1982) @InProceedings(Owre96, Author="S. Owre and S. Rajan and J.M. Rushby and N. Shankar and M. Srivas", Title="{PVS}: Combining Specification, Proof Checking, and Model Checking", Booktitle="Computer-Aided Verification, CAV'96", Editor="Rajeev Alur and Thomas A. Henzinger", Series=lncs, Volume=1102, Publisher=sv, Year=1996, Pages="411--414") @Article(Padovani00, Author="Vincent Padovani", Title="Decidability of Fourth Order Matching", Journal=mscs, Volume=10, Year=2000, Pages="361--372") @Article(Pastre78, Author="D. Pastre", Title="Automatic Theorem Proving in Set Theory", Journal=ai, Volume=10, Year=1978, Pages="1--27") @Article(PatersonWegman78, author="Paterson, M.S. and Wegman, M.N.", title="Linear Unification", journal=jcss, volume=16, pages="158--167", year=1978) @Article(PaulsonGrabczewski96, author="Lawrence Paulson and Krzystztof Grabczewski", title="Mechanising Set Theory: Cardinal Arithmetic and the Axiom of Choice", journal=jar, volume=17, pages="291--323", year=1996) @Article{Paulson97jlc, author = "Lawrence C. Paulson", title = "Mechanizing Coinduction and Corecursion in Higher-Order Logic", journal = "Journal of Logic and Computation", year = 1997, volume = 7, number = 2, pages = "175--204", month = mar, keywords = "Isabelle" } @misc(Paulson96, Author="Lawrence C. Paulson", Title="A Simple Mechanical Proof for the Mutilated Chess Board", Year=1996, Note="available from http://www.cl.cam.ac.uk/users/lcp/papers/mutil.dvi.gz") @Article(Paulson95, Author="Lawrence C. Paulson", Title="Set Theory for Verification: {II}. Induction and Recursion", Journal=jar, Year=1995, Pages="167--215", Volume=15, Number=2) @book{Paulson94, author = "Lawrence C. Paulson" , title = "Isabelle: A Generic Theorem Prover", publisher= "Springer Verlag", series = lncs, volume = "828", year = "1994"} @InProceedings{Paulson94cade, author = "Lawrence C. Paulson", title = "A Fixedpoint Approach to Implementing (Co)Inductive Definitions", editor = "Alan Bundy", booktitle = "Proceedings of the 12th International Conference on Automated Deduction", address = "Nancy, France", month = jun, year = 1994, publisher = "Springer-Verlag LNAI 814", pages = "148--161", urldvi = "http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz", keywords = "Isabelle" } @Article(Paulson93, Author="Lawrence C. Paulson", Title="Set Theory for Verification: {I}. From Foundations to Functions", Journal=jar, Year=1993, Pages="353--389", Volume=11) @Article(Paulson89, Title="The Foundation of a Generic Theorem Prover", Author="Lawrence C. Paulson", Journal=jar, Year=1989, Pages="363--397", Volume=5) @Book(Paulson87, Author="L. C. Paulson", Title="Logic and Computation. Interactive Proof with Cambridge {LCF}", Publisher="Cambridge University Press", Year=1987) @Article(Petermann92, Title="How to Build in an Open Theory into Connection Calculi", Author="Uwe Peterman", Journal="Computers and Artificial Intelligence", Year=1992, Pages="105--142", Volume=11) @InProceedings(Pfenning99, author="Frank Pfenning and Carsten Sch{\"{u}}rmann", title="System Description: Twelf--A Meta-Logical Framework for Deductive Systems", crossref="cade16", Pages="202--206") @InProceedings{Pfenning98types, author = "Frank Pfenning and Carsten Sch{\"u}rmann", title = "Algorithms for Equality and Unification in the Presence of Notational Definitions", editor = "T. Altenkirch and W. Naraschewski and B. Reus", booktitle = "Types for Proofs and Programs", month = mar, year = 1998, pages = "179--193", address = "Kloster Irsee, Germany", publisher = "Springer-Verlag LNCS 1657", keywords = "LF, Elf", urlpdf = "http://www.cs.cmu.edu/~fp/papers/types98.pdf", urlps = "http://www.cs.cmu.edu/~fp/papers/types98.ps" } @InProceedings(Pfenning90, Author="Frank Pfenning and Dan Nesmith", Title="Presenting Intuitive Deductions via Symmetric Simplification", Crossref="cade10", Pages="336--350") @PhdThesis(Pfenning86, Author="Frank Pfenning", Title="Proof Transformations in Higher-Order Logic", School=cmu, Year=1987, Note="156 pp.") @InProceedings(Pfenning84, Author="Frank Pfenning", Title="Analytic and Non-Analytic Proofs", Crossref="cade7", Pages="394--413") @InProceedings(Pierce90, Author="William Pierce", Title="Toward Mechanical Methods for Streamlining Proofs", Crossref="cade10", Pages="351--365") @Article(Pietrzykowski72, Author="Tomasz Pietrzykowski", Title="A Complete Mechanization of Second-Order Type Theory", Journal=jacm, Volume=20, Year=1973, Pages="333--364") @InProceedings(PietrzykowskiJensen72, Author="T. Pietrzykowski and D. C. Jensen", Title="A Complete Mechanization of ($\omega$)-Order Type Theory", BookTitle=proc # "ACM Annual Conference, Volume I", Publisher="ACM", Year=1972, Pages="82--92") @InProceedings(Plaisted80, Author="D.A. Plaisted", Title="Abstraction Mappings in Mechanical Theorem Proving", Crossref="cade5", Pages="264--280") @Article(Plaisted81, Author="D.A. Plaisted", Title="Theorem Proving with Abstraction", Journal=ai, Volume=16, Year=1981, Pages="47--108") @PhdThesis(Plummer87, Author="Dave Plummer", Title="Gazing: Controlling the Use of Rewrite Rules", School="Dept.\ of Artificial Intelligence, University of Edinburgh", Year=1987) @InProceedings(Prawitz71, Author="Dag Prawitz", Title="Ideas and Results in Proof Theory", Editor="J. E. Fenstad", Series="Studies in Logic and the Foundations of Mathematics 63", Publisher="North-Holland", Booktitle=proc # "Second Scandinavian Logic Symposium", Year=1971, Pages="235--307") @InProceedings(Prawitz70, Author="Dag Prawitz", Title="A Proof Procedure with Matrix Reduction", Editor="M. Laudet and D. Lacombe and L. Nolin and M. Schutzenberger", Series="Lecture Notes in Mathematics 125", Publisher=sv, Booktitle="Symposium on Automatic Demonstration, Versailles, France", Year=1970, Pages="207--214") @InCollection(Prawitz69, Author="Dag Prawitz", Title="Advances and Problems in Mechanical Proof Procedures", Editor="Meltzer and Michie", BookTitle="Machine Intelligence 4", Publisher="Edinburgh University Press", Year=1969, Pages="59--71") @Article(Prawitz68, Tag="Prawitz68", Author="Dag Prawitz", Title="Hauptsatz for Higher Order Logic", Journal=jsl, Volume=33, Year=1968, Pages="452--457") @Book(Prawitz65, Author="Dag Prawitz", Title="Natural Deduction", Publisher="Almqvist \& Wiksell", Year=1965) @Article(Prawitz60, Author="Dag Prawitz", Title="An improved proof procedure", Journal="Theoria", Volume=26, Year=1960, Pages="102--139") @Book(Prehofer97, Author="Christian Prehofer", Title="Solving Higher-Order Equations: From Logic to Programming", Publisher="Birkh{\"{a}}user Boston", Year=1997) @InProceedings(Prehofer94, Author="Christian Prehofer", Title="Decidable Higher-Order Unification Problems", Crossref="cade12", Pages="635--649") @inproceedings(Presburger30, author="Moj{\.{z}}esz Presburger", title="{\"{U}}ber die Vollst{\"{a}}ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt", booktitle="Sprawozdanie z I Kongresu metematyk{\'{o}}w slowia{\'{n}}skich, Warszawa 1929", pages="92-101,395", address="Warsaw, Poland", year=1930, note="Annotated English version in \cite{Stansifer84}.") @Misc(ProofPower, Key="ProofPower", Title="ProofPower", Year=2000, Note="http://www.lemma-one.com/ProofPower/doc/doc.html") @Misc(PVS, Key="PVS", Title="{PVS} {S}pecification and {V}erification {S}ystem", year=1996, Note="http://pvs.csl.sri.com/") @article(Quaife92, title="Automated Deduction in von {N}eumann-{B}ernays-{G\"{o}}del Set Theory", author="Art Quaife", journal=jar, year=1992, pages="91--147", volume=8) @article(Quaife90, title="Andrews' Challenge Problem Revisited", author="Art Quaife", journal=aarn, month=may, year=1990, pages="3--7", volume=15) @Misc(QED, Key="QED", Title="The QED Project", Note="http://www-unix.mcs.anl.gov/qed/index.html") @Article{Qian96, author = "Zhenyu Qian and Kang Wang", title = "Modular Higher-Order Equational Preunification", journal = jsc, volume = "22", number = "4", pages = "401--424", year = "1996"} @Inproceedings(Qian92, Author="Zhenyu Qian and K. Wang", Title="Higher Order {$E$}-Unification for Arbitrary Theories", Booktitle="Proc.\ Joint International Conference and Symposium on Logic Programming", Publisher="MIT Press", Year=1992, Pages="52--66") @unpublished(Quigley98, Author="Claire Quigley", Title="An Alternative Approach to Matingsearch", Note="(Unpublished). Computing Science Department, Glasgow University", Month=dec, Year=1998) @Book(Quine63, Author="Willard Van Orman Quine", Title="Set Theory and Its Logic", Publisher="Belknap Press of Harvard University Press", Year=1963) @Article(Quine55, Author="W. V. Quine", Title="A Proof Procedure for Quantification Theory", Journal=jsl, Volume=20, Year=1955, Pages="141--149") @Article(Quine50, Author="W. V. Quine", Title="On Natural Deduction", Journal=jsl, Volume=15, Year=1950, Pages="93--102") @Article(Quine37, Author="W. V. Quine", Title="Logic Based on Inclusion and Abstraction", Journal=jsl, Volume=2, Year=1937, Pages="145--152") @InProceedings(Raamsdonk99, author="Femke van Raamsdonk", title="Higher-Order Rewriting", Crossref="rta99", pages="221--239") @Article(Ramesh97, author="Anavai Ramesh and Neil V. Murray and Bernhard Beckert and Reiner H{\"{a}}hnle", title="Fast Subsumption Checks Using Anti-Links", Journal=jar, Volume=18, Year=1997, Pages="47--83") @techreport(Ramesh95, author="Anavai Ramesh and Neil V. Murray and Bernhard Beckert and Reiner H{\"{a}}hnle", title="Fast Subsumption Checks Using Anti-Links", institution="Universit{\"{a}}t Karlsruhe, Fakult{\"{a}}t f{\"{u}}r Informatik", type="Interner Bericht", number="24/95", month=apr, year=1995) @TechReport(Raph84, Author="Karl Mark G. Raph", Title="The {M}arkgraph {K}arl Refutation Procedure", Institution="Interner Bericht, Memo-SEKI-MK--84-01, Fachbereich Informatik, Universit{\"{a}}t Kaiserlautern", Year=1984) @Article(Rasiowa49, Author="H. Rasiowa", Title="Sur un certain syst\`{e}m d'axiomes du calcul des propositions", Journal="Norsk matematisk Tidsskrift", Volume="31", Year="1949", Pages="1-3") @Techreport(Reed2002, Author="Jason Reed", Title="Proof Irrelevance and Strict Definitions in a Logical Framework", Institution="School of Computer Science, Carnegie Mellon University", Number="02-153", Year=2002) @incollection{Reynolds90, AUTHOR = "J. C. Reynolds", TITLE = "Polymorphic Lambda-Calculus: Introduction", YEAR = 1990, BOOKTITLE = "Logical Foundations of Functional Programming", EDITOR = "G. Huet", PUBLISHER = "Addison-Wesley", ADDRESS = "Reading, MA", PAGES = "77-86"} @InProceedings(Richardson98, author="Julian Richardson and Alan Smaill and Ian Green", title="System Description: Proof Planning in Higher-Order Logic with $\lambda-{C}lam$", Crossref="cade15", pages="129--133") @InCollection(Robinson91, Author="J. A. Robinson", Title="Formal and Informal Proofs", Editor="R.S. Boyer", BookTitle="Automated Reasoning: Essays in Honor of Woody Bledsoe", Publisher="Kluwer Academic Publishers", Year=1991, Pages="267--281") @Book(Robinson79, Author="J. A. Robinson", Title="Logic: Form and Function", Publisher="Elsevier North-Holland Inc.", Year=1979, Address="New York") @InCollection(Robinson70, Author="J. A. Robinson", Title="A Note on Mechanizing Higher Order Logic", BookTitle="Machine Intelligence 5", Publisher="Edinburgh University Press", Year=1970, Pages="121--135") @InCollection(Robinson69, Author="J. A. Robinson", Title="Mechanizing Higher-Order Logic", BookTitle="Machine Intelligence 4", Publisher="Edinburgh University Press", Year=1969, Pages="151--170") @Article(Robinson69b, Author="Arthur Robinson and Larry Wos", Title="Paramodulation and {TP} in First Order Theories with Equality", Journal="Machine Intelligence", Volume=4, Year=1969, Pages="135--150") @InProceedings(Robinson68, Author="J. A. Robinson", Title="New Directions in Mechanical Theorem Proving", Booktitle=proc # "IFIP Congress", Year=1968, Pages="206--210") @Article(Robinson65, Author="J. A. Robinson", Title="A Machine-Oriented Logic Based on the Resolution Principle", Journal=jacm, Volume=12, Year=1965, Pages="23--41") @Book(Rogers87, Author="Hartley Rogers, Jr.", Title="Theory of Recursive Functions and Effective Computabiblity", Publisher="MIT Press", Year=1987, Address="Massachusetts") @Book(Rosser53, Author="J. Barkley Rosser", Title="Logic for Mathematicians", Publisher="McGraw-Hill", Year=1953) @Article(Rosser36, Author="J. B. Rosser", Title="Extensions of some Theorems of {G\"{o}}del and {C}hurch", Journal=jsl, Year=1936, Volume=1, Pages="87--91") @Book(Rubin1985, Author=" Herman Rubin and Jean E. Rubin", Title="Equivalents of the Axiom of Choice, {II}", Publisher="North-Holland", Year=1985) @article{Rushby98, AUTHOR = {John Rushby and Sam Owre and {N.} Shankar}, TITLE = {Subtypes for Specifications: Predicate Subtyping in {PVS}}, JOURNAL = {{IEEE} Transactions on Software Engineering}, VOLUME = {24}, NUMBER = {9}, YEAR = {1998}, PAGES = {709--720}, MONTH = {sep}, URL = {http://www.csl.sri.com/papers/tse98/} } @Book(Russell1903, Author="Bertrand Russell", Title="The Principles of Mathematics", Publisher="Cambridge University Press", Year=1903) @Article(Russell08, Author="Bertrand Russell", Title="Mathematical Logic as Based on the Theory of Types", Journal="American Journal of Mathematics", Volume=30, Year=1908, Pages="222--262", Note="Reprinted in \cite[pp. 150--182]{Heijenoort67}") @article(SaksStatman88, Author="M. Saks and R. Statman", Title="An Intersection Problem for Finite Automata", Journal="Discrete Applied Mathematics", Volume=21, Year=1988, Pages="245--255") @InProceedings{Schmitt2001, author = "Stephan Schmitt and Lori Lorigo and Christoph Kreitz and Alexey Nogin", title = "{{\sf JProver}}: Integrating Connection-based Theorem Proving into Interactive Proof Assistants", Crossref = "ijcar2001", pages = "421--426", } @InProceedings(Schmitt2000, Author="Stephan Schmitt", Title="A Tableau-Like Representation Framework for Efficient Proof Reconstruction", Crossref="tableaux00", Pages="398--414") @InProceedings{SchmittKreitz98a, author = "Stephan Schmitt and Christoph Kreitz", title = "Deleting Redundancy in Proof Reconstruction", crossref = "tableaux98", pages = "262--276", } @InProceedings(SchmittKreitz96, Author="Stephan Schmitt and Christoph Kreitz", Title="Converting Non-Classical Matrix proofs into Sequent-Style Systems", Crossref="cade13", Pages="418--432") @InProceedings(SchmittKreitz95, Author="Stephan Schmitt and Christoph Kreitz", Title="On Transforming Intuitionistic Matrix Proofs into Standard-Sequent Proofs", Crossref="tableaux95", Pages="106--121") @Article(Schonfinkel24, Author="M. Sch{\"{o}}nfinkel", Title="{\"{U}}ber die {B}austeine der mathematischen {L}ogik", Journal=ma, Year=1924, Volume=92, note="Translated in \cite[pp. 355--366]{Heijenoort67}", Pages="305--316") @book(Schroder90, author="E. Schr{\"o}der", title="Algebra der {L}ogik", publisher="Teubner-Verlag", year=1890, address="Leipzig") @Book(SchubertWindleyAlves-Foss95, Author="E. T. Schubert and P. J. Windley and J. Alves-Foss, eds.", Title="Higher Order Logic Theorem Proving and Its Applications: 8th International Workshop", address="Aspen Grove, Utah", series=lncs, volume=971, publisher=sv, Year=1995) @InProceedings(Schumann90, Author="J. Schumann and R. Letz", Title="{PARTHEO}: A High-Performance Parallel Theorem Prover", Crossref="cade10", Pages="40--56") @InProceedings(Schumann90b, Author="Johann Schumann", Title="Parallel Theorem Provers: An Overview", Booktitle="Parallelization in Inference Systems: International Workshop Proceedings", Editor="B. Fronh{\"{o}}fer and G. Wrightson", Address="Dagstuhl Castle, Germany", Series=lnai, Volume=590, Publisher=sv, Year=1990, Pages="26--50") @Article(Schutte56, Author="Kurt Sch{\"{u}}tte", Title="Ein {S}ystem des {V}erkn{\"{u}}pfenden {S}chliessens", Journal=amlg, Year=1956, Volume=2) @Article(Schutte60, Author="K. Sch{\"{u}}tte", Title="Syntactical and Semantical Properties of Simple Type Theory", Journal=jsl, Year=1960, Volume=25, Number=4, Pages="305--326") @Article(Schutte50, Author="K. Sch{\"{u}}tte", Title="{S}chlussweisen {K}alk{\"{u}}le der {P}r{\"{a}}dikatenlogik", Journal=ma, Year=1950, Volume=122, Pages="47--65") @TechReport(Scott81, Author="Dana Scott", Title="Lectures on a Mathematical Theory of Computation", Institution="Oxford Technical Monograph PRG --- 19", Month=may, Year=1981) @manual(Scribe80, Author="Brian K. Reid and Janet H. Walker", Title="{SCRIBE} Introductory User's Manual", Organization="UNILOGIC, Ltd.", Year=1980, Edition="Third", Address="160 N. Craig St., Pittsburgh, PA 15213") @Misc(SemanticWeb, Key="SemanticWeb", Title="Semantic Web Activity", Note="http://www.w3.org/2001/sw/") @inproceedings(Shankar2001, Author="Natarajan Shankar", Title="Using Decision Procedures with a Higher-Order Logic", Crossref="tphols01", Pages="5--26") @Book(Shapiro91, Author="Stewart Shapiro", Title="Foundations without Foundationalism : A Case for Second-order Logic", Publisher="Clarendon Press", Year=1991, Address="Oxford") @Book(Shin94, Author="Sun-Joo Shin", Title="The Logical Status of Diagrams", Publisher="Cambridge University Press", Year="1994") @Book(Shoenfield67, FullAuthor="Joseph R. Shoenfield", Author="J. R. Shoenfield", Title="Mathematical Logic", Publisher="Addison-Wesley", Year=1967, Address="Reading, Massachusetts") @Article(Shostak76, Author="Robert E. Shostak", Title="Refutation Graphs", Journal=ai, Volume=7, Year=1976, Pages="51--64") @Article(Sickel76, Author="Sharon Sickel", Title="A Search Technique for Clause Interconnectivity Graphs", Journal=ieeet, Volume="C--25", Year=1976, Pages="823--835") @Article(Siefkes, Author="Dirk Siefkes", Title="Undecidable Extensions of Monadic Second-Order Successor Arithemtic", Journal=zml, Year=1971, Volume=17, Pages="385--394", note="references Buchi, not Behmann") @Article(Sieg97, Author="Wilfried Sieg", Title="Step by recursive step: Church's analysis of effective calculabilty", Journal=bsl, Volume="3", Year="1997", Pages="154--180") @Article{Siekmann2006J12, author = {J{\"o}rg Siekmann and Christoph Benzm{\"u}ller and Serge Autexier}, title = {Computer Supported Mathematics with OMEGA}, journal = {Journal of Applied Logic}, volume = {4}, number = {4}, pages = {533-559}, year = 2006, } @InProceedings{Siekmann2004, author = {J. Siekmann and C. Benzm{\"u}ller}, editor = {S. Biundo, T. Frühwirth, G. Palm}, title = {OMEGA: Computer Supported Mathematics}, booktitle = {KI 2004: Advances in Artificial Intelligence: 27th Annual German Conference on AI}, number = 3228, pages = {3--28}, series = {lnai}, year = 2004, address = {Ulm, Germany} } @InCollection{Siekmann2003, author = {J{\"o}rg Siekmann and Christoph Benzm{\"u}ller and Armin Fiedler and Andreas Meier and Immanuel Normann and Martin Pollet}, editor = {Fairouz Kamareddine}, booktitle = {Thirty Five Years of Automating Mathematics}, title = {Proof Development in {OMEGA}: The Irrationality of Square Root of 2}, publisher = {Kluwer Academic Publishers}, year = 2003, pages = {271-314}, series = {Kluwer Applied Logic series (28)}, note = {ISBN 1-4020-1656-5} } @InProceedings{Siekmann2002, author = {J{\"o}rg Siekmann and Christoph Benzm{\"u}ller and Vladimir Brezhnev and Lassaad Cheikhrouhou and Armin Fiedler and Andreas Franke and Helmut Horacek and Michael Kohlhase and Andreas Meier and Erica Melis and Markus Moschner and Immanuel Normann and Martin Pollet and Volker Sorge and Carsten Ullrich and Claus-Peter Wirth and J{\"u}rgen Zimmer}, title = {Proof Development with ${\Omega}$mega}, Crossref= {cade18}, pages = {144--149}, url = {www.ags.uni-sb.de/$\,\sim$chris/papers/C11.pdf} } % url = {www.ags.uni-sb.de/~chris/papers/C11.pdf} % the tilde in the url above doesn't print without some kind of hack @Article{Siekmann99, author = {J{\"o}rg Siekmann and Stephan Hess and Christoph Benzm{\"u}ller and Lassaad Cheikhrouhou and Armin Fiedler and Helmut Horacek and Michael Kohlhase and Karsten Konrad and Andreas Meier and Erica Melis and Martin Pollet and Volker Sorge}, title = {{LOUI}: Lovely {OMEGA} User Interface}, journal = {Formal Aspects of Computing}, year = 1999, volume = 11, pages = {326--342}, url = {www.ags.uni-sb.de/~chris/papers/J2.pdf}, } @Article(Siekmann89, Author="J{\"{o}}rg Siekmann", Title="Unification Theory", Journal=jsc, Volume=7, Year=1989, Pages="207--274") @InProceedings(Siekmann84, Author="J{\"{o}}rg Siekmann", Title="Universal Unification", Crossref="cade7", Pages="1--42") @Book(SiekmannWrightson83b, Editor="J{\"{o}}rg Siekmann and Graham Wrightson", Title="Automation of Reasoning. Vol.\ 2. Classical Papers on Computational Logic 1967--1970", Publisher=sv, Year=1983) @Book(SiekmannWrightson83a, Editor="J{\"{o}}rg Siekmann and Graham Wrightson", Title="Automation of Reasoning. Vol.\ 1. Classical Papers on Computational Logic 1957--1966", Publisher=sv, Year=1983) @InProceedings(Simon88, Author="Donald Simon", Title="Checking Natural Language Proofs", Crossref="cade9", Pages="141--150") @Article(Skolem28, Author="Thoralf Skolem", Title="{\"U}ber die Mathematische {L}ogik", Journal="Norse matematisk tidsskrift", Year=1928, Volume=10, Pages="125--142", Note="Translated in \cite[pp.\ 508--524]{Heijenoort67}") @Article(Skolem20, Author="Thoralf Skolem", Title="{L}ogisch-kombinatorische {U}ntersuchungen {\"{u}}ber die erf{\"{u}}llbarkeit oder beweisbarkeit mathematischer {S\"{a}}tze nebst einem {T}heoreme {\"{u}}ber dichte {M}engen", Journal="Skr.\ av Videnkapsselskapet i Kristiana, I.\ Matem.-natur klasse", Year=1920, Volume=4) @Article(Slagle74, Author="J.R. Slagle", Title="Automated Theorem-Proving for Theories with Simplifiers, Commutativity and Associativity", Journal=jacm, Year=1974) @Book(Smullyan95, author={Raymond M. Smullyan}, title={First-Order Logic}, publisher={Dover Publications, New York}, edition={Second corrected}, year={1995}, note={First published in 1968 by } # sv) @Book(Smullyan85, Author="Raymond Smullyan", Title="To Mock a Mockingbird", Publisher="Alfred A. Knopf", Year=1985, Address="New York") @Article(Smullyan68a, Author="Raymond M. Smullyan", Title="Uniform {G}entzen Systems", Journal=jsl, Year=1968, Volume=33, Pages="549--559") @Article(Smullyan68b, Author="Raymond M. Smullyan", Title="Analytic Cut", Journal=jsl, Year=1968, Volume=33, Pages="560--564") @Book(Smullyan68, FullAuthor="Raymond M. Smullyan", Author="R. M. Smullyan", Title="First-Order Logic", Publisher=sv, Year=1968, Address="Berlin") @Article(Smullyan63, Author="Raymond M. Smullyan", Title="A Unifying Principle in Quantification Theory", Journal=proc # "National Academy of Sciences, U.S.A.", Volume=49, Year=1963, Pages="828--832") @Book(Snyder91, Author="Wayne Snyder", Title="A Proof Theory for General Unification", Publisher="Birkh{\"{a}}user Boston", Year=1991) @InProceedings(Snyder90, Author="Wayne Snyder", Title="Higher-Order {$E$}-Unification", Crossref="cade10", Pages="573--587") @Article(Snyder89, Author="Wayne Snyder and Jean Gallier", Title="Higher-Order Unification Revisited: Complete Sets of Transformations", Journal=jsc, Volume=8, Year=1989, Pages="101--140") @techreport(Stansifer84, author="R. Stansifer", title="Presburger's Article on Integer Arithmetic: Remarks and Translation", institution="Cornell University Computer Science Department", number="TR84--639", year=1984) @misc(Statman95a, Author="R. Statman", Title="The Matching Problem for Simply Typed Lambda Calculus with Surjective Pairing", Year=1994) @Techreport(Statman94b, Author="R. Statman", Title="On the Existence of $n$ but not $n+1$ Easy Combinators", Institution=mathcmu, Number="94--165", Year=1994) @Techreport(Statman94a, Author="R. Statman", Title="Recursive Types and the Subject Reduction Theorem", Institution=mathcmu, Number="94--164", Year=1994) @InCollection(Statman93a, Author="Rick Statman", Title="Some Examples of Non-Existent Combinators", Editor="M. Dezani-Ciancaglini and S. Ronchi Della Rocca and M. Venturini Zilli", BookTitle="A Collection of Contributions in Honour of Corrado Bohm on the Occasion of his 70th Birthday", Publisher="Elsevier", Year=1993, Pages="441--448", Note="(Reprinted from " # tcs # " 121 (1993))") @Techreport(Statman92d, Author="Rick Statman", Title="An Embedding of Untyped $\lambda$-Calculus into Simply Typed $\lambda$-Calculus", Institution=mathcmu, Number="92--147", Year=1992) @Techreport(Statman92c, Author="Rick Statman", Title="Simply Typed $\lambda$ Calculus with Surjective Pairing", Institution=mathcmu, Number="92--146", Year=1992) @Article(Statman92b, Author="R. Statman", Title="The {V}isser Fixed Point Theorem", Journal="Journal of Functional Programming", Year=1992, Volume=2, Pages="233--236", Note="(in Enumerators of lambda terms are reducing by Henk Barendregt)") @misc(Statman92a, Author="R. Statman", Title="Some Results about {S}-terms", Year=1991, Note="unpublished") @InProceedings(Statman92, Author="R. Statman and U. Deliquoro and A. Piperno", Title="Retracts in the Simply Typed $\lambda\beta\eta$-Calculus", Crossref="lics7", Pages="461--469") @Techreport(Statman91a, Author="R. Statman", Title="There is no Hyperrecurrent {S}, {K} Combinator", Institution=mathcmu, Number="91--133", Year=1991) @Techreport(Statman91, Author="R. Statman", Title="A Local Translation of Untyped $\lambda$-Calculus into Simply Typed $\lambda$-Calculus", Institution=mathcmu, Number="91--134", Year=1991) @misc(Statman90b, Author="R. Statman", Title="Taming the Wild Ant-Lion", Year=1990, Note="unpublished") @InProceedings(Statman90a, Author="Rick Statman", Title="{F}reyd's Hierarchy of Combinator Monoids", Crossref="lics6", Pages="186--190") @misc(Statman89g, Author="R. Statman", Title="Marginalia to a Proof of {M}itchke's", Year=1989, Note="unpublished") @misc(Statman89f, Author="R. Statman", Title="Solution to a Problem of {B}arendregt", Year=1989, Note="unpublished") @Misc(Statman89e, Author="R. Statman", Title="Two Recursion-Theoretic Problems in $\lambda$-Calculus", Year=1989, Note="unpublished") @Techreport(Statman89d, Author="R. Statman", Title="Normal Varieties of Combinators", Institution=mathcmu, Number="89--61", Month=oct, Year=1989) @Article(Statman89c, Author="R. Statman", Title="The Word Problem for {S}mullyan's Lark Combinator is Decidable", Journal=jsc, Volume=7, Year=1989, Pages="103--112") @Article(Statman89b, Author="R. Statman", Title="On Sets of Solutions to Combinator Equations", Journal=tcs, Volume=66, Year=1989, Pages="(99--104)") @Misc(Statman89a, Author="R. Statman", Title="Some Properties of Linear Combinators", Note="in preparation") @Techreport(Statman88c, Author="R. Statman", Title="Combinators Hereditarily of Order Two", Institution=mathcmu, Number="88--33", Year=1988) @Techreport(Statman88b, Author="R. Statman", Title="Combinators Hereditarily of Order One", Institution=mathcmu, Number="88--32", Year=1988) @Techreport(Statman88a, Author="R. Statman", Title="Combinators and the Theory of Partitions", Institution=mathcmu, Number="88--31", Year=1988) @inproceedings(Statman87a, Author="R. Statman", Title="Empty Types in Polymorphic $\lambda$-Calculus", Booktitle="ACM Symposium on Principles of Programming Languages", Year=1987, Pages="253--262") @InProceedings(Statman87, Author="R. Statman", Title="A Model of {S}cott's Theory {LCF}", Series="Contemporary Mathematics series", Publisher=ams, Volume=106, Year=1987, Pages="263--280") @Article(Statman86g, Author="Ana Pasztor and Rick Statman", Title="{S}cott Induction and Closure Under $\omega$-Sups", Journal=tcs, Year=1986, Volume=43, Pages="251--263") @Article(Statman86f, Author="R. Statman", Title="Solving Functional Equations at Higher Types", Journal=ndjfl, Volume=27, Year=1986, Pages="66--74") @Misc(Statman86e, Author="R. Statman", Title="Real and Imaginary Terms in Polymorphic $\lambda$-Calculus", Year=1986, Note="unpublished.") @Misc(Statman86d, Author="R. Statman", Title="Combinator Word Problems", Year=1986, Note="course lecture notes in 1990") @Techreport(Statman85e, Author="R. Statman", Title="Three Notes on Combinatory Algebra", Institution=mathcmu, Number="85--5", Year=1985) @Techreport(Statman85d, Author="R. Statman", Title="Two Exercises in Combinatory Algebra", Institution=mathcmu, Number="85--6", Year=1985) @Article(Statman86c, Author="R. Statman", Title="Every Countable Poset is Embeddedable in the Poset of Unsolvable Terms", Journal=tcs, Volume=48, Year=1986, Pages="95--100") @InProceedings(Statman86b, Author="R. Statman", Title="On Translating $\lambda$-Terms into Combinators", Crossref="lics1", Pages="378--383") @Misc(Statman85c, Author="R. Statman", Title="Lectures on Typed $\lambda$-Calculus", Year=1985, Note="unpublished lecture notes.") @InProceedings(Statman85b, Author="R. Statman", Title="Equality Between Functionals Revisited", BookTitle="Harvey Friedman's Research on the Foundations of Mathematics", Editor="L. Harrington and M. Morley and S. Simpson", Publisher="North Holland", Year=1985, Pages="331--338") @article(Statman85a, Author="R. Statman", Title="Logical Relations and the Typed $\lambda$-Calculus", Journal="Information and Control", Pages="85--97", Volume=65, Year=1985) @misc(Statman85, Author="R. Statman", Title="A Theory of Higher Type Functional Equations: Text of Talk to the {B}oston Logic Colloquium", Year=1985) @Misc(Statman83, Author="R. Statman", Title="Embeddings, Homomorphisms and $\lambda$-Definability", Year=1983, Note="unpublished") @article(Statman82a, Author="R. Statman", Title="$\lambda$-Definable Functionals and $\beta\eta$-Conversion", Journal=amlg, volume=22, Year=1982, Pages="1--6") @article(Statman82, Author="R. Statman", Title="Completeness, Invariance and $\lambda$-Definability", Journal=jsl, Volume=47, Year=1982, Pages="17--26") @inproceedings(Statman81d, Author="R. Statman", Title="Number Theoretic Functions Computable by Polymorphic Programs", Booktitle="22nd Annual Symposium on Foundations of Computer Science", Publisher="Computer Society Press", Year=1981, Pages="279--282") @misc(Statman81c, Author="R. Statman", Title="On the Existence of Closed Terms in the Typed $\lambda$-Calculus {III}", Year=1981, Note="unpublished") @article(Statman81b, Author="R. Statman", Title="On the Existence of Closed Terms in the Typed $\lambda$-Calculus {II}", Journal=tcs, Volume=15, Year=1981, Pages="329--338") @InCollection(Statman80, Author="Richard Statman", Title="On the Existence of Closed Terms in the Typed $\lambda$-Calculus {I}", Editor="J. P. Seldin and J. R. Hindley", BookTitle="To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism", Publisher="Academic Press", Pages="511--534", Year=1980) @Article(Statman79a, Author="R. Statman", Title="Intuitionistic Propositional Logic is Polynomial Space Complete", Journal=tcs, volume=1, Year=1979, Pages="67--72") @Article(Statman79, Author="R. Statman", Title="The Typed $\lambda$-Calculus is not Elementary Recursive", Journal=tcs, Volume=9, Year=1979, Pages="73--81") @Article(Statman78, Author="Richard Statman", Title="Bounds for Proof Search and Speed-up in the Predicate Calculus", Journal="Annals of Mathematical Logic", Volume=15, Year=1978, Pages="225--287") @Book(Stenlund72, Author="Soren Stenlund", Title="Combinators, $\lambda$-terms and Proof Theory", publisher="D. Reidel", address="Dordrecht", Year=1972) @Article(Stickel85, Author="Mark E. Stickel", Title="Automated Deduction by Theory Resolution", Journal=jar, Volume=1, Year=1985, Pages="333-355") @Article(Subramanian95, Author="Sakthi Subramanian", Title="An Interactive Solution to the $n\times n$ Mutilated Checkerboard Problem", Journal="Journal of Logic and Computation", Year="to appear") @Book(Suppes81, Author="Patrick Suppes", Title="University-Level Computer-Assisted Instruction at {S}tanford", Publisher="Leland Stanford Junior University", Year=1981, Note="Part I") @Book(Suppes60, Author="Patrick Suppes", Title="Axiomatic Set Theory", Publisher="D. Van Nostrand Company, Inc.", Year=1960, Address="Princeton, N.J.") @InProceedings(Sutcliffe94, Author="Geoff Sutcliffe and Christian Suttner and Theodor Yemenis", Title="The {TPTP} Problem Library", Crossref="cade12", Pages="252--266") @Book(Szasz63, Author="Gabor Sz{\'a}sz", Title="Introduction to Lattice Theory", Publisher="Academic Press", Address="New York and London", Year=1963) @Article(Tait66, author = {W. W. Tait}, title = {A nonconstructive proof of {G}entzen's {H}auptsatz for second order predicate logic}, journal = {Bulletin of the AMS}, year = {1966}, volume = {72}, number = {6}, pages = {980--983} ) @Article(Takahashi70, Author="{Moto-o} Takahashi", Title="A System of Simple Type Theory of {G}entzen Style with Inference on Extensionality, and the Cut Elimination in it", Journal="Commentarii Mathematici Universitatis Sancti Pauli", Volume=18, Year=1970, Pages="129--147") @comment{the paper below seems not to exist @article(Takahashi68, author="{Moto-o} Takahashi", journal="Journal of the Mathematical Society of Japan", title="Cut-Elimination in Simple Type Theory with Extensionality", volume=19, year=1968) } @Article(Takahashi67, Author="{Moto-o} Takahashi", Title="A Proof of Cut-Elimination Theorem in Simple Type Theory", Journal="Journal of the Mathematical Society of Japan", Volume=19, Year=1967, Pages="399--410") @Book(Takeuti87, Author="Gaisi Takeuti", Title="Proof Theory", Publisher="Elsevier Science Publishers", Year=1987) @Article(Takeuti58, Author="Gaisi Takeuti", Title="Remark on the fundamental conjecture of GLC", Journal="Journal of the Mathematical Society of Japan", Volume=10, Year=1958, Pages="44--45") @Article(Takeuti53, Author="Gaisi Takeuti", Title="On a Generalized Logic Calculus", Journal="Japanese Journal of Mathematics", Volume=23, Year=1953, Pages="39--96", note="Errata: ibid, vol.\ 24 (1954), 149--156") @InCollection(Tarski56, FullAuthor="Alfred Tarski", Author="A. Tarski", Title="The Concept of Truth in Formalized Languages", BookTitle="Logic, Semantics, Metamathematics", Publisher="Oxford University Press", Year=1956, Address="Oxford", Editor="J. H. Woodger", Pages="152--278") @Book(Tarski56a, Author="Alfred Tarski", Title="Logic, Semantics, Metamathematics", Publisher="Oxford University Press", Year=1956, Address="Oxford", Editor="J. H. Woodger") @book(Tarski51, 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") @Article(Tarski36, Author="Alfred Tarski", Title="Der Wahrheitsbegriff in den formalisierten Sprachen", Journal="Studia Philosophica", Volume="1", Year="1936", Note="translated in \cite{Tarski56a}", Pages="261-405") @Article(Tarski23, Author="Alfred Tarski", Title="Sur le terme primitif de la Logistique", Journal=fm, Volume="4", Year="1923", Note="translated in \cite[pp. 1--23]{Tarski56a}", Pages="196--200") @Misc(TPShomepage, Key="TPShomepage", Title="TPS and ETPS Homepage", Note="http://gtps.math.cmu.edu/tps.html") @Misc(TPSnotations, Key="TPSnotations", Title="Notations used by {TPS} and {ETPS}", Note="http://gtps.math.cmu.edu/notations.pdf") @Article(TrybulecSwieczkowska89, Author="Zinaida Trybulec and Halina Swieczkowska", Title="Boolean Properties of Sets", Journal="Journal of Formalized Mathematics", Volume="1", Year="1989", Note="\\Available from http://mizar.org/JFM/Vol1/boole.html", Pages="") @Article(Turing48, Author="A. M. Turing", Title="Practical Forms of Type Theory", Journal=jsl, Year=1948, Volume=13, Pages="80--94") @InProceedings(UribeStickel94, Author="Thomas E. Uribe and Mark E. Stickel", Title="Ordered Binary Decision Diagrams and the {D}avis-{P}utnam Procedure", Booktitle=proc # "First International Conference on Constraints in Computational Logics", Editor="J. P. Jouannaud", Series=lncs, Volume=845, Publisher=sv, Year=1994, Pages="34--49") @InProceedings(Vagin98, Author="V.N. Vagin and N.O. Salapina", Title="Parallel Inference on Connection Graphs", Booktitle=proc # "1998 IEEE International Symposium on Intelligent Control", Publisher=ieeep, address="Gaithersburg, MD, USA", Year=1998, Pages="204--209") @comment{Use Heijenoort67 instead of the reference below} @Book(vanHeijenoort67, Author="Jean van Heijenoort", Title="From {F}rege to {G\"{o}}del. A Source Book in Mathematical Logic 1879--1931", Publisher="Harvard University Press", Year=1967, Address="Cambridge, Massachusetts") @Inproceedings(vanVaalen75, Author="Jophien van Vaalen", Title="An Extension of Unification to Substitutions with an Application to Automatic Theorem Proving", Crossref="ijcai4", Pages="77--82") @InCollection(Visser80, Author="Albert Visser", Title="Numerations, $\lambda$-Calculus and Arithmetic", Editor="J. P. Seldin and J. R. Hindley", BookTitle="To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism", Publisher="Academic Press", Year=1980, Pages="259--284") @Article{Voronkov99, author = "Andrei Voronkov", title = "Simultaneous rigid {E}-unification and other decision problems related to the Herbrand Theorem", journal = tcs, volume = "224", year = "1999", pages="319--352"} @techreport(Voronkov98, author="Andrei Voronkov", title="Simultaneous Rigid {$E$}-Unification and Other Decision Problems Related to the {H}erbrand Theorem", institution="Computing Science Department, Uppsala University, Sweden", year=1998, number="UPMAIL-152") Publication BibTeX @INPROCEEDINGS{Waldinger2003a, AUTHOR={R. Waldinger and P. Jarvis and J. Dungan}, EDITOR={Kornai, A and Sundheim, B}, TITLE={Pointing to Places in a Deductive Geospatial Theory}, BOOKTITLE={Workshop on Analysis of Geographical References; Human Language Technology Conference }, ADDRESS={Edmonton, Canada}, ORGANIZATION={NAACL}, MONTH={May}, YEAR={2003}, ABSTRACT={Issues in the description of places are discussed in the context of a logical geospatial theory. This theory lies at the core of the system GeoLogica, which deduces answers to geographical questions based on knowledge provided by multiple agents. } } @book(Wallen90, Author="Lincoln A. Wallen", Title="Automated Deduction in Nonclassical Logics", Publisher="MIT Press", Year=1990) @mastersThesis(Warren87, Author="K. Warren", Title="Implementation of a Definition Expansion Mechanism in a Connection Method Theorem Prover", School="Dept.\ of Artificial Intelligence, Univ.\ of Edinburgh", Year=1987) @Article(Weaver82, Author="George Weaver and Gumb Raymond", Title="First-Order Properties of Relations with Monotonic Closure Property", Journal=zml, Year=1982, Volume=28, Number=1, Pages="1--5") @incollection(WhiteheadRussell-ch3, Author="Alfred North Whitehead and Bertrand Russell", Title="Incomplete Symbols", Booktitle="Principia Mathematica", Publisher="Cambridge University Press", Year="1927", Edition="2nd", Volume="1", Chapter="III", Pages="66--84", Note="Reprinted in \cite[pp. 216--223]{Heijenoort67}") @Book(Whitehead27, Author="Alfred North Whitehead and B. Russell", Title="Principia Mathematica", Publisher="Cambridge University Press", Year="1927", Edition="2nd", Volume=1) @book(WhiteheadRussell, Author="Alfred North Whitehead and Bertrand Russell", Title="Principia Mathematica", Publisher="Cambridge University Press", Address="Cambridge, England", Year="1913", Note="3 volumes; first edition 1913, second edition 1927") @Book(Wilder52, FullAuthor="Raymond L. Wilder", Author="R. L. Wilder", Title="Introduction to the Foundations of Mathematics", Publisher="John Wiley & Sons", Year=1952, Address="New York") @inproceedings{Wolf98, author = {Andreas Wolf}, title = {{A} {S}tep {T}owards a {B}etter {U}nderstanding of {A}utomatically {G}enerated {M}odel {E}limination {P}roofs}, booktitle = {Information Technologies and Knowledge Systems (IT\&KNOWS'98) --- {P}roceedings of the XV.\ IFIP World Computer Congress}, editor = {Jos{\'e} Cuena}, year = {1998}, annote = {ISBN 3-85403-122-X}, pages = {415--428}, publisher = {{\"O}sterreichische Computergesellschaft/International Federation for Information Processing}, } @inproceedings{WolfSchumann97, AUTHOR = {Andreas Wolf and Johann Schumann}, TITLE = {ILF-SETHEO: Processing Model Elimination Proof for Natural Language Output }, crossref = {CADE14}, pages = {61--64} } @inproceedings{Wolf97, author = {Andreas Wolf}, title = {{A} {T}ranslation of {M}odel {E}limination {P}roofs into a {S}tructured {N}atural {D}eduction}, booktitle = {Proc.\ of 10th Int.\ Florida AI Research Society Conference}, year = {1997}, editor = {Douglas D. Dankel II}, pages = {11-15}, publisher = {Florida AI Research Society}, address = {Daytona Beach, FL, USA}, } @article{Wolf94, author = {Andreas Wolf}, title = {{O}ptimization and {T}ranslation of {T}ableau-{P}roofs into {R}esolution}, journal = {Journal of Information Processing and Cybernetics (EIK)}, year = {1994}, volume = {30}, number = {5-6}, pages = {311-325}, note = {Akademie Verlag Berlin}, } @Book(WolframD93, Author="D. A. Wolfram", Title="The Clausal Theory of Types", Publisher="Cambridge University Press", series="Cambridge Tracts in Theoretical Computer Science", volume="21", Year=1993) @Book(Wolfram88, Author="S. Wolfram", Title="Mathematica: A System for Doing Mathematics by Computer", Publisher="Wolfram Research, Inc.", Year=1988, Address="New York") @Article(Wos90, Title="The Problem of Finding a Mapping between Clause Representation and Natural-Deduction Representation", Author="Larry Wos", Journal=jar, Year=1990, Pages="211--212", Volume=6) @Article(Wos87, Title="The Problem of Definition Expansion and Contraction", Author="Larry Wos", Journal=jar, Year=1987, Pages="433--435", Volume=3) @Book(Wos84, Author="Larry Wos and Ross Overbeek and Ewing Lusk and Jim Boyle", Title="Automated Reasoning. Introduction and Applications", Publisher="Prentice Hall", Year=1984) @Article(Wos65, Author="Lawrence Wos and George A. Robinson and Daniel F. Carson", Title="Efficiency and Completeness of the Set of Support Strategy in Theorem Proving", Journal=jacm, Year=1965, Volume=12, Pages="536--541") @Article(Yasuhara75, Author="Mitsuru Yasuhara", Title="The Axiom of Choice in {C}hurch's Type Theory (abstract)", Journal=nams, Year=1975, Volume=22, Month=jan, Pages="A--34") @InProceedings{ZimmerKohlhase02, author = {J{\"u}rgen Zimmer and Michael Kohlhase}, title = {System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning}, pages = {139--143}, crossref = "cade18" } @Book(Zylberajch91, author="Cecile Zylberajch", Title="Syntaxe et Semantique de la Facilite en Lambda-Calcul", Publisher="These de Doctorat, Mathematiques, Universite de Paris VII", Year=1991) @COMMENT(This is classified as a book because we do not want references to say "Phd thesis") %Crossreferences go below this line %Crossreferences should have both title and booktitle so that there will be a booktitle %whether the book is listed as a separate item or as part of the information for a paper @Proceedings{AAAI99, key = {AAAI99}, title = "Proceedings of the {Sixteenth National Conference on Artificial Intelligence (AAAI-99)} and {Eleventh Innovative Application of Artificial Intelligence Conference (IAAI-99)}", booktitle = "Proceedings of the {Sixteenth National Conference on Artificial Intelligence (AAAI-99)} and {Eleventh Innovative Application of Artificial Intelligence Conference (IAAI-99)}", year = 1999, publisher = "{AAAI} Press" } @Book{Bibel98a, title="Automated Deuction -- A Basis for Applications", booktitle="Automated Deduction -- A Basis for Applications", publisher="Kluwer", year=1998, editor="Wolfgang Bibel and Peter Schmitt"} @proceedings(cade5, Editor="W. Bibel and R. Kowalski", Address="Les Arcs, France", Series=lncs, Volume=87, Publisher=sv, BookTitle=proc # "5th " # cade, Title=proc # "5th " # cade, Year=1980) @proceedings(cade6, Editor="Donald W. Loveland", Address="New York, USA", Series=lncs, Volume=138, Publisher=sv, Booktitle=proc # "6th " # cade, Title=proc # "6th " # cade, Year=1982) @proceedings(cade7, Editor="R. E. Shostak", Series=lncs, Volume=170, Address="Napa, California, USA", Publisher=sv, Booktitle=proc # "7th " # cade, Title=proc # "7th " # cade, Year=1984) @proceedings(cade8, Booktitle=proc # "8th " # cade, Title=proc # "8th " # cade, Series=lncs, Volume=230, Publisher=sv, Editor="J{\"{o}}rg H. Siekmann", Address="Oxford, England", Year=1986) @proceedings(cade9, Booktitle=proc # "9th " # cade, Title=proc # "9th " # cade, Editor="Ewing Lusk and Ross Overbeek", Address="Argonne, Illinois", Series=lncs, Volume=310, Publisher=sv, Year=1988) @proceedings(cade10, Booktitle=proc # "10th " # cade, Title=proc # "10th " # cade, Editor="M. E. Stickel", Address="Kaiserslautern, Germany", Series=lnai, Volume=449, Publisher=sv, Year=1990) @proceedings(cade11, booktitle=proc # "11th " # cade, title=proc # "11th " # cade, address="Saratoga Springs, NY, USA", editor="D. Kapur", publisher=sv, series=lnai, volume=607, year=1992) @proceedings(cade12, Booktitle=proc # "12th " # cade, Title=proc # "12th " # cade, Editor="Alan Bundy", Address="Nancy, France", Series=lnai, Volume=814, Publisher=sv, Year=1994) @proceedings(cade13, Booktitle=proc # "13th " # cade, title=proc # "13th " # cade, Editor="M.A. McRobbie and J.K. Slaney", Series=lnai, Volume=1104, address="New Brunswick, NJ, USA", Publisher=sv, Year=1996) @proceedings(cade14, booktitle=proc # "14th " # cade, title=proc # "14th " # cade, publisher=sv, Series=lnai, Volume=1249, address="Townsville, North Queensland, Australia", editor="William McCune", year=1997) @proceedings(cade15, booktitle=proc # "15th " # cade, title=proc # "15th " # cade, publisher=sv, Series=lnai, Volume=1421, editor="Claude Kirchner and H{\'{e}}l{\`{e}}ne Kirchner", address="Lindau, Germany", year=1998) @proceedings(cade16, booktitle=proc # "16th " # cade, title=proc # "16th " # cade, Series=lnai, Publisher=sv, Volume=1632, editor="Harald Ganzinger", address="Trento, Italy", year=1999) @proceedings(cade17, booktitle=proc # "17th " # cade, title=proc # "17th " # cade, publisher=sv, Series=lnai, Volume=1831, editor="David McAllester", address="Pittsburgh, PA, USA", year=2000) @proceedings(cade18, booktitle=proc # "18th " # cade, title=proc # "18th " # cade, publisher=sv, Series=lnai, Volume=2392, editor="Andrei Voronkov", url="http://www.springeronline.com/sgw/cda/frontpage/0,11855,5-147-22-2247523-0,00.html?changeHeader=true", address="Copenhagen, Denmark", year=2002) @proceedings(cade19, booktitle=proc # "19th " # cade, title=proc # "19th " # cade, publisher=sv, Series=lnai, Volume=2741, editor="Franz Baader", address="Miami Beach, FL, USA", year=2003) @Proceedings{cl2000, booktitle = {Computational Logic -- CL 2000; First International Conference}, editor = {John Lloyd and Veronica Dahl and Ulrich Furbach and Manfred Kerber and Kung-Kiu Lau and Catuscia Palamidessi and Lu{\'i}s Moniz Pereira and Yehoshua Sagiv and Peter J. Stuckey}, Address="London, UK", publisher = {Springer, Heidelberg}, series = lncs, volume = {1861}, issn = {0302-9743}, year = {2000} } @Proceedings{DaleEtAl:aoanlg92, booktitle = {Aspects of Automated Natural Language Generation}, title = {Aspects of Automated Natural Language Generation}, year = 1992, publisher = {Springer Verlag}, editor = {Robert Dale and Eduard Hovy and Dietmar R{\"o}sner and Oliviero Stock}, volume = 587, series = {Lecture Notes in Artifical Intelligence} } @proceedings(ijcai3, key="IJCAI-3", organization="IJCAI", booktitle=proc # "Third " # ijcai, title=proc # "Third " # ijcai, address="Stanford University, California, USA", year=1973) @proceedings(ijcai4, key="IJCAI-4", Booktitle=proc # "Fourth " # ijcai, Title=proc # "Fourth " # ijcai, Address="Tbilisi, Georgia", Year=1975) @proceedings(ijcai5, key="IJCAI-5", organization="IJCAI", title=proc # "5th " # ijcai # "{, IJCAI-77}", booktitle=proc # "5th " # ijcai # "{, IJCAI-77}", address="MIT, Cambridge, MA", year=1977) @proceedings(ijcai6, organization="IJCAI", title=proc # "Sixth " # ijcai, booktitle=proc # "Sixth " # ijcai, address="Tokyo, Japan", editor="B.G. Buchanan", year=1979) @proceedings(ijcai7, key="IJCAI-7", Booktitle=proc # "Seventh " # ijcai, Title=proc # "Seventh " # ijcai, Address="Vancouver, B.C., Canada", organization="IJCAI", Year=1981) @proceedings(ijcai8, key="IJCAI-8", Booktitle=proc # "Eighth " # ijcai, Title=proc # "Eighth " # ijcai, Address="Karlsruhe, Germany", organization="IJCAI", Year=1983) @proceedings(ijcai9, key="IJCAI-9", Booktitle=proc # "Ninth " # ijcai, Title=proc # "Ninth " # ijcai, Address="Los Angeles, California", organization="IJCAI", Year=1985) @proceedings(ijcai10, key="IJCAI-10", Booktitle=proc # "Tenth " # ijcai, Title=proc # "Tenth " # ijcai, Address="Los Altos, California", organization="IJCAI", Year=1987) @proceedings(ijcai11, Booktitle=proc # "Eleventh " # ijcai, Title=proc # "Eleventh " # ijcai, Address="Detroit, Michigan, USA", Editor="N.S. Sridharan", organization="IJCAI", publisher="Morgan Kaufmann", Year=1989) @proceedings(ijcai12, key="IJCAI-12", Booktitle=proc # "Twelfth " # ijcai, Title=proc # "Twelfth " # ijcai, Address="Darling Harbour, Sydney, Australia", organization="IJCAI", Year=1991) @proceedings(ijcai13, Booktitle=proc # "Thirteenth " # ijcai, Title=proc # "Thirteenth " # ijcai, Address="Chambery, France", Editor="R. Bajscy", organization="IJCAI", Year=1993) @Proceedings{IJCAI97, key = "IJCAI97", booktitle = "Proceedings of the 15th {I}nternational {J}oint {C}onference on {A}rtificial {I}ntelligence ({IJCAI-97})", title = "Proceedings of the 15th {I}nternational {J}oint {C}onference on {A}rtificial {I}ntelligence ({IJCAI-97})", year = 1997, editor = "Martha E. Pollack", publisher = "Morgan Kaufmann", address = "Nagoya, JAPAN", annote = {} } %006.3 I611P AT CMU @Proceedings{IJCAI99, key = "IJCAI99", title = "Proceedings of the 16th {I}nternational {J}oint {C}onference on {A}rtificial {I}ntelligence ({IJCAI})", booktitle = "Proceedings of the 16th {I}nternational {J}oint {C}onference on {A}rtificial {I}ntelligence ({IJCAI})", year = 1999, editor = "Thomas Dean", publisher = "Morgan Kaufmann", address = "Stockholm, SWEDEN" } @proceedings(ijcar2001, Title="Automated Reasoning, First International Joint Conference, IJCAR 2001", Booktitle="Automated Reasoning, First International Joint Conference, IJCAR 2001", Address="Siena, Italy", Editor="Rajeev Gor\'{e} and Alexander Leitsch and Tobias Nipkow", publisher=sv, Series=lnai, Volume=2083, Year=2001) @proceedings(ijcar2004, Title="Automated Reasoning, Second International Joint Conference, IJCAR 2004", Booktitle="Automated Reasoning, Second International Joint Conference, IJCAR 2004", Address="Cork, Ireland", Editor="David Basin, Michael Rusinowitch", publisher=sv, Series=lnai, Volume=3097, Year=2004) @proceedings(lics1, Key="LICS-1", Booktitle=proc # lics, Title=proc # lics, Address="Cambridge, MA, USA", Publisher=ieeep, Year=1986) @proceedings(lics2, key="LICS-2", Booktitle=proc # "2nd Annual " # lics, Title=proc # "2nd Annual " # lics, Address="Ithaca, NY, USA", Month=jun, Year=1987, Publisher=ieeep) @proceedings(lics3, key="LICS-3", Booktitle=proc # "3rd Annual " # lics, Title=proc # "3rd Annual " # lics, Address="Edinburgh, Scotland", Month=jul, Year=1988, Publisher=ieeep) @proceedings(lics4, key="LICS-4", Booktitle=proc # "4th Annual " # lics, Title=proc # "4th Annual " # lics, Address="Pacific Grove, California, USA", Month=jun, Year=1989, Publisher=ieeep) @proceedings(lics6, key="LICS-6", Booktitle=proc # "6th Annual " # lics, Title=proc # "6th Annual " # lics, Address="Amsterdam, The Netherlands", Month=jul, Year=1991, Publisher=ieeep) @proceedings(lics7, key="LICS-7", Booktitle=proc # "7th Annual " # lics, Title=proc # "7th Annual " # lics, Address="Santa Cruz, CA, USA", Year=1992, Publisher=ieeep) @proceedings(lics8, key="LICS-8", Booktitle=proc # "8th Annual " # lics, Title=proc # "8th Annual " # lics, Address="Montreal, Canada", Year=1993, Publisher=ieeep) @proceedings(rta98, Booktitle="Rewriting Techniques and Applications. 9th International Conference, RTA-98", Title="Rewriting Techniques and Applications. 9th International Conference, RTA-98", Address="Tsukuba, Japan", publisher=sv, Series=lncs, Volume=1379, editor="Tobias Nipkow", year=1998) %005.131 R454 @proceedings(rta99, Booktitle="Rewriting Techniques and Applications.10th International Conference, RTA-99", Title="Rewriting Techniques and Applications.10th International Conference, RTA-99", Address="Trento, Italy", publisher=sv, Series=lncs, Volume=1631, editor="Paliath Narendran and Michael Rusinowitch", year=1999) @proceedings(tableaux95, Booktitle="Theorem Proving with Analytic Tableaux and Related Methods. 4th International Workshop. (TABLEAUX '95)", Title="Theorem Proving with Analytic Tableaux and Related Methods. 4th International Workshop. (TABLEAUX '95)", Address="Schlo{{\ss}} Rheinfels, St.\ Goar, Germany", Month=may, Year=1995, Editor="Peter Baumgartner and Reiner H{\"{a}}hnle and Joachim Posegga", Series=lnai, Volume=918, Publisher=sv) @proceedings(tableaux96, Booktitle="Theorem Proving with Analytic Tableaux and Related Methods. 5th International Workshop. (TABLEAUX '96)", Title="Theorem Proving with Analytic Tableaux and Related Methods. 5th International Workshop. (TABLEAUX '96)", Address="Terrasini, Italy", Month=may, Editor="Pierangelo Miglioli and Ugo Moscato and Daniele Mundici and Mario Ornaghi", Series=lnai, Volume=1071, Publisher=sv, Year=1996) @proceedings(tableaux97, Booktitle="Theorem Proving with Analytic Tableaux and Related Methods. (TABLEAUX '97)", Title="Theorem Proving with Analytic Tableaux and Related Methods. (TABLEAUX '97)", Address="Pont-a-Mousson, France", Month=may, Editor="Didier Galmiche", Series=lnai, Volume=1227, Publisher=sv, Year=1997) @proceedings(tableaux98, Booktitle="Theorem Proving with Analytic Tableaux and Related Methods. (TABLEAUX '98)", Title="Theorem Proving with Analytic Tableaux and Related Methods. (TABLEAUX '98)", Address="Oisterwijk, The Netherlands", Month=may, Editor="Harrie de Swart", Series=lnai, Volume=1397, Publisher=sv, Year=1998) @proceedings(tableaux99, Booktitle="Theorem Proving with Analytic Tableaux and Related Methods. (TABLEAUX '99)", Title="Theorem Proving with Analytic Tableaux and Related Methods. (TABLEAUX '99)", Address="Saratoga Springs, NY, USA", Month=jun, Editor="Neil V. Murray", Series=lnai, Volume=1617, Publisher=sv, Year=1999) @proceedings(tableaux00, Booktitle="Theorem Proving with Analytic Tableaux and Related Methods. (TABLEAUX 2000)", Title="Theorem Proving with Analytic Tableaux and Related Methods. (TABLEAUX 2000)", Address="St Andrews, Scotland, UK", Month=jul, Editor="Roy Dyckhoff", Series=lnai, Volume=1847, Publisher=sv, Year=2000) %006.333 T11T 2000 at cmu @proceedings(tableaux2003, Booktitle="Automated Reasoning with Analytic Tableaux and Related Methods. (TABLEAUX 2003)", Title="Automated Reasoning with Analytic Tableaux and Related Methods. (TABLEAUX 2003)", Address="Rome, Italy", Month=jul, Editor="Marta Cialdea Mayer and Fiora Pirri", Series=lnai, Volume=2796, Publisher=sv, Year=2003) %next item is in the tphols series @Proceedings(hug93, Editor="Jeffrey J. Joyce and Carl-Johan H. Seger", Booktitle="Higher Order Logic Theorem Proving and Its Applications: 6th International Workshop, HUG '93", Title="Higher Order Logic Theorem Proving and Its Applications: 6th International Workshop, HUG '93", Address="Vancouver, B.C., Canada", Month=aug, Series=lncs, Volume=780, Publisher=sv, Year=1994) @proceedings(tphols9, Booktitle=tphols # " 9th International Conference, TPHOLs'96", Title=tphols # " 9th International Conference, TPHOLs'96", Editor="J. von Wright and J. Grundy and J. Harrison", address="Turku, Finland", series=lncs, volume=1125, publisher=sv, Year=1996) @Proceedings(tphols10, Editor="Elsa L. Gunter and Amy Felty", Title=tphols # " 10th International Conference, TPHOLs'97", BookTitle=tphols # " 10th International Conference, TPHOLs'97", address="Murray Hill, NJ, USA", Series=lncs, Volume=1275, Publisher=sv, Year=1997) @PROCEEDINGS{tphols98, editor = "Jim Grundy and Malcolm Newey", Title=tphols # " 11th International Conference, TPHOLs'98", booktitle =tphols # " 11th International Conference, TPHOLs'98", series = lncs, volume = 1479, address = "Canberra, Australia", year = 1998, publisher = sv} @Proceedings{tphols99, title = {Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'99)}, booktitle = {Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'99)}, year = {1999}, series = {Lecture Notes in Computer Science}, volume = {1690}, editor = {Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th\'ery}, publisher=sv, address = {Nice, France}, month = {September}} @Proceedings{tphols00, title = {Theorem Proving in Higher Order Logics : 13th international conference, TPHOLs 2000}, booktitle = {Theorem Proving in Higher Order Logics : 13th international conference, TPHOLs 2000}, editor = {Mark Aagaard and John Harrison}, year = {2000}, series = lncs, volume = {1869}, publisher=sv, address = {Portland, Oregon, USA}} @Proceedings{tphols01, title = {Theorem Proving in Higher Order Logics : 14th international conference, TPHOLs 2001}, booktitle = {Theorem Proving in Higher Order Logics : 14th international conference, TPHOLs 2001}, editor = {Richard J. Boulton and Paul B. Jackson}, year = {2001}, series = lncs, volume = {2152}, publisher=sv, address = {Edinburgh, Scotland, UK}} @Proceedings{tphols02, title = {Theorem Proving in Higher Order Logics : 15th international conference, TPHOLs 2002}, booktitle = {Theorem Proving in Higher Order Logics : 15th international conference, TPHOLs 2002}, editor = {Victor A. Carreno and C\'{e}sar A. Munoz and Sofi\`{e}ne Tahar}, year = {2002}, series = lncs, volume = {2410}, publisher=sv, address = {Hampton, Va., USA}} % editor = {Victor A. Carreño and César A. Muñoz and Sofiène Tahar}, %should work but doesn't work: % editor = {Victor A. Carre\~{n}o and Cesar A. Mu\~{n}oz and Sofi\`{e}ne Tahar}, @Proceedings{tphols03, title = {Theorem proving in higher order logics : 16th international conference, TPHOLs 2003}, booktitle = {Theorem proving in higher order logics : 16th international conference, TPHOLs 2003}, editor = {David Basin and Burkhart Wolff}, year = {2003}, series = lncs, volume = {2758}, publisher=sv, address = {Rome, Italy}} @Proceedings{tphols04, title = {Theorem proving in higher order logics : 17th international conference, TPHOLs 2004}, booktitle = {Theorem proving in higher order logics : 17th international conference, TPHOLs 2004}, editor = {Konrad Slind and Annette Bunker and Ganesh Gopalakrishnan}, year = {2004}, series = lncs, volume = {3223}, publisher=sv, address = {Park City, Utah}} @Proceedings(ZimmermannCunningham, Booktitle="Visualization in Teaching and Learning Mathematics", Title="Visualization in Teaching and Learning Mathematics", Editor="Walter Zimmermann and Steve Cunningham", Publisher="Mathematical Association of America", Year="1991")