Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic. - Peter B. Andrews; Chad E. Brown (CADE, 2000)

System Description: TPS: A Theorem Proving System for Type Theory. - Peter B. Andrews; Matthew Bishop; Chad E. Brown (CADE, 2000)

Solving for Set Variables in Higher-Order Theorem Proving. - Chad E. Brown (CADE, 2002)

ETPS: A System to Help Students Write Formal Proofs. - Peter B. Andrews; Chad E. Brown; Frank Pfenning; Matthew Bishop; Sunil Issar; Hongwei Xi 001 (J. Autom. Reason., 2004)

Higher-order semantics and extensionality. - Christoph Benzmüller; Chad E. Brown; Michael Kohlhase (J. Symb. Log., 2004)

Reasoning in Extensional Type Theory with Equality. - Chad E. Brown (CADE, 2005)

A Structured Set of Higher-Order Problems. - Christoph Benzmüller; Chad E. Brown (TPHOLs, 2005)

Cut-Simulation in Impredicative Logics. - Christoph Benzmüller; Chad E. Brown; Michael Kohlhase (IJCAR, 2006)

Combining Type Theory and Untyped Set Theory. - Chad E. Brown (IJCAR, 2006)

Verifying and Invalidating Textbook Proofs Using Scunak. - Chad E. Brown (MKM, 2006)

Encoding Functional Relations in Scunak. - Chad E. Brown (LFMTP@FLoC, 2006)

TPS: A hybrid automatic-interactive system for developing proofs. - Peter B. Andrews; Chad E. Brown (J. Appl. Log., 2006)

Formal Representation of Mathematics in a Dependently Typed Set Theory. - Feryal Fulya Horozal; Chad E. Brown (Calculemus/MKM, 2007)

Progress in the Development of Automated Theorem Proving for Higher-Order Logic. - Geoff Sutcliffe; Christoph Benzmüller; Chad E. Brown; Frank Theiss (CADE, 2009)

Terminating Tableaux for the Basic Fragment of Simple Type Theory. - Chad E. Brown; Gert Smolka (TABLEAUX, 2009)

Extended First-Order Logic. - Chad E. Brown; Gert Smolka (TPHOLs, 2009)

Cut-Simulation and Impredicativity - Christoph Benzmüller; Chad E. Brown; Michael Kohlhase (Log. Methods Comput. Sci., 2009)

Analytic Tableaux for Simple Type Theory and its First-Order Fragment - Chad E. Brown; Gert Smolka (Log. Methods Comput. Sci., 2010)

Analytic Tableaux for Higher-Order Logic with Choice. - Julian Backes; Chad E. Brown (J. Autom. Reason., 2011)

Satallax: An Automatic Higher-Order Prover. - Chad E. Brown (IJCAR, 2012)

From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction. - Chad E. Brown; Christine Rizkallah (PxTP@CADE, 2013)

Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems. - Chad E. Brown (J. Autom. Reason., 2013)

Glivenko and Kuroda for Simple Type Theory. - Chad E. Brown; Christine Rizkallah (J. Symb. Log., 2014)

Reconsidering Pairs and Functions as Sets. - Chad E. Brown (J. Autom. Reason., 2015)

Internal Guidance for Satallax. - Michael Färber 002; Chad E. Brown (IJCAR, 2016)

Extracting Higher-Order Goals from the Mizar Mathematical Library. - Chad E. Brown; Josef Urban (CICM, 2016)

GRUNGE: A Grand Unified ATP Challenge. - Chad E. Brown; Thibault Gauthier; Cezary Kaliszyk; Geoff Sutcliffe; Josef Urban (CADE, 2019)

Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. - Chad E. Brown; Cezary Kaliszyk; Karol Pak (ITP, 2019)

A Tale of Two Set Theories. - Chad E. Brown; Karol Pak (CICM, 2019)

Cantor-Bernstein implies Excluded Middle. - Cécilia Pradic; Chad E. Brown (CoRR, 2019)

Can Neural Networks Learn Symbolic Rewriting? - Bartosz Piotrowski; Josef Urban; Chad E. Brown; Cezary Kaliszyk (CoRR, 2019)

Self-Learned Formula Synthesis in Set Theory. - Chad E. Brown; Thibault Gauthier (CoRR, 2019)

AIM Loops and the AIM Conjecture. - Chad E. Brown; Karol Pak (Formaliz. Math., 2019)

Prolog Technology Reinforcement Learning Prover - (System Description). - Zsolt Zombori; Josef Urban; Chad E. Brown (IJCAR (2), 2020)

Exploration of neural machine translation in autoformalization of mathematics in Mizar. - Qingxiang Wang; Chad E. Brown; Cezary Kaliszyk; Josef Urban (CPP, 2020)

Prolog Technology Reinforcement Learning Prover. - Zsolt Zombori; Josef Urban; Chad E. Brown (CoRR, 2020)

First-Order Instantiation using Discriminating Terms. - Chad E. Brown; Mikolás Janota (SMT, 2021)

Lash 1.0 (System Description). - Chad E. Brown; Cezary Kaliszyk (IJCAR, 2022)

Proofgold: Blockchain for Formal Methods. - Chad E. Brown; Cezary Kaliszyk; Thibault Gauthier; Josef Urban (FMBC@CAV, 2022)

Abstract: Challenges and Solutions for Higher-Order SMT Proofs. - Chad E. Brown; Mikolás Janota; Cezary Kaliszyk (SMT, 2022)

Translating SUMO-K to Higher-Order Set Theory. - Chad E. Brown; Adam Pease; Josef Urban (FroCoS, 2023)

Automated Theorem Proving for Metamath. - Mario Carneiro; Chad E. Brown; Josef Urban (ITP, 2023)

A Mathematical Benchmark for Inductive Theorem Provers. - Thibault Gauthier; Chad E. Brown; Mikolas Janota; Josef Urban (LPAR, 2023)

Experiments on Infinite Model Finding in SMT Solving. - Julian Parsert; Chad E. Brown; Mikolas Janota; Cezary Kaliszyk (LPAR, 2023)

Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic. - Johannes Niederhauser; Chad E. Brown; Cezary Kaliszyk (IJCAR (1), 2024)

A Formal Proof of R(4, 5)=25. - Thibault Gauthier; Chad E. Brown (ITP, 2024)

Experiments with Choice in Dependently-Typed Higher-Order Logic. - Daniel Ranalter; Chad E. Brown; Cezary Kaliszyk (LPAR, 2024)

Symbolic Computation for All the Fun. - Chad E. Brown; Mikolas Janota; Mirek Olsák (PAAR+SC²@IJCAR, 2024)

Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version). - Johannes Niederhauser; Chad E. Brown; Cezary Kaliszyk (CoRR, 2024)

SMT and Functional Equation Solving over the Reals: Challenges from the IMO. - Chad E. Brown; Karel Chvalovský; Mikolás Janota; Mirek Olsák; Stefan Ratschan (CADE, 2025)