Skip to main content
  • Conference proceedings
  • © 2020

Automated Reasoning

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

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

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 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 89.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 (30 papers)

  1. Front Matter

    Pages i-xxvii
  2. Invited Paper

    1. Front Matter

      Pages 1-1
  3. SAT, SMT and QBF

    1. Front Matter

      Pages 11-11
    2. An SMT Theory of Fixed-Point Arithmetic

      • Marek Baranowski, Shaobo He, Mathias Lechner, Thanh Son Nguyen, Zvonimir Rakamarić
      Pages 13-31
    3. Covered Clauses Are Not Propagation Redundant

      • Lee A. Barnett, David Cerna, Armin Biere
      Pages 32-47
    4. The Resolution of Keller’s Conjecture

      • Joshua Brakensiek, Marijn Heule, John Mackey, David Narváez
      Pages 48-65
    5. How QBF Expansion Makes Strategy Extraction Hard

      • Leroy Chew, Judith Clymo
      Pages 66-82
    6. Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates

      • Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti
      Pages 83-102
    7. Solving Bitvectors with MCSAT: Explanations from Bits and Pieces

      • Stéphane Graham-Lengrand, Dejan Jovanović, Bruno Dutertre
      Pages 103-121
    8. Monadic Decomposition in Integer Linear Arithmetic

      • Matthew Hague, Anthony W. Lin, Philipp Rümmer, Zhilin Wu
      Pages 122-140
    9. Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis

      • Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli
      Pages 141-160
  4. Decision Procedures and Combination of Theories

    1. Front Matter

      Pages 161-161
    2. Combined Covers and Beth Definability

      • Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
      Pages 181-200
    3. A Decision Procedure for String to Code Point Conversion

      • Andrew Reynolds, Andres Nötzli, Clark Barrett, Cesare Tinelli
      Pages 218-237
    4. Politeness for the Theory of Algebraic Datatypes

      • Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark Barrett
      Pages 238-255
  5. Superposition

    1. Front Matter

      Pages 257-257
    2. A Knuth-Bendix-Like Ordering for Orienting Combinator Equations

      • Ahmed Bhayat, Giles Reger
      Pages 259-277

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 ‘Constructive Hybrid Games’ 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 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 89.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