Extending Nunchaku to Dependent Type Theory

Autor: Simon Cruanes, Jasmin Christian Blanchette

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 210, Iss Proc. HaTT 2016, Pp 3-12 (2016)

Nunchaku is a new higher-order counterexample generator based on a sequence of transformations from polymorphic higher-order logic to first-order logic. Unlike its predecessor Nitpick for Isabelle, it is designed as a stand-alone tool, with frontends

Externí odkaz: https://doaj.org/article/b7a9953e270949af90abbf581487e2a5

Automated Reasoning

Autor: Jasmin Christian Blanchette

Publikováno v: Lecture Notes in Computer Science ISBN: 9783031107689

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::97a35aea699f487c7035540a70e6ba45
https://doi.org/10.1007/978-3-031-10769-6

SAT-Inspired Eliminations for Superposition

Autor: Jasmin Christian Blanchette, Marijn Heule, Petar Vukmirovic

Publikováno v: 21st International Conference on Formal Methods in Computer-Aided Design (FMCAD 2021)
21st International Conference on Formal Methods in Computer-Aided Design (FMCAD 2021), Oct 2021, Virtual, United States. ⟨10.5281/zenodo.4552499⟩
Vukmirović, P, Blanchette, J & Heule, M J H 2023, ' SAT-Inspired Eliminations for Superposition ', ACM Transactions on Computational Logic, vol. 24, no. 1, 3565366, pp. 1-25 . https://doi.org/10.1145/3565366
ACM Transactions on Computational Logic, 24(1):3565366, 1-25. Association for Computing Machinery (ACM)
Vukmirovic, P, Blanchette, J & Heule, M J H 2021, SAT-Inspired Eliminations for Superposition . in R Piskac, M W Whalen, W A Hunt & G Weissenbacher (eds), Proceedings of the 21st Formal Methods in Computer-Aided Design-FMCAD 2021 . Conference Series: Formal Methods in Computer-Aided Design, Institute of Electrical and Electronics Engineers Inc., pp. 231-240, 21st International Conference on Formal Methods in Computer-Aided Design, FMCAD 2021, Virtual, Online, United States, 18/10/21 . https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_32
FMCAD 2021-21st International Conference on Formal Methods in Computer-Aided Design
FMCAD 2021-21st International Conference on Formal Methods in Computer-Aided Design, Oct 2021, New Haven, CT / virtual, United States. pp.231-240, ⟨10.5281/zenodo.4552499⟩

Optimized SAT solvers not only preprocess the clause set, they also transform it during solving as inprocessing. Some preprocessing techniques have been generalized to first-order logic with equality. In this article, we port inprocessing techniques

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::41d3525d3261e4026b00dbfc2b185e06
https://hal.inria.fr/hal-03485200

A Formal Proof of the Expressiveness of Deep Learning

Autor: Dietrich Klakow, Jasmin Christian Blanchette, Alexander Bentkamp

Publikováno v: ITP
Journal of Automated Reasoning
Journal of Automated Reasoning, 63(2), 347-368. Springer Netherlands
Interactive Theorem Proving ISBN: 9783319661063
Journal of Automated Reasoning, Springer Verlag, 2019, 63 (2), pp.347-368. ⟨10.1007/s10817-018-9481-5⟩
Vrije Universiteit Amsterdam
Interactive Theorem Proving-8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017, Proceedings, 10499, 46-64
ITP 2017: 8th International Conference on Interactive Theorem Proving
ITP 2017: 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. ⟨10.1007/3-540-48256-3_12⟩
Journal of Automated Reasoning, 2019, 63 (2), pp.347-368. ⟨10.1007/s10817-018-9481-5⟩
Bentkamp, A, Blanchette, J C & Klakow, D 2019, ' A Formal Proof of the Expressiveness of Deep Learning ', Journal of Automated Reasoning, vol. 63, no. 2, pp. 347-368 . https://doi.org/10.1007/s10817-018-9481-5
Bentkamp, A, Blanchette, J C & Klakow, D 2017, A formal proof of the expressiveness of deep learning . in Interactive Theorem Proving-8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017, Proceedings . vol. 10499, LNCS, Springer, pp. 46-64 .

Deep learning has had a profound impact on computer science in recentyears, with applications to image recognition, language processing, bioinformatics,and more. Recently, Cohen et al. provided theoretical evidence for the superiorityof deep learning

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3150f5319de154298dbcab552d176b51
https://doi.org/10.1007/s10817-018-9481-5

A decision procedure for (co)datatypes in SMT solvers

Autor: Jasmin Christian Blanchette, Andrew Reynolds

Publikováno v: IJCAI 2016-25th International Joint Conference on Artificial Intelligence
IJCAI 2016-25th International Joint Conference on Artificial Intelligence, Jul 2016, New York, United States
Lecture Notes in Computer Science
CADE-25-The 25th jubilee edition of the International Conference on Automated Deduction
CADE-25-The 25th jubilee edition of the International Conference on Automated Deduction, Aug 2015, Berlin, Germany. pp.197-213, ⟨10.1007/978-3-319-21401-6_13⟩
Reynolds, A & Blanchette, J C 2017, ' A decision procedure for (co)datatypes in SMT solvers ', Journal of Automated Reasoning, vol. 58, no. 3, pp. 341-362 . https://doi.org/10.1007/s10817-016-9372-6
Automated Deduction-CADE-25 ISBN: 9783319214009
IJCAI
Journal of Automated Reasoning, 58(3), 341-362. Springer Netherlands
Vrije Universiteit Amsterdam

International audience; We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifies observationally equal codatatype values, including cyc

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::010977b9e713f3b40e74942ddd730063
https://doi.org/10.1007/s10817-016-9372-6