Please respect all copyrights when downloading.

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

3Chad E. Brown. Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems. Journal of Automated Reasoning 51(1):57-77, March 2013 Info At Saarland University
4Chad E. Brown, Christine Rizkallah.Glivenko and Kuroda for Simple Type Theory. Technical Report 2011. Accepted for Publication in the Journal of Symbolic Logic. Info At Saarland University
5Julian Backes, Chad E. Brown. Analytic Tableaux for Higher-Order Logic with Choice. Journal of Automated Reasoning, 2011. DOI 10.1007/s10817-011-9233-2 Info At Saarland University
6Chad E. Brown, Gert Smolka. Analytic Tableaux for Simple Type Theory and its First-Order Fragment. Logical Methods in Computer Science 6:2. June 2010. Info At Saarland University
7Christoph 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
8Peter B. Andrews, Chad E. Brown. TPS: A hybrid automatic-interactive system for developing proofs. J. Applied Logic 4:367-395, 2006.
9Peter 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.
10Christoph Benzmüller, Chad E. Brown, Michael Kohlhase. Higher-order semantics and extensionality. Journal of Symbolic Logic 69:1027-1088, 2004. bib
11V. 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

12Chad E. Brown. Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems. CADE – the 23rd International Conference on Automated Deduction, Proceedings. Editors Nikolaj Bjørner and Viorica Sofronie-Stockkermans. Springer LNCS/LNAI 6803. pp. 147 -- 161. 2011. Info At Saarland University
13Julian Backes, Chad E. Brown. Analytic Tableaux for Higher-Order Logic with Choice. Automated Reasoning: 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010, Proceedings. Editors J¨rgen Geisl, Reiner Hähnle. Springer LNCS/LNAI 6173. pp. 76--90. 2010. Info At Saarland University
14Geoff Sutcliffe, Christoph E. Benzmüller, Chad E. Brown, Frank Theiss. Progress in the Development of Automated Theorem Proving for Higher-Order Logic. Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. Springer LNCS 5663. pp. 116--130. 2009. Info At Saarland University
15Chad E. Brown and Gert Smolka. Extended First-Order Logic. TPHOLs 2009, Springer LNCS 5674, August 2009 pdf Abstract with PDF and BIBTEX bib
16Chad 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
17Feryal Fulya Horozal, Chad E. Brown. Formal Representation of Mathematics in a Dependently Typed Set Theory. Toward Mechanized Mathematical Assistants (MKM 2007) 265-279, 2007.
18Chad E. Brown. Verifying and Invalidating Textbook Proofs using Scunak. Mathematical Knowledge Management, MKM 2006 110-123, 2006. bib
19Christoph Benzmüller, Chad E. Brown, Michael Kohlhase. Cut-Simulation in Impredicative Logics. IJCAR 220-234, 2006. bib
20Chad E. Brown. Combining Type Theory and Untyped Set Theory. 2006. bib
21Chad E. Brown. Reasoning in Extensional Type Theory with Equality. CADE 23-37, 2005. bib
22Christoph Benzmüller, Chad E. Brown. A Structured Set of Higher-Order Problems. TPHOLs 66-81, 2005. bib
23Chad E. Brown. Solving for Set Variables in Higher-Order Theorem Proving. CADE 408-422, 2002.

Articles in Collections

24Chad E. Brown. M-Set Models. Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday, 2008. bib
25Christoph 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
26Christoph 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

Workshops Articles

27Chad E. Brown, Christine Rizkallah. From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction. Third International Workshop on Proof Exchange for Theorem Proving.June 2013 Info At Saarland University
28Chad E. Brown. Encoding Functional Relations in Scunak. LFMTP'2006, 2006. bib

System Descriptions

29Chad E. Brown. Satallax: An Automated Higher-Order Prover. 6th International Joint Conference on Automated Reasoning (IJCAR 2012), pp. 111 -- 117, Springer, 2012 Info At Saarland University
30Peter B. Andrews, Matthew Bishop, Chad E. Brown. System Description: TPS: A Theorem Proving System for Type Theory. CADE 164-169, 2000.

Technical Reports

31Chad E. Brown. Reconsidering Pairs and Functions as Sets. Technical Report, Saarland University, August 2013. Submitted. Info At Saarland University
32Julian 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
33Chad 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
34Chad 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
35Peter 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.
36Christoph Benzmüller, Chad E. Brown, Michael Kohlhase. Higher Order Semantics and Extensionality. Department of Mathematical Sciences, Carnegie Mellon University. 03-001. 2003.

Working Papers

37Chad E. Brown. Dependently Typed Set Theory. SEKI-Working-Paper SWP--2006--03 (ISSN 1860--5931). SEKI Publications. Saarland Univ., 2006. bib