Skip to main content
SpringerLink
Log in
Book cover

Automated Reasoning

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

  • Conference proceedings
  • © 2020

Overview

Editors:
  1. Nicolas Peltier

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

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Viorica Sofronie-Stokkermans

    1. University Koblenz-Landau, Koblenz, Germany

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

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)

Included in the following conference series:

Conference proceedings info: IJCAR 2020.

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

Access this book

Log in via an institution
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

Licence this eBook for your library

Institutional subscriptions

Table of contents (30 papers)

  1. Front Matter

    Pages i-xxvii
    Download chapter PDF

  3. SAT, SMT and QBF

    1. Front Matter

      Pages 11-11
      Download chapter PDF

    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
      Download chapter PDF

    2. Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols

      • Franz Baader, Deepak Kapur
      Pages 163-180

    3. Combined Covers and Beth Definability

      • Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, Andrey Rivkin
      Pages 181-200

    4. Deciding Simple Infinity Axiom Sets with One Binary Relation by Means of Superpostulates

      • Timm Lampert, Anderson Nakano
      Pages 201-217

    5. A Decision Procedure for String to Code Point Conversion

      • Andrew Reynolds, Andres Nötzli, Clark Barrett, Cesare Tinelli
      Pages 218-237

    6. 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
      Download chapter PDF

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

      • Ahmed Bhayat, Giles Reger
      Pages 259-277
Back to top

Other volumes

  1. Automated Reasoning

  2. Automated Reasoning

Keywords

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

Publish with us

Policies and ethics

Back to top

Search

Navigation