Automated Reasoning

10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II

  • Nicolas Peltier
  • Viorica Sofronie-Stokkermans
Conference proceedings IJCAR 2020

Part of the Lecture Notes in Computer Science book series (LNCS, volume 12167)

Also part of the Lecture Notes in Artificial Intelligence book sub series (LNAI, volume 12167)

Table of contents

  1. Front Matter
    Pages i-xvii
  2. Interactive Theorem Proving/HOL

    1. Front Matter
      Pages 1-1
    2. Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi
      Pages 3-20
    3. Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
      Pages 58-78
    4. Dominik Kirst, Dominique Larchey-Wendling
      Pages 79-96
    5. Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric
      Pages 97-118
    6. Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala
      Pages 119-137
    7. Kazuhiko Sakaguchi
      Pages 138-157
    8. Stephan Schulz, Adam Pease
      Pages 158-166
    9. Sebastian Ullrich, Leonardo de Moura
      Pages 167-182
  3. Formalizations

    1. Front Matter
      Pages 183-183
    2. Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub
      Pages 185-203
    3. Paulo Emílio de Vilhena, Lawrence C. Paulson
      Pages 204-220
    4. Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf
      Pages 221-235
    5. Thomas Hales, Rodrigo Raya
      Pages 254-269
  4. Verification

    1. Front Matter
      Pages 289-289
    2. Robin Eßmann, Tobias Nipkow, Simon Robillard
      Pages 291-306
    3. Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie
      Pages 324-340 Open Access
    4. Martin Rau, Tobias Nipkow
      Pages 341-357
  5. Reasoning Systems and Tools

    1. Front Matter
      Pages 359-359
    2. Ahmed Bhayat, Giles Reger
      Pages 361-368
    3. Hadrien Bride, Cheng-Hao Cai, Jin Song Dong, Rajeev Gore, Zhé Hóu, Brendan Mahony et al.
      Pages 369-377
    4. Tiziano Dalmonte, Nicola Olivetti, Gian Luca Pozzato
      Pages 378-387
    5. André Duarte, Konstantin Korovin
      Pages 388-397
    6. Zarathustra Amadeus Goertzel
      Pages 408-415
    7. Raúl Gutiérrez, Salvador Lucas
      Pages 416-435
    8. Raúl Gutiérrez, Salvador Lucas
      Pages 436-447
    9. Jan Jakubův, Karel Chvalovský, Miroslav Olšák, Bartosz Piotrowski, Martin Suda, Josef Urban
      Pages 448-463
    10. Grant Passmore, Simon Cruanes, Denis Ignatovich, Dave Aitken, Matt Bray, Elijah Kagan et al.
      Pages 464-471
    11. Giselle Reis, Zan Naeem, Mohammed Hashim
      Pages 480-488
    12. Zsolt Zombori, Josef Urban, Chad E. Brown
      Pages 489-507
  6. Back Matter
    Pages 509-511

Other volumes

  1. 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I
  2. Automated Reasoning
    10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II

About these proceedings


This two-volume set LNAI 12166 and 12167 constitutes the refereed proceedings of the 10th International Joint Conference on Automated Reasoning, IJCAR 2020, held in Paris, France, in July 2020.* In 2020, IJCAR was a merger of the following leading events, namely CADE (International Conference on Automated Deduction), FroCoS (International Symposium on Frontiers of Combining Systems), ITP (International Conference on Interactive Theorem Proving), and TABLEAUX (International Conference on Analytic Tableaux and Related Methods).

The 46 full research papers, 5 short papers, and 11 system descriptions presented together with two invited talks were carefully reviewed and selected from 150 submissions. The papers focus on the following topics:

Part I: SAT; SMT and QBF; decision procedures and combination of theories; superposition; proof procedures; non classical logics

Part II: interactive theorem proving/ HOL; formalizations; verification; reasoning systems and tools

*The conference was held virtually due to the COVID-19 pandemic.

Chapter ‘A Fast Verified Liveness Analysis in SSA Form’ is available open access under a Creative Commons Attribution 4.0 International License via


artificial intelligence automata theory automated reasoning computer programming formal languages formal logic linguistics modal logic model checking satisfiability semantics software architecture software design software engineering software quality theorem provers verification verification and validation

Editors and affiliations

  • Nicolas Peltier
    • 1
  • Viorica Sofronie-Stokkermans
    • 2
  1. 1.CNRS, LIG, Université Grenoble AlpesSaint Martin d’HèresFrance
  2. 2.University Koblenz-LandauKoblenzGermany

Bibliographic information

Industry Sectors
IT & Software