default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Chad E. Brown
@inproceedings{DBLP:conf/ijcar/NiederhauserBK24,
author = {Johannes Niederhauser and
Chad E. Brown and
Cezary Kaliszyk},
editor = {Christoph Benzm{\"{u}}ller and
Marijn J. H. Heule and
Renate A. Schmidt},
title = {Tableaux for Automated Reasoning in Dependently-Typed Higher-Order
Logic},
booktitle = {Automated Reasoning - 12th International Joint Conference, {IJCAR}
2024, Nancy, France, July 3-6, 2024, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {14739},
pages = {86--104},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-63498-7\_6},
doi = {10.1007/978-3-031-63498-7\_6},
timestamp = {Fri, 02 Aug 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/ijcar/NiederhauserBK24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/GauthierB24,
author = {Thibault Gauthier and
Chad E. Brown},
editor = {Yves Bertot and
Temur Kutsia and
Michael Norrish},
title = {A Formal Proof of R(4, 5)=25},
booktitle = {15th International Conference on Interactive Theorem Proving, {ITP}
2024, September 9-14, 2024, Tbilisi, Georgia},
series = {LIPIcs},
volume = {309},
pages = {16:1--16:18},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2024},
url = {https://doi.org/10.4230/LIPIcs.ITP.2024.16},
doi = {10.4230/LIPICS.ITP.2024.16},
timestamp = {Mon, 02 Sep 2024 16:55:27 +0200},
biburl = {https://dblp.org/rec/conf/itp/GauthierB24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/RanalterBK24,
author = {Daniel Ranalter and
Chad E. Brown and
Cezary Kaliszyk},
editor = {Nikolaj S. Bj{\o}rner and
Marijn Heule and
Andrei Voronkov},
title = {Experiments with Choice in Dependently-Typed Higher-Order Logic},
booktitle = {{LPAR} 2024: Proceedings of 25th Conference on Logic for Programming,
Artificial Intelligence and Reasoning, Port Louis, Mauritius, May
26-31, 2024},
series = {EPiC Series in Computing},
volume = {100},
pages = {311--320},
publisher = {EasyChair},
year = {2024},
url = {https://doi.org/10.29007/2v8h},
doi = {10.29007/2V8H},
timestamp = {Sun, 04 Aug 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/RanalterBK24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/paar/BrownJO24,
author = {Chad E. Brown and
Mikolas Janota and
Mirek Ols{\'{a}}k},
editor = {Christopher W. Brown and
Daniela Kaufmann and
Cl{\'{a}}udia Nalon and
Alexander Steen and
Martin Suda},
title = {Symbolic Computation for All the Fun},
booktitle = {Joint Proceedings of the 9th Workshop on Practical Aspects of Automated
Reasoning {(PAAR)} and the 9th Satisfiability Checking and Symbolic
Computation Workshop (SC-Square), 2024 co-located with the 12th International
Joint Conference on Automated Reasoning {(IJCAR} 2024), Nancy, France,
July 2, 2024},
series = {{CEUR} Workshop Proceedings},
volume = {3717},
pages = {111--121},
publisher = {CEUR-WS.org},
year = {2024},
url = {https://ceur-ws.org/Vol-3717/paper6.pdf},
timestamp = {Wed, 03 Jul 2024 23:09:04 +0200},
biburl = {https://dblp.org/rec/conf/paar/BrownJO24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2404-01761,
author = {Thibault Gauthier and
Chad E. Brown},
title = {A Formal Proof of R(4, 5)=25},
journal = {CoRR},
volume = {abs/2404.01761},
year = {2024},
url = {https://doi.org/10.48550/arXiv.2404.01761},
doi = {10.48550/ARXIV.2404.01761},
eprinttype = {arXiv},
eprint = {2404.01761},
timestamp = {Wed, 08 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2404-01761.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2404-12048,
author = {Chad E. Brown and
Mikol{\'{a}}s Janota and
Mirek Ols{\'{a}}k},
title = {Symbolic Computation for All the Fun},
journal = {CoRR},
volume = {abs/2404.12048},
year = {2024},
url = {https://doi.org/10.48550/arXiv.2404.12048},
doi = {10.48550/ARXIV.2404.12048},
eprinttype = {arXiv},
eprint = {2404.12048},
timestamp = {Wed, 22 May 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2404-12048.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/BrownPU23,
author = {Chad E. Brown and
Adam Pease and
Josef Urban},
editor = {Uli Sattler and
Martin Suda},
title = {Translating {SUMO-K} to Higher-Order Set Theory},
booktitle = {Frontiers of Combining Systems - 14th International Symposium, FroCoS
2023, Prague, Czech Republic, September 20-22, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14279},
pages = {255--274},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-43369-6\_14},
doi = {10.1007/978-3-031-43369-6\_14},
timestamp = {Wed, 01 Nov 2023 08:59:02 +0100},
biburl = {https://dblp.org/rec/conf/frocos/BrownPU23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/CarneiroBU23,
author = {Mario Carneiro and
Chad E. Brown and
Josef Urban},
editor = {Adam Naumowicz and
Ren{\'{e}} Thiemann},
title = {Automated Theorem Proving for Metamath},
booktitle = {14th International Conference on Interactive Theorem Proving, {ITP}
2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
series = {LIPIcs},
volume = {268},
pages = {9:1--9:19},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2023},
url = {https://doi.org/10.4230/LIPIcs.ITP.2023.9},
doi = {10.4230/LIPICS.ITP.2023.9},
timestamp = {Wed, 21 Aug 2024 22:46:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/CarneiroBU23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/GauthierBJU23,
author = {Thibault Gauthier and
Chad E. Brown and
Mikolas Janota and
Josef Urban},
editor = {Ruzica Piskac and
Andrei Voronkov},
title = {A Mathematical Benchmark for Inductive Theorem Provers},
booktitle = {{LPAR} 2023: Proceedings of 24th International Conference on Logic
for Programming, Artificial Intelligence and Reasoning, Manizales,
Colombia, 4-9th June 2023},
series = {EPiC Series in Computing},
volume = {94},
pages = {224--237},
publisher = {EasyChair},
year = {2023},
url = {https://doi.org/10.29007/jr72},
doi = {10.29007/JR72},
timestamp = {Wed, 12 Jul 2023 16:50:32 +0200},
biburl = {https://dblp.org/rec/conf/lpar/GauthierBJU23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/ParsertBJK23,
author = {Julian Parsert and
Chad E. Brown and
Mikolas Janota and
Cezary Kaliszyk},
editor = {Ruzica Piskac and
Andrei Voronkov},
title = {Experiments on Infinite Model Finding in {SMT} Solving},
booktitle = {{LPAR} 2023: Proceedings of 24th International Conference on Logic
for Programming, Artificial Intelligence and Reasoning, Manizales,
Colombia, 4-9th June 2023},
series = {EPiC Series in Computing},
volume = {94},
pages = {317--328},
publisher = {EasyChair},
year = {2023},
url = {https://doi.org/10.29007/slrm},
doi = {10.29007/SLRM},
timestamp = {Sun, 04 Aug 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/ParsertBJK23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2304-02986,
author = {Thibault Gauthier and
Chad E. Brown and
Mikolas Janota and
Josef Urban},
title = {A Mathematical Benchmark for Inductive Theorem Provers},
journal = {CoRR},
volume = {abs/2304.02986},
year = {2023},
url = {https://doi.org/10.48550/arXiv.2304.02986},
doi = {10.48550/ARXIV.2304.02986},
eprinttype = {arXiv},
eprint = {2304.02986},
timestamp = {Tue, 18 Apr 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2304-02986.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2305-07903,
author = {Chad E. Brown and
Adam Pease and
Josef Urban},
title = {Translating {SUMO-K} to Higher-Order Set Theory},
journal = {CoRR},
volume = {abs/2305.07903},
year = {2023},
url = {https://doi.org/10.48550/arXiv.2305.07903},
doi = {10.48550/ARXIV.2305.07903},
eprinttype = {arXiv},
eprint = {2305.07903},
timestamp = {Wed, 12 Jul 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2305-07903.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BrownK22,
author = {Chad E. Brown and
Cezary Kaliszyk},
editor = {Jasmin Blanchette and
Laura Kov{\'{a}}cs and
Dirk Pattinson},
title = {Lash 1.0 (System Description)},
booktitle = {Automated Reasoning - 11th International Joint Conference, {IJCAR}
2022, Haifa, Israel, August 8-10, 2022, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13385},
pages = {350--358},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-10769-6\_21},
doi = {10.1007/978-3-031-10769-6\_21},
timestamp = {Mon, 24 Oct 2022 16:36:35 +0200},
biburl = {https://dblp.org/rec/conf/cade/BrownK22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/BrownKGU22,
author = {Chad E. Brown and
Cezary Kaliszyk and
Thibault Gauthier and
Josef Urban},
editor = {Zaynah Dargaye and
Clara Schneidewind},
title = {Proofgold: Blockchain for Formal Methods},
booktitle = {4th International Workshop on Formal Methods for Blockchains, FMBC@CAV
2022, August 11, 2022, Haifa, Israel},
series = {OASIcs},
volume = {105},
pages = {4:1--4:15},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2022},
url = {https://doi.org/10.4230/OASIcs.FMBC.2022.4},
doi = {10.4230/OASICS.FMBC.2022.4},
timestamp = {Wed, 21 Aug 2024 22:46:00 +0200},
biburl = {https://dblp.org/rec/conf/cav/BrownKGU22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/smt/BrownJK22,
author = {Chad E. Brown and
Mikol{\'{a}}s Janota and
Cezary Kaliszyk},
editor = {David D{\'{e}}harbe and
Antti E. J. Hyv{\"{a}}rinen},
title = {Abstract: Challenges and Solutions for Higher-Order {SMT} Proofs},
booktitle = {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), Haifa, Israel, August 11-12, 2022},
series = {{CEUR} Workshop Proceedings},
volume = {3185},
pages = {128},
publisher = {CEUR-WS.org},
year = {2022},
url = {https://ceur-ws.org/Vol-3185/abstract697.pdf},
timestamp = {Fri, 10 Mar 2023 16:22:48 +0100},
biburl = {https://dblp.org/rec/conf/smt/BrownJK22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2205-06640,
author = {Chad E. Brown and
Cezary Kaliszyk},
title = {Lash 1.0 (System Description)},
journal = {CoRR},
volume = {abs/2205.06640},
year = {2022},
url = {https://doi.org/10.48550/arXiv.2205.06640},
doi = {10.48550/ARXIV.2205.06640},
eprinttype = {arXiv},
eprint = {2205.06640},
timestamp = {Tue, 17 May 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2205-06640.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/smt/BrownJ21,
author = {Chad E. Brown and
Mikol{\'{a}}s Janota},
editor = {Alexander Nadel and
Aina Niemetz},
title = {First-Order Instantiation using Discriminating Terms},
booktitle = {Proceedings of the 19th International Workshop on Satisfiability Modulo
Theories co-located with 33rd International Conference on Computer
Aided Verification(CAV 2021), Online (initially located in Los Angeles,
USA), July 18-19, 2021},
series = {{CEUR} Workshop Proceedings},
volume = {2908},
pages = {17--22},
publisher = {CEUR-WS.org},
year = {2021},
url = {https://ceur-ws.org/Vol-2908/short6.pdf},
timestamp = {Wed, 12 Jul 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/smt/BrownJ21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/ZomboriUB20,
author = {Zsolt Zombori and
Josef Urban and
Chad E. Brown},
editor = {Nicolas Peltier and
Viorica Sofronie{-}Stokkermans},
title = {Prolog Technology Reinforcement Learning Prover - (System Description)},
booktitle = {Automated Reasoning - 10th International Joint Conference, {IJCAR}
2020, Paris, France, July 1-4, 2020, Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {12167},
pages = {489--507},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-51054-1\_33},
doi = {10.1007/978-3-030-51054-1\_33},
timestamp = {Fri, 03 Jul 2020 13:56:19 +0200},
biburl = {https://dblp.org/rec/conf/cade/ZomboriUB20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/WangBKU20,
author = {Qingxiang Wang and
Chad E. Brown and
Cezary Kaliszyk and
Josef Urban},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Exploration of neural machine translation in autoformalization of
mathematics in Mizar},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {85--98},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373827},
doi = {10.1145/3372885.3373827},
timestamp = {Sun, 02 Oct 2022 15:58:04 +0200},
biburl = {https://dblp.org/rec/conf/cpp/WangBKU20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2004-06997,
author = {Zsolt Zombori and
Josef Urban and
Chad E. Brown},
title = {Prolog Technology Reinforcement Learning Prover},
journal = {CoRR},
volume = {abs/2004.06997},
year = {2020},
url = {https://arxiv.org/abs/2004.06997},
eprinttype = {arXiv},
eprint = {2004.06997},
timestamp = {Tue, 21 Apr 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2004-06997.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fm/BrownP19,
author = {Chad E. Brown and
Karol Pak},
title = {{AIM} Loops and the {AIM} Conjecture},
journal = {Formaliz. Math.},
volume = {27},
number = {4},
pages = {321--335},
year = {2019},
url = {https://doi.org/10.2478/forma-2019-0027},
doi = {10.2478/FORMA-2019-0027},
timestamp = {Sun, 22 Oct 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/fm/BrownP19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BrownGKSU19,
author = {Chad E. Brown and
Thibault Gauthier and
Cezary Kaliszyk and
Geoff Sutcliffe and
Josef Urban},
editor = {Pascal Fontaine},
title = {{GRUNGE:} {A} Grand Unified {ATP} Challenge},
booktitle = {Automated Deduction - {CADE} 27 - 27th International Conference on
Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {11716},
pages = {123--141},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-29436-6\_8},
doi = {10.1007/978-3-030-29436-6\_8},
timestamp = {Wed, 16 Mar 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cade/BrownGKSU19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/BrownKP19,
author = {Chad E. Brown and
Cezary Kaliszyk and
Karol Pak},
editor = {John Harrison and
John O'Leary and
Andrew Tolmach},
title = {Higher-Order Tarski Grothendieck as a Foundation for Formal Proof},
booktitle = {10th International Conference on Interactive Theorem Proving, {ITP}
2019, September 9-12, 2019, Portland, OR, {USA}},
series = {LIPIcs},
volume = {141},
pages = {9:1--9:16},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2019},
url = {https://doi.org/10.4230/LIPIcs.ITP.2019.9},
doi = {10.4230/LIPICS.ITP.2019.9},
timestamp = {Wed, 21 Aug 2024 22:46:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/BrownKP19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/BrownP19,
author = {Chad E. Brown and
Karol Pak},
editor = {Cezary Kaliszyk and
Edwin C. Brady and
Andrea Kohlhase and
Claudio Sacerdoti Coen},
title = {A Tale of Two Set Theories},
booktitle = {Intelligent Computer Mathematics - 12th International Conference,
{CICM} 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {11617},
pages = {44--60},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-23250-4\_4},
doi = {10.1007/978-3-030-23250-4\_4},
timestamp = {Sun, 21 Jun 2020 17:42:36 +0200},
biburl = {https://dblp.org/rec/conf/mkm/BrownP19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1903-02539,
author = {Chad E. Brown and
Thibault Gauthier and
Cezary Kaliszyk and
Geoff Sutcliffe and
Josef Urban},
title = {{GRUNGE:} {A} Grand Unified {ATP} Challenge},
journal = {CoRR},
volume = {abs/1903.02539},
year = {2019},
url = {http://arxiv.org/abs/1903.02539},
eprinttype = {arXiv},
eprint = {1903.02539},
timestamp = {Sun, 31 Mar 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1903-02539.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1904-09193,
author = {C{\'{e}}cilia Pradic and
Chad E. Brown},
title = {Cantor-Bernstein implies Excluded Middle},
journal = {CoRR},
volume = {abs/1904.09193},
year = {2019},
url = {http://arxiv.org/abs/1904.09193},
eprinttype = {arXiv},
eprint = {1904.09193},
timestamp = {Wed, 13 Mar 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1904-09193.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1907-08368,
author = {Chad E. Brown and
Karol Pak},
title = {A Tale of Two Set Theories},
journal = {CoRR},
volume = {abs/1907.08368},
year = {2019},
url = {http://arxiv.org/abs/1907.08368},
eprinttype = {arXiv},
eprint = {1907.08368},
timestamp = {Tue, 23 Jul 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1907-08368.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1911-04873,
author = {Bartosz Piotrowski and
Josef Urban and
Chad E. Brown and
Cezary Kaliszyk},
title = {Can Neural Networks Learn Symbolic Rewriting?},
journal = {CoRR},
volume = {abs/1911.04873},
year = {2019},
url = {http://arxiv.org/abs/1911.04873},
eprinttype = {arXiv},
eprint = {1911.04873},
timestamp = {Mon, 02 Dec 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1911-04873.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1912-01525,
author = {Chad E. Brown and
Thibault Gauthier},
title = {Self-Learned Formula Synthesis in Set Theory},
journal = {CoRR},
volume = {abs/1912.01525},
year = {2019},
url = {http://arxiv.org/abs/1912.01525},
eprinttype = {arXiv},
eprint = {1912.01525},
timestamp = {Thu, 02 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1912-01525.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1912-02636,
author = {Qingxiang Wang and
Chad E. Brown and
Cezary Kaliszyk and
Josef Urban},
title = {Exploration of Neural Machine Translation in Autoformalization of
Mathematics in Mizar},
journal = {CoRR},
volume = {abs/1912.02636},
year = {2019},
url = {http://arxiv.org/abs/1912.02636},
eprinttype = {arXiv},
eprint = {1912.02636},
timestamp = {Fri, 03 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1912-02636.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/FarberB16,
author = {Michael F{\"{a}}rber and
Chad E. Brown},
editor = {Nicola Olivetti and
Ashish Tiwari},
title = {Internal Guidance for Satallax},
booktitle = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9706},
pages = {349--361},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-40229-1\_24},
doi = {10.1007/978-3-319-40229-1\_24},
timestamp = {Mon, 26 Jun 2023 20:45:22 +0200},
biburl = {https://dblp.org/rec/conf/cade/FarberB16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/BrownU16,
author = {Chad E. Brown and
Josef Urban},
editor = {Michael Kohlhase and
Moa Johansson and
Bruce R. Miller and
Leonardo de Moura and
Frank Wm. Tompa},
title = {Extracting Higher-Order Goals from the Mizar Mathematical Library},
booktitle = {Intelligent Computer Mathematics - 9th International Conference, {CICM}
2016, Bialystok, Poland, July 25-29, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9791},
pages = {99--114},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-42547-4\_8},
doi = {10.1007/978-3-319-42547-4\_8},
timestamp = {Thu, 29 Sep 2022 08:36:57 +0200},
biburl = {https://dblp.org/rec/conf/mkm/BrownU16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BrownU16,
author = {Chad E. Brown and
Josef Urban},
title = {Extracting Higher-Order Goals from the Mizar Mathematical Library},
journal = {CoRR},
volume = {abs/1605.06996},
year = {2016},
url = {http://arxiv.org/abs/1605.06996},
eprinttype = {arXiv},
eprint = {1605.06996},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BrownU16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/FarberB16,
author = {Michael F{\"{a}}rber and
Chad E. Brown},
title = {Internal Guidance for Satallax},
journal = {CoRR},
volume = {abs/1605.09293},
year = {2016},
url = {http://arxiv.org/abs/1605.09293},
eprinttype = {arXiv},
eprint = {1605.09293},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/FarberB16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/Brown15,
author = {Chad E. Brown},
title = {Reconsidering Pairs and Functions as Sets},
journal = {J. Autom. Reason.},
volume = {55},
number = {3},
pages = {199--210},
year = {2015},
url = {https://doi.org/10.1007/s10817-015-9340-6},
doi = {10.1007/S10817-015-9340-6},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/Brown15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsyml/BrownR14,
author = {Chad E. Brown and
Christine Rizkallah},
title = {Glivenko and Kuroda for Simple Type Theory},
journal = {J. Symb. Log.},
volume = {79},
number = {2},
pages = {485--495},
year = {2014},
url = {https://doi.org/10.1017/jsl.2013.10},
doi = {10.1017/JSL.2013.10},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsyml/BrownR14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/Brown13,
author = {Chad E. Brown},
title = {Reducing Higher-Order Theorem Proving to a Sequence of {SAT} Problems},
journal = {J. Autom. Reason.},
volume = {51},
number = {1},
pages = {57--77},
year = {2013},
url = {https://doi.org/10.1007/s10817-013-9283-8},
doi = {10.1007/S10817-013-9283-8},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/Brown13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BrownR13,
author = {Chad E. Brown and
Christine Rizkallah},
editor = {Jasmin Christian Blanchette and
Josef Urban},
title = {From Classical Extensional Higher-Order Tableau to Intuitionistic
Intentional Natural Deduction},
booktitle = {Third International Workshop on Proof Exchange for Theorem Proving,
PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
series = {EPiC Series in Computing},
volume = {14},
pages = {27--42},
publisher = {EasyChair},
year = {2013},
url = {https://doi.org/10.29007/8p9q},
doi = {10.29007/8P9Q},
timestamp = {Sun, 15 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/BrownR13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Brown12,
author = {Chad E. Brown},
editor = {Bernhard Gramlich and
Dale Miller and
Uli Sattler},
title = {Satallax: An Automatic Higher-Order Prover},
booktitle = {Automated Reasoning - 6th International Joint Conference, {IJCAR}
2012, Manchester, UK, June 26-29, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7364},
pages = {111--117},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-31365-3\_11},
doi = {10.1007/978-3-642-31365-3\_11},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/Brown12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BackesB11,
author = {Julian Backes and
Chad E. Brown},
title = {Analytic Tableaux for Higher-Order Logic with Choice},
journal = {J. Autom. Reason.},
volume = {47},
number = {4},
pages = {451--479},
year = {2011},
url = {https://doi.org/10.1007/s10817-011-9233-2},
doi = {10.1007/S10817-011-9233-2},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/BackesB11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Brown11,
author = {Chad E. Brown},
editor = {Nikolaj S. Bj{\o}rner and
Viorica Sofronie{-}Stokkermans},
title = {Reducing Higher-Order Theorem Proving to a Sequence of {SAT} Problems},
booktitle = {Automated Deduction - {CADE-23} - 23rd International Conference on
Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6803},
pages = {147--161},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-22438-6\_13},
doi = {10.1007/978-3-642-22438-6\_13},
timestamp = {Mon, 28 Aug 2023 21:17:45 +0200},
biburl = {https://dblp.org/rec/conf/cade/Brown11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1004-1947,
author = {Chad E. Brown and
Gert Smolka},
title = {Analytic Tableaux for Simple Type Theory and its First-Order Fragment},
journal = {Log. Methods Comput. Sci.},
volume = {6},
number = {2},
year = {2010},
url = {http://arxiv.org/abs/1004.1947},
timestamp = {Thu, 25 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1004-1947.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BackesB10,
author = {Julian Backes and
Chad E. Brown},
editor = {J{\"{u}}rgen Giesl and
Reiner H{\"{a}}hnle},
title = {Analytic Tableaux for Higher-Order Logic with Choice},
booktitle = {Automated Reasoning, 5th International Joint Conference, {IJCAR} 2010,
Edinburgh, UK, July 16-19, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6173},
pages = {76--90},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14203-1\_7},
doi = {10.1007/978-3-642-14203-1\_7},
timestamp = {Wed, 25 Sep 2019 18:19:14 +0200},
biburl = {https://dblp.org/rec/conf/cade/BackesB10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-0902-0043,
author = {Christoph Benzm{\"{u}}ller and
Chad E. Brown and
Michael Kohlhase},
title = {Cut-Simulation and Impredicativity},
journal = {Log. Methods Comput. Sci.},
volume = {5},
number = {1},
year = {2009},
url = {http://arxiv.org/abs/0902.0043},
timestamp = {Thu, 25 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-0902-0043.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/SutcliffeBBT09,
author = {Geoff Sutcliffe and
Christoph Benzm{\"{u}}ller and
Chad E. Brown and
Frank Theiss},
editor = {Renate A. Schmidt},
title = {Progress in the Development of Automated Theorem Proving for Higher-Order
Logic},
booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated
Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5663},
pages = {116--130},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-02959-2\_8},
doi = {10.1007/978-3-642-02959-2\_8},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/SutcliffeBBT09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tableaux/BrownS09,
author = {Chad E. Brown and
Gert Smolka},
editor = {Martin Giese and
Arild Waaler},
title = {Terminating Tableaux for the Basic Fragment of Simple Type Theory},
booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods, 18th
International Conference, {TABLEAUX} 2009, Oslo, Norway, July 6-10,
2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5607},
pages = {138--151},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-02716-1\_11},
doi = {10.1007/978-3-642-02716-1\_11},
timestamp = {Tue, 14 May 2019 10:00:54 +0200},
biburl = {https://dblp.org/rec/conf/tableaux/BrownS09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tphol/BrownS09,
author = {Chad E. Brown and
Gert Smolka},
editor = {Stefan Berghofer and
Tobias Nipkow and
Christian Urban and
Makarius Wenzel},
title = {Extended First-Order Logic},
booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference,
TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5674},
pages = {164--179},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-03359-9\_13},
doi = {10.1007/978-3-642-03359-9\_13},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/tphol/BrownS09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/HorozalB07,
author = {Feryal Fulya Horozal and
Chad E. Brown},
editor = {Manuel Kauers and
Manfred Kerber and
Robert Miner and
Wolfgang Windsteiger},
title = {Formal Representation of Mathematics in a Dependently Typed Set Theory},
booktitle = {Towards Mechanized Mathematical Assistants, 14th Symposium, Calculemus
2007, 6th International Conference, {MKM} 2007, Hagenberg, Austria,
June 27-30, 2007, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4573},
pages = {265--279},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-73086-6\_22},
doi = {10.1007/978-3-540-73086-6\_22},
timestamp = {Tue, 14 May 2019 10:00:38 +0200},
biburl = {https://dblp.org/rec/conf/mkm/HorozalB07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/japll/AndrewsB06,
author = {Peter B. Andrews and
Chad E. Brown},
title = {{TPS:} {A} hybrid automatic-interactive system for developing proofs},
journal = {J. Appl. Log.},
volume = {4},
number = {4},
pages = {367--395},
year = {2006},
url = {https://doi.org/10.1016/j.jal.2005.10.002},
doi = {10.1016/J.JAL.2005.10.002},
timestamp = {Tue, 16 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/japll/AndrewsB06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Brown06,
author = {Chad E. Brown},
editor = {Ulrich Furbach and
Natarajan Shankar},
title = {Combining Type Theory and Untyped Set Theory},
booktitle = {Automated Reasoning, Third International Joint Conference, {IJCAR}
2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4130},
pages = {205--219},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11814771\_19},
doi = {10.1007/11814771\_19},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/Brown06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BenzmullerBK06,
author = {Christoph Benzm{\"{u}}ller and
Chad E. Brown and
Michael Kohlhase},
editor = {Ulrich Furbach and
Natarajan Shankar},
title = {Cut-Simulation in Impredicative Logics},
booktitle = {Automated Reasoning, Third International Joint Conference, {IJCAR}
2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4130},
pages = {220--234},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11814771\_20},
doi = {10.1007/11814771\_20},
timestamp = {Sun, 21 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/BenzmullerBK06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/Brown06,
author = {Chad E. Brown},
editor = {Jonathan M. Borwein and
William M. Farmer},
title = {Verifying and Invalidating Textbook Proofs Using Scunak},
booktitle = {Mathematical Knowledge Management, 5th International Conference, {MKM}
2006, Wokingham, UK, August 11-12, 2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4108},
pages = {110--123},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11812289\_10},
doi = {10.1007/11812289\_10},
timestamp = {Tue, 14 May 2019 10:00:38 +0200},
biburl = {https://dblp.org/rec/conf/mkm/Brown06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/Brown07,
author = {Chad E. Brown},
editor = {Alberto Momigliano and
Brigitte Pientka},
title = {Encoding Functional Relations in Scunak},
booktitle = {Proceedings of the First International Workshop on Logical Frameworks
and Meta-Languages: Theory and Practice, LFMTP@FLoC 2006, Seattle,
WA, USA, August 16, 2006},
series = {Electronic Notes in Theoretical Computer Science},
volume = {174},
number = {5},
pages = {127--139},
publisher = {Elsevier},
year = {2006},
url = {https://doi.org/10.1016/j.entcs.2007.01.022},
doi = {10.1016/J.ENTCS.2007.01.022},
timestamp = {Fri, 27 Jan 2023 13:31:48 +0100},
biburl = {https://dblp.org/rec/journals/entcs/Brown07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Brown05,
author = {Chad E. Brown},
editor = {Robert Nieuwenhuis},
title = {Reasoning in Extensional Type Theory with Equality},
booktitle = {Automated Deduction - CADE-20, 20th International Conference on Automated
Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3632},
pages = {23--37},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/11532231\_3},
doi = {10.1007/11532231\_3},
timestamp = {Sun, 02 Oct 2022 15:55:55 +0200},
biburl = {https://dblp.org/rec/conf/cade/Brown05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tphol/BenzmullerB05,
author = {Christoph Benzm{\"{u}}ller and
Chad E. Brown},
editor = {Joe Hurd and
Thomas F. Melham},
title = {A Structured Set of Higher-Order Problems},
booktitle = {Theorem Proving in Higher Order Logics, 18th International Conference,
TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3603},
pages = {66--81},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/11541868\_5},
doi = {10.1007/11541868\_5},
timestamp = {Tue, 14 May 2019 10:00:48 +0200},
biburl = {https://dblp.org/rec/conf/tphol/BenzmullerB05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/AndrewsBPBIX04,
author = {Peter B. Andrews and
Chad E. Brown and
Frank Pfenning and
Matthew Bishop and
Sunil Issar and
Hongwei Xi},
title = {{ETPS:} {A} System to Help Students Write Formal Proofs},
journal = {J. Autom. Reason.},
volume = {32},
number = {1},
pages = {75--92},
year = {2004},
url = {https://doi.org/10.1023/B:JARS.0000021871.18776.94},
doi = {10.1023/B:JARS.0000021871.18776.94},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/AndrewsBPBIX04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsyml/BenzmullerBK04,
author = {Christoph Benzm{\"{u}}ller and
Chad E. Brown and
Michael Kohlhase},
title = {Higher-order semantics and extensionality},
journal = {J. Symb. Log.},
volume = {69},
number = {4},
pages = {1027--1088},
year = {2004},
url = {https://doi.org/10.2178/jsl/1102022211},
doi = {10.2178/JSL/1102022211},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsyml/BenzmullerBK04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Brown02,
author = {Chad E. Brown},
editor = {Andrei Voronkov},
title = {Solving for Set Variables in Higher-Order Theorem Proving},
booktitle = {Automated Deduction - CADE-18, 18th International Conference on Automated
Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {2392},
pages = {408--422},
publisher = {Springer},
year = {2002},
url = {https://doi.org/10.1007/3-540-45620-1\_33},
doi = {10.1007/3-540-45620-1\_33},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/Brown02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/AndrewsBB00,
author = {Peter B. Andrews and
Matthew Bishop and
Chad E. Brown},
editor = {David A. McAllester},
title = {System Description: {TPS:} {A} Theorem Proving System for Type Theory},
booktitle = {Automated Deduction - CADE-17, 17th International Conference on Automated
Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1831},
pages = {164--169},
publisher = {Springer},
year = {2000},
url = {https://doi.org/10.1007/10721959\_11},
doi = {10.1007/10721959\_11},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/AndrewsBB00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/AndrewsB00,
author = {Peter B. Andrews and
Chad E. Brown},
editor = {David A. McAllester},
title = {Tutorial: Using {TPS} for Higher-Order Theorem Proving and {ETPS}
for Teaching Logic},
booktitle = {Automated Deduction - CADE-17, 17th International Conference on Automated
Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1831},
pages = {511--512},
publisher = {Springer},
year = {2000},
url = {https://doi.org/10.1007/10721959\_44},
doi = {10.1007/10721959\_44},
timestamp = {Sun, 21 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/AndrewsB00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
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.
last updated on 2024-09-04 01:24 CEST 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:
