default search action
Chad E. Brown
Person information
- affiliation: Czech Technical University in Prague, Prague, Czech Republic
- affiliation: Saarland University, Germany
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [c36]Johannes Niederhauser
, Chad E. Brown, Cezary Kaliszyk
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic. IJCAR (1) 2024: 86-104 - [c35]Thibault Gauthier, Chad E. Brown:
A Formal Proof of R(4, 5)=25. ITP 2024: 16:1-16:18 - [c34]Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk
Experiments with Choice in Dependently-Typed Higher-Order Logic. LPAR 2024: 311-320 - [c33]Chad E. Brown, Mikolas Janota, Mirek Olsák:
Symbolic Computation for All the Fun. PAAR+SC²@IJCAR 2024: 111-121 - [i16]Thibault Gauthier, Chad E. Brown:
A Formal Proof of R(4, 5)=25. CoRR abs/2404.01761 (2024) - [i15]Chad E. Brown, Mikolás Janota, Mirek Olsák:
Symbolic Computation for All the Fun. CoRR abs/2404.12048 (2024) - [i14]Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk:
Experiments with Choice in Dependently-Typed Higher-Order Logic. CoRR abs/2410.08874 (2024) - [i13]Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk:
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version). CoRR abs/2410.14232 (2024) - 2023
- [c32]Chad E. Brown, Adam Pease
Translating SUMO-K to Higher-Order Set Theory. FroCoS 2023: 255-274 - [c31]Mario Carneiro, Chad E. Brown, Josef Urban:
Automated Theorem Proving for Metamath. ITP 2023: 9:1-9:19 - [c30]Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban:
A Mathematical Benchmark for Inductive Theorem Provers. LPAR 2023: 224-237 - [c29]Julian Parsert
Experiments on Infinite Model Finding in SMT Solving. LPAR 2023: 317-328 - [i12]Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban:
A Mathematical Benchmark for Inductive Theorem Provers. CoRR abs/2304.02986 (2023) - [i11]Chad E. Brown, Adam Pease, Josef Urban:
Translating SUMO-K to Higher-Order Set Theory. CoRR abs/2305.07903 (2023) - 2022
- [c28]Chad E. Brown, Cezary Kaliszyk
Lash 1.0 (System Description). IJCAR 2022: 350-358 - [c27]Chad E. Brown, Cezary Kaliszyk
Proofgold: Blockchain for Formal Methods. FMBC@CAV 2022: 4:1-4:15 - [c26]Chad E. Brown, Mikolás Janota, Cezary Kaliszyk:
Abstract: Challenges and Solutions for Higher-Order SMT Proofs. SMT 2022: 128 - [i10]Chad E. Brown, Cezary Kaliszyk:
Lash 1.0 (System Description). CoRR abs/2205.06640 (2022) - 2021
- [c25]Chad E. Brown, Mikolás Janota:
First-Order Instantiation using Discriminating Terms. SMT 2021: 17-22 - 2020
- [c24]Zsolt Zombori, Josef Urban, Chad E. Brown:
Prolog Technology Reinforcement Learning Prover - (System Description). IJCAR (2) 2020: 489-507 - [c23]Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk
Exploration of neural machine translation in autoformalization of mathematics in Mizar. CPP 2020: 85-98 - [i9]Zsolt Zombori, Josef Urban, Chad E. Brown:
Prolog Technology Reinforcement Learning Prover. CoRR abs/2004.06997 (2020)
2010 – 2019
- 2019
- [j10]Chad E. Brown, Karol Pak:
AIM Loops and the AIM Conjecture. Formaliz. Math. 27(4): 321-335 (2019) - [c22]Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk
GRUNGE: A Grand Unified ATP Challenge. CADE 2019: 123-141 - [c21]Chad E. Brown, Cezary Kaliszyk
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ITP 2019: 9:1-9:16 - [c20]Chad E. Brown, Karol Pak
A Tale of Two Set Theories. CICM 2019: 44-60 - [i8]Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban:
GRUNGE: A Grand Unified ATP Challenge. CoRR abs/1903.02539 (2019) - [i7]Cécilia Pradic, Chad E. Brown:
Cantor-Bernstein implies Excluded Middle. CoRR abs/1904.09193 (2019) - [i6]Chad E. Brown, Karol Pak:
A Tale of Two Set Theories. CoRR abs/1907.08368 (2019) - [i5]Bartosz Piotrowski, Josef Urban, Chad E. Brown, Cezary Kaliszyk:
Can Neural Networks Learn Symbolic Rewriting? CoRR abs/1911.04873 (2019) - [i4]Chad E. Brown, Thibault Gauthier:
Self-Learned Formula Synthesis in Set Theory. CoRR abs/1912.01525 (2019) - [i3]Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban:
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar. CoRR abs/1912.02636 (2019) - 2016
- [c19]Michael Färber
Internal Guidance for Satallax. IJCAR 2016: 349-361 - [c18]Chad E. Brown, Josef Urban:
Extracting Higher-Order Goals from the Mizar Mathematical Library. CICM 2016: 99-114 - [i2]Chad E. Brown, Josef Urban:
Extracting Higher-Order Goals from the Mizar Mathematical Library. CoRR abs/1605.06996 (2016) - [i1]Michael Färber, Chad E. Brown:
Internal Guidance for Satallax. CoRR abs/1605.09293 (2016) - 2015
- [j9]Chad E. Brown:
Reconsidering Pairs and Functions as Sets. J. Autom. Reason. 55(3): 199-210 (2015) - 2014
- [j8]Chad E. Brown, Christine Rizkallah
Glivenko and Kuroda for Simple Type Theory. J. Symb. Log. 79(2): 485-495 (2014) - 2013
- [j7]Chad E. Brown:
Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems. J. Autom. Reason. 51(1): 57-77 (2013) - [c17]Chad E. Brown, Christine Rizkallah:
From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction. PxTP@CADE 2013: 27-42 - 2012
- [c16]Chad E. Brown:
Satallax: An Automatic Higher-Order Prover. IJCAR 2012: 111-117 - 2011
- [j6]Julian Backes, Chad E. Brown:
Analytic Tableaux for Higher-Order Logic with Choice. J. Autom. Reason. 47(4): 451-479 (2011) - [c15]Chad E. Brown:
Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems. CADE 2011: 147-161 - 2010
- [j5]Chad E. Brown, Gert Smolka:
Analytic Tableaux for Simple Type Theory and its First-Order Fragment. Log. Methods Comput. Sci. 6(2) (2010) - [c14]Julian Backes, Chad E. Brown:
Analytic Tableaux for Higher-Order Logic with Choice. IJCAR 2010: 76-90
2000 – 2009
- 2009
- [j4]Christoph Benzmüller, Chad E. Brown, Michael Kohlhase:
Cut-Simulation and Impredicativity. Log. Methods Comput. Sci. 5(1) (2009) - [c13]Geoff Sutcliffe
Progress in the Development of Automated Theorem Proving for Higher-Order Logic. CADE 2009: 116-130 - [c12]Chad E. Brown, Gert Smolka:
Terminating Tableaux for the Basic Fragment of Simple Type Theory. TABLEAUX 2009: 138-151 - [c11]Chad E. Brown, Gert Smolka:
Extended First-Order Logic. TPHOLs 2009: 164-179 - 2007
- [c10]Feryal Fulya Horozal, Chad E. Brown:
Formal Representation of Mathematics in a Dependently Typed Set Theory. Calculemus/MKM 2007: 265-279 - 2006
- [j3]Peter B. Andrews, Chad E. Brown:
TPS: A hybrid automatic-interactive system for developing proofs. J. Appl. Log. 4(4): 367-395 (2006) - [c9]Chad E. Brown:
Combining Type Theory and Untyped Set Theory. IJCAR 2006: 205-219 - [c8]Christoph Benzmüller, Chad E. Brown, Michael Kohlhase:
Cut-Simulation in Impredicative Logics. IJCAR 2006: 220-234 - [c7]Chad E. Brown:
Verifying and Invalidating Textbook Proofs Using Scunak. MKM 2006: 110-123 - [c6]Chad E. Brown:
Encoding Functional Relations in Scunak. LFMTP@FLoC 2006: 127-139 - 2005
- [c5]Chad E. Brown:
Reasoning in Extensional Type Theory with Equality. CADE 2005: 23-37 - [c4]Christoph Benzmüller, Chad E. Brown:
A Structured Set of Higher-Order Problems. TPHOLs 2005: 66-81 - 2004
- [j2]Peter B. Andrews, Chad E. Brown, Frank Pfenning, Matthew Bishop, Sunil Issar, Hongwei Xi:
ETPS: A System to Help Students Write Formal Proofs. J. Autom. Reason. 32(1): 75-92 (2004) - [j1]Christoph Benzmüller
Higher-order semantics and extensionality. J. Symb. Log. 69(4): 1027-1088 (2004) - 2002
- [c3]Chad E. Brown:
Solving for Set Variables in Higher-Order Theorem Proving. CADE 2002: 408-422 - 2000
- [c2]Peter B. Andrews, Matthew Bishop, Chad E. Brown:
System Description: TPS: A Theorem Proving System for Type Theory. CADE 2000: 164-169 - [c1]Peter B. Andrews, Chad E. Brown:
Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic. CADE 2000: 511-512
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-11-28 20:33 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: