Books
1Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday, IFCoLog. Editors: Christoph Benzmüller, Chad E. Brown, Jörg Siekmann, Richard Statman. 2008. Available through Amazon
2Chad E. Brown. Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church's Type Theory. 2007. Available through Amazon
Articles in Refereed Journals
3Christoph Benzmüller, Chad E. Brown, Michael Kohlhase. Cut-Simulation in Impredicative Logics. Logical Methods in Computer Science. Volume 5, Issue 1:1-21, March 2009 LMCS Page pdf ps
4Peter B. Andrews, Chad E. Brown. TPS: A hybrid automatic-interactive system for developing proofs. J. Applied Logic 4:367-395, 2006.
5Christoph Benzmüller, Chad E. Brown, Michael Kohlhase. Higher-order semantics and extensionality. Journal of Symbolic Logic 69:1027-1088, 2004. bib pdf
6Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, Hongwei Xi. ETPS: A System to Help Students Write Formal Proofs. J. Autom. Reasoning 32:75-92, 2004.
7V. Anuradha, C. E. Brown, and R. Shivaji. Explosive non-negative solutions to two point boundary value problem, J. Nonlinear Analysis, TMA 26(3), 1996, pp. 613-630.
Articles in Proceedings of Conferences
8Chad E. Brown and Gert Smolka. Extended First-Order Logic. TPHOLs 2009, Springer LNCS 5674, August 2009 pdf Abstract with PDF and BIBTEX bib
9Chad E. Brown and Gert Smolka. Terminating Tableaux for the Basic Fragment of Simple Type Theory. TABLEAUX 2009:138-151, Springer LNCS 5607 Abstract with PDF and BIBTEX pdf bib
10Feryal Fulya Horozal, Chad E. Brown. Formal Representation of Mathematics in a Dependently Typed Set Theory. Toward Mechanized Mathematical Assistants (MKM 2007) 265-279, 2007. pdf
11Chad E. Brown. Verifying and Invalidating Textbook Proofs using Scunak. Mathematical Knowledge Management, MKM 2006 110-123, 2006. ps pdf bib
12Chad E. Brown. Combining Type Theory and Untyped Set Theory. 2006. ps pdf bib
13Christoph Benzmüller, Chad E. Brown, Michael Kohlhase. Cut-Simulation in Impredicative Logics. IJCAR 220-234, 2006. bib pdf
14Chad E. Brown. Reasoning in Extensional Type Theory with Equality. CADE 23-37, 2005. bib ps pdf
15Christoph Benzmüller, Chad E. Brown. A Structured Set of Higher-Order Problems. TPHOLs 66-81, 2005. bib pdf
16Chad E. Brown. Solving for Set Variables in Higher-Order Theorem Proving. CADE 408-422, 2002. ps
Articles in Collections
17Christoph Benzmüller, Chad E. Brown, Michael Kohlhase. Cut Elimination with xi-Functionality. Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday, 2008. bib pdf
18Chad E. Brown. M-Set Models. Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday, 2008. bib pdf
19Christoph Benzmüller, Chad E. Brown. The Curious Inference of Boolos in Mizar and OMEGA.
From Insight to Proof: Festschrift in Honour of Andrzej Trybulec
Studies in Logic, Grammar and Rhetoric. Editors R. Matuszewski and A. Zalewska.
University of Bialystok. 10(23), 299--386. 2007 bib pdf
Workshops Articles
20Chad E. Brown. Encoding Functional Relations in Scunak. LFMTP'2006, 2006. pdf bib
System Descriptions
21Peter B. Andrews, Matthew Bishop, Chad E. Brown. System Description: TPS: A Theorem Proving System for Type Theory. CADE 164-169, 2000. ps
Technical Reports
22Julian Backes and Chad E. Brown. Analytic Tableaux for Higher-Order Logic with Choice. Technical Report, Saarbrücken, Germany, January 2010. Submitted. Abstract with PDF and BIBTEX
23Chad E. Brown and Gert Smolka. Analytic Tableaux for Simple Type Theory and its First-Order Fragment. Technical Report, Saarbrücken, Germany, December 2009. Submitted. Abstract with PDF and BIBTEX
24Chad E. Brown and Gert Smolka. Complete Cut-Free Tableaux for Equational Simple Type Theory. Technical Report, Saarbrücken, Germany, April 2009 Abstract with PDF and BIBTEX
25Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, Hongwei Xi. ETPS: A System to Help Students Write Formal Proofs. Department of Mathematical Sciences, Carnegie Mellon University. 03-002. 2003.
26Christoph Benzmüller, Chad E. Brown, Michael Kohlhase. Higher Order Semantics and Extensionality. Department of Mathematical Sciences, Carnegie Mellon University. 03-001. 2003.
Working Papers
27Chad E. Brown. Dependently Typed Set Theory. SEKI-Working-Paper SWP--2006--03 (ISSN 1860--5931). SEKI Publications. Saarland Univ., 2006. SEKI Page bib pdf
Slides
28Chad E. Brown. Interactive Higher-Order Theorem Proving on the Web. (Slides) Deduktionstreffe, Saarbrücken 2008. pdf
29Chad E. Brown. Nonstandard Models of Fragments of Church's Type Theory. (Slides) CAMELEON, Cambridge, April 2008. pdf The last part of the talk is about an approach to the consistency problem for Quine's NF
30Christoph E. Benzmüller, Chad E. Brown. Slides for Semantics of HOL at ESSLLI 2006. pdf slides 4 on 1 page pdf
31Chad E. Brown. Scunak Proofreads a Latex Proof. (Slides) MKM, 2006 pdf
32Chad E. Brown. Ordinals in Scunak. (Slides) CIAO, April 2006 pdf
33Chad E. Brown. Induction and Cut (CIAO 2005, Nottingham, April 2005) pdf ps
34Chad E. Brown. Reasoning in Extensional Type Theory with Equality (Slides). CADE 23-37, 2005. pdf ps
35Chad E. Brown. Encoding Hybrid Logic in Higher-Order Logic (Loria, Nancy, April 2005) pdf ps
36Chad E. Brown. Benchmarks for Higher-Order Automated Reasoning
(ESHOL Workshop at LPAR, Jamaica, December 2005) pdf Uses a translation of Jutting's Automath encoding of Landau's book -- more information here
37Chad E. Brown. Set Comprehension in Church's Type Theory (Part I). Math Logic Seminar, Carnegie Mellon University, Spring 2004. pdf Abstract
38Chad E. Brown. Set Comprehension in Church's Type Theory (Part II). Math Logic Seminar, Carnegie Mellon University, Spring 2004. pdf Abstract
Abstracts
39Chad E. Brown. Set comprehension in Church's type theory (abstract of contributed talk to the 2004 annual meeting of the Association for Symbolic Logic), Bulletin of Symbolic Logic 11 (2005) 109.
40Chad E. Brown. Set Comprehension in Church's Type Theory -- 20 Page Description. 2005. ps
41Peter B. Andrews, Chad E. Brown. Proving theorems and teaching logic with TPS and ETPS (abstract of contributed talk to the 2004 annual meeting of the Association for Symbolic Logic), Bulletin of Symbolic Logic 11 (2005) 108--109.
Dissertation
42Chad E. Brown. Set Comprehension in Church's Type Theory. 2004. bib pdf
Misc
43Chad E. Brown. Foundations in DeTSeT. Foundations for Mathematics in a Dependently Typed Set Theory. (Online Book) link
44Chad E. Brown. Simptcheck Manual. 2008. Available as part of Simptcheck ps pdf
45Chad E. Brown. Scunak 1.0 Users Manual. 2006. Available as part of Scunak 1.0 ps pdf
46Chad E. Brown. Naive Skolemization Makes Lambda Logic Inconsistent. pdf ps
47Chad E. Brown. Work Summary 2002. ps
48Chad E. Brown. Work Summary 2001. ps
49Web Notes on Automated Theorem Proving link
50Web Notes on Logic link
51Chad E. Brown. The Standard PER Model in the Reynolds/Ma Framework. 1999. ps
52Chad E. Brown. The Bainbridge-Freyd-Scedrov-Scott Parametric PER Model in the Reynolds/Ma Framework. 1999. ps
53Web Notes on Cognitive Science link
54Web Notes on Machine Learning link
55Chad E. Brown. The Kolmogorov Translation of Classical Logic in Intuitionistic Logic. 1998. ps
Formal Documents
56Boolos' Curious Inference in Mizar Main Mizar File Mizar Vocabulary File
Andrzej Trybulec pointed out by email that this Mizar file can be simplified by using Mizar's iter operator.
57Mac Lane Set Theory with Universes (IJCAR2006 Kernel for Scunak 1.0) LISP kernel file for Scunak 1.0