Chad E. Brown

71 papers A 14B 8C 4Journal 31Unranked 14
YearRankTypeTitle / Venue / Authors
2026 J jnl
Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents.
CoRR
Chad E. Brown, Cezary Kaliszyk, Josef Urban
2025 C conf
Exploring Formal Math on the Blockchain: An Explorer for Proofgold.
CICM
Chad E. Brown, Cezary Kaliszyk, Josef Urban
2025 J jnl
Exploring Formal Math on the Blockchain: An Explorer for Proofgold.
CoRR
Chad E. Brown, Cezary Kaliszyk, Josef Urban
2025 C conf
Hammering Higher Order Set Theory.
CICM
Chad E. Brown, Cezary Kaliszyk, Martin Suda, Josef Urban
2025 J jnl
Hammering Higher Order Set Theory.
CoRR
Chad E. Brown, Cezary Kaliszyk, Martin Suda, Josef Urban
2025 — conf
Payment Channels with Proofs.
BCCA
Chad E. Brown, Cezary Kaliszyk, Josef Urban
2025 J jnl
Payment Channels with Proofs.
CoRR
Chad E. Brown, Cezary Kaliszyk, Josef Urban
2025 A conf
SMT and Functional Equation Solving over the Reals: Challenges from the IMO.
CADE
Chad E. Brown, Karel Chvalovský, Mikolás Janota, Mirek Olsák, Stefan Ratschan
2025 J jnl
SMT and Functional Equation Solving over the Reals: Challenges from the IMO.
CoRR
Chad E. Brown, Karel Chvalovský, Mikolás Janota, Mirek Olsák, Stefan Ratschan
2024 B conf
A Formal Proof of R(4, 5)=25.
ITP
Thibault Gauthier, Chad E. Brown
2024 J jnl
A Formal Proof of R(4, 5)=25.
CoRR
Thibault Gauthier, Chad E. Brown
2024 B conf
Experiments with Choice in Dependently-Typed Higher-Order Logic.
LPAR
Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk
2024 J jnl
Experiments with Choice in Dependently-Typed Higher-Order Logic.
CoRR
Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk
2024 — conf
Symbolic Computation for All the Fun.
PAAR+SC²@IJCAR
Chad E. Brown, Mikolas Janota, Mirek Olsák
2024 J jnl
Symbolic Computation for All the Fun.
CoRR
Chad E. Brown, Mikolás Janota, Mirek Olsák
2024 J jnl
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version).
CoRR
Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk
2024 — conf
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic.
IJCAR (1)
Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk
2023 B conf
A Mathematical Benchmark for Inductive Theorem Provers.
LPAR
Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban
2023 J jnl
A Mathematical Benchmark for Inductive Theorem Provers.
CoRR
Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban
2023 B conf
Automated Theorem Proving for Metamath.
ITP
Mario Carneiro, Chad E. Brown, Josef Urban
2023 B conf
Experiments on Infinite Model Finding in SMT Solving.
LPAR
Julian Parsert, Chad E. Brown, Mikolas Janota, Cezary Kaliszyk
2023 — conf
Translating SUMO-K to Higher-Order Set Theory.
FroCoS
Chad E. Brown, Adam Pease, Josef Urban
2023 J jnl
Translating SUMO-K to Higher-Order Set Theory.
CoRR
Chad E. Brown, Adam Pease, Josef Urban
2022 — conf
Abstract: Challenges and Solutions for Higher-Order SMT Proofs.
SMT
Chad E. Brown, Mikolás Janota, Cezary Kaliszyk
2022 A conf
Lash 1.0 (System Description).
IJCAR
Chad E. Brown, Cezary Kaliszyk
2022 J jnl
Lash 1.0 (System Description).
CoRR
Chad E. Brown, Cezary Kaliszyk
2022 — conf
Proofgold: Blockchain for Formal Methods.
FMBC@CAV
Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban
2021 — conf
First-Order Instantiation using Discriminating Terms.
SMT
Chad E. Brown, Mikolás Janota
2020 B conf
Exploration of neural machine translation in autoformalization of mathematics in Mizar.
CPP
Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban
2020 — conf
Prolog Technology Reinforcement Learning Prover - (System Description).
IJCAR (2)
Zsolt Zombori, Josef Urban, Chad E. Brown
2020 J jnl
Prolog Technology Reinforcement Learning Prover.
CoRR
Zsolt Zombori, Josef Urban, Chad E. Brown
2019 C conf
A Tale of Two Set Theories.
CICM
Chad E. Brown, Karol Pak
2019 J jnl
A Tale of Two Set Theories.
CoRR
Chad E. Brown, Karol Pak
2019 J jnl
AIM Loops and the AIM Conjecture.
Formaliz. Math.
Chad E. Brown, Karol Pak
2019 J jnl
Can Neural Networks Learn Symbolic Rewriting?
CoRR
Bartosz Piotrowski, Josef Urban, Chad E. Brown, Cezary Kaliszyk
2019 J jnl
Cantor-Bernstein implies Excluded Middle.
CoRR
Cécilia Pradic, Chad E. Brown
2019 J jnl
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar.
CoRR
Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban
2019 A conf
GRUNGE: A Grand Unified ATP Challenge.
CADE
Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
2019 J jnl
GRUNGE: A Grand Unified ATP Challenge.
CoRR
Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
2019 B conf
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
ITP
Chad E. Brown, Cezary Kaliszyk, Karol Pak
2019 J jnl
Self-Learned Formula Synthesis in Set Theory.
CoRR
Chad E. Brown, Thibault Gauthier
2016 C conf
Extracting Higher-Order Goals from the Mizar Mathematical Library.
CICM
Chad E. Brown, Josef Urban
2016 J jnl
Extracting Higher-Order Goals from the Mizar Mathematical Library.
CoRR
Chad E. Brown, Josef Urban
2016 A conf
Internal Guidance for Satallax.
IJCAR
Michael Färber, Chad E. Brown
2016 J jnl
Internal Guidance for Satallax.
CoRR
Michael Färber, Chad E. Brown
2015 J jnl
Reconsidering Pairs and Functions as Sets.
J. Autom. Reason.
Chad E. Brown
2014 J jnl
Glivenko and Kuroda for Simple Type Theory.
J. Symb. Log.
Chad E. Brown, Christine Rizkallah
2013 — conf
From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction.
PxTP@CADE
Chad E. Brown, Christine Rizkallah
2013 J jnl
Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems.
J. Autom. Reason.
Chad E. Brown
2012 A conf
Satallax: An Automatic Higher-Order Prover.
IJCAR
Chad E. Brown
2011 J jnl
Analytic Tableaux for Higher-Order Logic with Choice.
J. Autom. Reason.
Julian Backes, Chad E. Brown
2011 A conf
Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems.
CADE
Chad E. Brown
2010 A conf
Analytic Tableaux for Higher-Order Logic with Choice.
IJCAR
Julian Backes, Chad E. Brown
2010 J jnl
Analytic Tableaux for Simple Type Theory and its First-Order Fragment
Log. Methods Comput. Sci.
Chad E. Brown, Gert Smolka
2009 J jnl
Cut-Simulation and Impredicativity
Log. Methods Comput. Sci.
Christoph Benzmüller, Chad E. Brown, Michael Kohlhase
2009 — conf
Extended First-Order Logic.
TPHOLs
Chad E. Brown, Gert Smolka
2009 A conf
Progress in the Development of Automated Theorem Proving for Higher-Order Logic.
CADE
Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss
2009 B conf
Terminating Tableaux for the Basic Fragment of Simple Type Theory.
TABLEAUX
Chad E. Brown, Gert Smolka
2007 — conf
Formal Representation of Mathematics in a Dependently Typed Set Theory.
Calculemus/MKM
Feryal Fulya Horozal, Chad E. Brown
2006 A conf
Combining Type Theory and Untyped Set Theory.
IJCAR
Chad E. Brown
2006 A conf
Cut-Simulation in Impredicative Logics.
IJCAR
Christoph Benzmüller, Chad E. Brown, Michael Kohlhase
2006 — conf
Encoding Functional Relations in Scunak.
LFMTP@FLoC
Chad E. Brown
2006 J jnl
TPS: A hybrid automatic-interactive system for developing proofs.
J. Appl. Log.
Peter B. Andrews, Chad E. Brown
2006 — conf
Verifying and Invalidating Textbook Proofs Using Scunak.
MKM
Chad E. Brown
2005 — conf
A Structured Set of Higher-Order Problems.
TPHOLs
Christoph Benzmüller, Chad E. Brown
2005 A conf
Reasoning in Extensional Type Theory with Equality.
CADE
Chad E. Brown
2004 J jnl
ETPS: A System to Help Students Write Formal Proofs.
J. Autom. Reason.
Peter B. Andrews, Chad E. Brown, Frank Pfenning, Matthew Bishop, Sunil Issar, Hongwei Xi
2004 J jnl
Higher-order semantics and extensionality.
J. Symb. Log.
Christoph Benzmüller, Chad E. Brown, Michael Kohlhase
2002 A conf
Solving for Set Variables in Higher-Order Theorem Proving.
CADE
Chad E. Brown
2000 A conf
System Description: TPS: A Theorem Proving System for Type Theory.
CADE
Peter B. Andrews, Matthew Bishop, Chad E. Brown
2000 A conf
Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic.
CADE
Peter B. Andrews, Chad E. Brown