Chad E. Brown

According to our database, Chad E. Brown authored at least 44 papers between 2000 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2023

Experiments on Infinite Model Finding in SMT Solving.

Julian Parsert, Chad E. Brown, Mikolas Janota, Cezary Kaliszyk

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

A Mathematical Benchmark for Inductive Theorem Provers.

Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

Automated Theorem Proving for Metamath.

Mario Carneiro, Chad E. Brown, Josef Urban

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

Translating SUMO-K to Higher-Order Set Theory.

Chad E. Brown, Adam Pease, Josef Urban

Proceedings of the Frontiers of Combining Systems - 14th International Symposium, 2023

2022

Abstract: Challenges and Solutions for Higher-Order SMT Proofs.

Chad E. Brown, Mikolás Janota, Cezary Kaliszyk

Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), 2022

Proofgold: Blockchain for Formal Methods.

Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban

Proceedings of the 4th International Workshop on Formal Methods for Blockchains, 2022

Lash 1.0 (System Description).

Chad E. Brown, Cezary Kaliszyk

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

First-Order Instantiation using Discriminating Terms.

Chad E. Brown, Mikolás Janota

Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021), 2021

2020

Prolog Technology Reinforcement Learning Prover.

Zsolt Zombori, Josef Urban, Chad E. Brown

CoRR, 2020

Exploration of neural machine translation in autoformalization of mathematics in Mizar.

Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

Prolog Technology Reinforcement Learning Prover - (System Description).

Zsolt Zombori, Josef Urban, Chad E. Brown

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

AIM Loops and the AIM Conjecture.

Chad E. Brown, Karol Pak

Formaliz. Math., 2019

Self-Learned Formula Synthesis in Set Theory.

Chad E. Brown, Thibault Gauthier

CoRR, 2019

Can Neural Networks Learn Symbolic Rewriting?

Bartosz Piotrowski, Josef Urban, Chad E. Brown, Cezary Kaliszyk

CoRR, 2019

Cantor-Bernstein implies Excluded Middle.

Cécilia Pradic, Chad E. Brown

CoRR, 2019

A Tale of Two Set Theories.

Chad E. Brown, Karol Pak

Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.

Chad E. Brown, Cezary Kaliszyk, Karol Pak

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

GRUNGE: A Grand Unified ATP Challenge.

Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban

Proceedings of the Automated Deduction - CADE 27, 2019

2016

Extracting Higher-Order Goals from the Mizar Mathematical Library.

Chad E. Brown, Josef Urban

Proceedings of the Intelligent Computer Mathematics - 9th International Conference, 2016

Internal Guidance for Satallax.

Michael Färber, Chad E. Brown

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015

Reconsidering Pairs and Functions as Sets.

Chad E. Brown

J. Autom. Reason., 2015

2014

Glivenko and Kuroda for Simple Type Theory.

Chad E. Brown, Christine Rizkallah

J. Symb. Log., 2014

2013

Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems.

Chad E. Brown

J. Autom. Reason., 2013

From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction.

Chad E. Brown, Christine Rizkallah

Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

2012

Satallax: An Automatic Higher-Order Prover.

Chad E. Brown

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

Analytic Tableaux for Higher-Order Logic with Choice.

Julian Backes, Chad E. Brown

J. Autom. Reason., 2011

2010

Analytic Tableaux for Simple Type Theory and its First-Order Fragment

Chad E. Brown, Gert Smolka

Log. Methods Comput. Sci., 2010

2009

Cut-Simulation and Impredicativity

Christoph Benzmüller, Chad E. Brown, Michael Kohlhase

Log. Methods Comput. Sci., 2009

Extended First-Order Logic.

Chad E. Brown, Gert Smolka

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Terminating Tableaux for the Basic Fragment of Simple Type Theory.

Chad E. Brown, Gert Smolka

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2009

Progress in the Development of Automated Theorem Proving for Higher-Order Logic.

Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss

Proceedings of the Automated Deduction, 2009

2007

Formal Representation of Mathematics in a Dependently Typed Set Theory.

Feryal Fulya Horozal, Chad E. Brown

Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

2006

TPS: A hybrid automatic-interactive system for developing proofs.

Peter B. Andrews, Chad E. Brown

J. Appl. Log., 2006

Encoding Functional Relations in Scunak.

Chad E. Brown

Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2006

Verifying and Invalidating Textbook Proofs Using Scunak.

Chad E. Brown

Proceedings of the Mathematical Knowledge Management, 5th International Conference, 2006

Combining Type Theory and Untyped Set Theory.

Chad E. Brown

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

Cut-Simulation in Impredicative Logics.

Christoph Benzmüller, Chad E. Brown, Michael Kohlhase

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

A Structured Set of Higher-Order Problems.

Christoph Benzmüller, Chad E. Brown

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Reasoning in Extensional Type Theory with Equality.

Chad E. Brown

Proceedings of the Automated Deduction, 2005

2004

Higher-order semantics and extensionality.

Christoph Benzmüller, Chad E. Brown, Michael Kohlhase

J. Symb. Log., 2004

ETPS: A System to Help Students Write Formal Proofs.

Peter B. Andrews, Chad E. Brown, Frank Pfenning, Matthew Bishop, Sunil Issar, Hongwei Xi

J. Autom. Reason., 2004

2002

Solving for Set Variables in Higher-Order Theorem Proving.

Chad E. Brown

Proceedings of the Automated Deduction, 2002

2000

System Description: TPS: A Theorem Proving System for Type Theory.

Peter B. Andrews, Matthew Bishop, Chad E. Brown

Proceedings of the Automated Deduction, 2000

Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic.

Peter B. Andrews, Chad E. Brown

Proceedings of the Automated Deduction, 2000