See also the web page for slides

My Book on Higher Order Automated Reasoning

Chad E Brown Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church's Type Theory College Publications. Studies in Logic: Logic and Cognitive Systems, volume 10. 2007

DeTSeT (Dependently Typed Set Theory) Related Material

One page memo describing the reason for changing the foundation of Omega to DeTSeT. ps pdf

Dependently Typed Set Theory. (A SEKI Report specifying DeTSeT -- a ZFC-style set theory encoded in a dependent type theory with proof irrelevance) ps pdf

Scunak Related Papers

Paper presented at IJCAR 2006: Combining Type Theory and Untyped Set Theory ps pdf bib

Paper presented at LFMTP Workshop 2006: Encoding Functional Relations in Scunak pdf bib

Paper presented at MKM 2006: Verifying and Refuting Textbook Proofs using Scunak ps pdf bib

MKM 2007 Paper with Feryal Fulya Horozal: Formal Representation of Mathematics in a Dependently Typed Set Theory

Scunak Users Manual (in progress)

Automated Theorem Proving

For my thesis work, I studied set comprehension in higher-order theorem proving.

Set Comprehension in Church's Type Theory (Ph.D. Dissertation, 2004) bib

An updated version of my Ph.D. dissertation has been published as a book: Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church's Type Theory

There is also a 20 page description of my Ph.D. Dissertation.

Slides from Talks given in the Math Logic Seminar, Spring 2004

Set Comprehension in Church's Type Theory (Part I)

Abstract

Set Comprehension in Church's Type Theory (Part II)

Abstract

Other Published Papers

Chad E. Brown Reasoning in Extensional Type Theory with Equality CADE 20, 2005, pages 23-37. bib

C. Benzmüller, C. E. Brown, and M. Kohlhase. Higher-Order Semantics and Extensionality, Journal of Symbolic Logic, vol. 69, 2004, pp. 1027-1088. bib

In 2002 at CADE-18, I published the following paper about my work integrating theorem proving with solving set constraints.

Chad E. Brown, Solving for Set Variables in Higher-Order Theorem Proving (copyright Springer-Verlag), Automated Deduction - CADE-18; 18th International Conference on Automated Deduction, Copenhagen, Denmark, edited by Andrei Voronkov, Lecture Notes in Computer Science 2392, Springer 2002, 408--422. Proceedings of CADE-18.

My advisor Peter B. Andrews and I participated in CADE-17, 2000, resulting in the following two publications:

Peter B. Andrews, Matthew Bishop & Chad E. Brown, System Description: TPS: A Theorem Proving System for Type Theory (copyright Springer-Verlag), Automated Deduction - CADE-17; 17th International Conference on Automated Deduction, Pittsburgh, PA, edited by David McAllester, Lecture Notes in Artificial Intelligence 1831, Springer-Verlag, 2000, 164-169. Proceedings of CADE-17.

Peter B. Andrews & Chad E. Brown, Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic, Automated Deduction - CADE-17; 17th International Conference on Automated Deduction, Pittsburgh, PA, edited by David McAllester, Lecture Notes in Artificial Intelligence 1831, Springer-Verlag, 2000, 511-512. Proceedings of CADE-17.

Christoph Benzmüller, Michael Kohlhase and I wrote and published two technical report concerning extensionality in higher-order logics.

Higher Order Semantics and Extensionality.

In 2001 and 2002 I wrote summaries of my work leading to completion of my Ph.D. Here are the 2001 and 2002 reports.

MISC.

Naive Skolemization Makes Lambda Logic Inconsistent: A short paper I wrote in 2006 proving that naive Skolemization, the axiom of choice and the axiom of description are all inconsistent with Lambda Logic pspdf This may be useful for someone learning about Otter Lambda and Lambda Logic.

The following are two reports I wrote about semantics of polymorphic lambda calculus while I was taking a reading course under John Reynolds.

The Standard PER Model in the Reynolds/Ma Framework This report explains how to place the standard PER model in the framework of Reynolds and Ma (by constructing the appropriate PL category). It also shows how to put saturated relations into this framework.

The Bainbridge-Freyd-Scedrov-Scott Parametric PER Model in the Reynolds/Ma Framework This report explains how to place the Bainbridge-Freyd-Scedrov-Scott Parametric PER model in the framework of Reynolds and Ma by constructing appropriate PL categories and functors.

The following is a report I wrote while taking Frank Pfenning's Computation and Deduction as a reading course. It concerns an implementation of the Kolmogorov double negation translation in Twelf.

The Kolmogorov Translation of Classical Logic in Intuitionistic Logic.

My first publication was in the area of Differential Equations. I did this work with my adivisor, Ratnasingham Shivaji, at Mississippi State University.

V. Anuradha, Chad Brown, and R. Shivaji. Explosive non-negative solutions to two point boundary value problem, J. Nonlinear Analysis, TMA 26(3), 1996, pp.613-630.

Finally, I have an old set of notes I wrote years ago about miscellaneous Logic-related literature I read years ago.