default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID10th IJCAR 2020: Paris, France
- Nicolas Peltier, Viorica Sofronie-Stokkermans:
Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II. Lecture Notes in Computer Science 12167, Springer 2020, ISBN 978-3-030-51053-4
Interactive Theorem Proving/HOL
- Reynald Affeldt
, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi:
Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. 3-20 - Anne Baanen:
A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper). 21-27 - Lukasz Czajka:
Practical Proof Search for Coq by Type Inhabitation. 28-57 - Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel:
Quotients of Bounded Natural Functors. 58-78 - Dominik Kirst, Dominique Larchey-Wendling:
Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model Theory. 79-96 - Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric:
Deep Generation of Coq Lemma Names Using Elaborated Terms. 97-118 - Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala:
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. 119-137 - Kazuhiko Sakaguchi:
Validating Mathematical Structures. 138-157 - Stephan Schulz, Adam Pease:
Teaching Automated Theorem Proving by Example: PyRes 1.2 - (System Description). 158-166 - Sebastian Ullrich, Leonardo de Moura:
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages. 167-182
Formalizations
- Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub:
Formalizing the Face Lattice of Polyhedra. 185-203 - Paulo Emílio de Vilhena, Lawrence C. Paulson:
Algebraically Closed Fields in Isabelle/HOL. 204-220 - Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf:
Formalization of Forcing in Isabelle/ZF. 221-235 - Walter Guttmann:
Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL. 236-253 - Thomas C. Hales, Rodrigo Raya:
Formal Proof of the Group Law for Edwards Elliptic Curves. 254-269 - Filip Maric:
Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation. 270-287
Verification
- Robin Eßmann, Tobias Nipkow, Simon Robillard:
Verified Approximation Algorithms. 291-306 - Peter Lammich:
Efficient Verified Implementation of Introsort and Pdqsort. 307-323 - Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie:
A Fast Verified Liveness Analysis in SSA Form. 324-340 - Martin Rau, Tobias Nipkow:
Verification of Closest Pair of Points Algorithms. 341-357
Reasoning Systems and Tools
- Ahmed Bhayat, Giles Reger:
A Polymorphic Vampire - (Short Paper). 361-368 - Hadrien Bride, Cheng-Hao Cai, Jin Song Dong, Rajeev Goré, Zhé Hóu, Brendan P. Mahony, Jim McCarthy:
N-PAT: A Nested Model-Checker - (System Description). 369-377 - Tiziano Dalmonte, Nicola Olivetti, Gian Luca Pozzato:
HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description). 378-387 - André Duarte, Konstantin Korovin:
Implementing Superposition in iProver (System Description). 388-397 - Marianna Girlando, Lutz Straßburger:
MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description). 398-407 - Zarathustra Amadeus Goertzel:
Make E Smart Again (Short Paper). 408-415 - Raúl Gutiérrez, Salvador Lucas:
Automatically Proving and Disproving Feasibility Conditions. 416-435 - Raúl Gutiérrez, Salvador Lucas:
mu-term: Verify Termination Properties Automatically (System Description). 436-447 - Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban:
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description). 448-463 - Grant O. Passmore, Simon Cruanes, Denis Ignatovich, Dave Aitken, Matt Bray, Elijah Kagan, Kostya Kanishev, Ewen Maclean, Nicola Mometto:
The Imandra Automated Reasoning System (System Description). 464-471 - Adam Pease:
A Programmer's Text Editor for a Logical Theory: The SUMOjEdit Editor (System Description). 472-479 - Giselle Reis, Zan Naeem, Mohammed Hashim:
Sequoia: A Playground for Logicians - (System Description). 480-488 - Zsolt Zombori, Josef Urban, Chad E. Brown:
Prolog Technology Reinforcement Learning Prover - (System Description). 489-507
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 2025-11-28 23:53 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:
