Skip to main content
  • Conference proceedings
  • © 2020

Automated Reasoning

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

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

Part of the book sub series: Lecture Notes in Artificial Intelligence (LNAI)

Conference series link(s): IJCAR: International Joint Conference on Automated Reasoning

Conference proceedings info: IJCAR 2020.

Buy it now

Buying options

eBook USD 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 79.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

This is a preview of subscription content, log in via an institution to check for access.

Table of contents (33 papers)

  1. Front Matter

    Pages i-xvii
  2. Interactive Theorem Proving/HOL

    1. Front Matter

      Pages 1-1
    2. Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis

      • Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi
      Pages 3-20
    3. Quotients of Bounded Natural Functors

      • Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
      Pages 58-78
    4. Trakhtenbrot’s Theorem in Coq

      • Dominik Kirst, Dominique Larchey-Wendling
      Pages 79-96
    5. Deep Generation of Coq Lemma Names Using Elaborated Terms

      • Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric
      Pages 97-118
    6. Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs

      • Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala
      Pages 119-137
    7. Validating Mathematical Structures

      • Kazuhiko Sakaguchi
      Pages 138-157
    8. Teaching Automated Theorem Proving by Example: PyRes 1.2

      • Stephan Schulz, Adam Pease
      Pages 158-166
    9. Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages

      • Sebastian Ullrich, Leonardo de Moura
      Pages 167-182
  3. Formalizations

    1. Front Matter

      Pages 183-183
    2. Formalizing the Face Lattice of Polyhedra

      • Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub
      Pages 185-203
    3. Algebraically Closed Fields in Isabelle/HOL

      • Paulo Emílio de Vilhena, Lawrence C. Paulson
      Pages 204-220
    4. Formalization of Forcing in Isabelle/ZF

      • Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf
      Pages 221-235
    5. Formal Proof of the Group Law for Edwards Elliptic Curves

      • Thomas Hales, Rodrigo Raya
      Pages 254-269
  4. Verification

    1. Front Matter

      Pages 289-289

Other Volumes

  1. Automated Reasoning

About this book

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 link.springer.com.


Editors and Affiliations

  • CNRS, LIG, Université Grenoble Alpes, Saint Martin d’Hères, France

    Nicolas Peltier

  • University Koblenz-Landau, Koblenz, Germany

    Viorica Sofronie-Stokkermans

Bibliographic Information

Buy it now

Buying options

eBook USD 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 79.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access