Skip to main content
  • Conference proceedings
  • © 2016

Automated Reasoning

8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016, Proceedings

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

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 2016.

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 (38 papers)

  1. Front Matter

    Pages I-XX
  2. Satisfiability of Boolean Formulas

    1. Front Matter

      Pages 23-23
    2. A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

      • Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
      Pages 25-44
    3. Super-Blocked Clauses

      • Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere
      Pages 45-61
  3. Satisfiability Modulo Theory

    1. Front Matter

      Pages 63-63
    2. Counting Constraints in Flat Array Fragments

      • Francesco Alberti, Silvio Ghilardi, Elena Pagani
      Pages 65-81
    3. A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT

      • Kshitij Bansal, Andrew Reynolds, Clark Barrett, Cesare Tinelli
      Pages 82-98
    4. Congruence Closure in Intensional Type Theory

      • Daniel Selsam, Leonardo de Moura
      Pages 99-115
    5. Fast Cube Tests for LIA Constraint Solving

      • Martin Bromberger, Christoph Weidenbach
      Pages 116-132
    6. Model Finding for Recursive Functions in SMT

      • Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli
      Pages 133-151
    7. Colors Make Theories Hard

      • Roberto Sebastiani
      Pages 152-170
  4. Rewriting

    1. Front Matter

      Pages 171-171
    2. Nominal Confluence Tool

      • Takahito Aoto, Kentaro Kikuchi
      Pages 173-182
    3. Built-in Variant Generation and Unification, and Their Applications in Maude 2.7

      • Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott
      Pages 183-192
  5. Arithmetic Reasoning and Mechanizing Mathematics

    1. Front Matter

      Pages 193-193
    2. Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF

      • Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, Mingshuai Chen
      Pages 195-212

Other Volumes

  1. Automated Reasoning

About this book

This book constitutes the refereed proceedings of the 8th International Joint Conference on Automated Reasoning, IJCAR 2016, held in Coimbra, Portugal, in June/July 2016. IJCAR 2014 was a merger of three leading events in automated reasoning, namely CADE (International Conference on Automated Deduction), FroCoS (International Symposium on Frontiers of Combining Systems) and TABLEAUX (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods).

The 26 revised full research papers and 9 system descriptions presented together with 4 invited talks were carefully reviewed and selected from 79 submissions. The papers have been organized in topical sections on satisfiability of Boolean formulas, satisfiability modulo theory, rewriting, arithmetic reasoning and mechanizing mathematics, first-order logic and proof theory, first-order theorem proving, higher-order theorem proving, modal and temporal logics, non-classical logics, and verification.

Editors and Affiliations

  • Aix-Marseille University, Marseille, France

    Nicola Olivetti

  • SRI International, Menlo Park, USA

    Ashish Tiwari

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