Automated Reasoning

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

  • Nicola Olivetti
  • Ashish Tiwari
Conference proceedings IJCAR 2016

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

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

Table of contents

  1. Front Matter
    Pages I-XX
  2. Invited Talks

  3. Satisfiability of Boolean Formulas

    1. Front Matter
      Pages 23-23
    2. Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach
      Pages 25-44
    3. Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere
      Pages 45-61
  4. Satisfiability Modulo Theory

    1. Front Matter
      Pages 63-63
    2. Francesco Alberti, Silvio Ghilardi, Elena Pagani
      Pages 65-81
    3. Kshitij Bansal, Andrew Reynolds, Clark Barrett, Cesare Tinelli
      Pages 82-98
    4. Daniel Selsam, Leonardo de Moura
      Pages 99-115
    5. Martin Bromberger, Christoph Weidenbach
      Pages 116-132
    6. Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli
      Pages 133-151
    7. Roberto Sebastiani
      Pages 152-170
  5. Rewriting

    1. Front Matter
      Pages 171-171
    2. Takahito Aoto, Kentaro Kikuchi
      Pages 173-182
    3. Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott
      Pages 183-192
  6. Arithmetic Reasoning and Mechanizing Mathematics

    1. Front Matter
      Pages 193-193
    2. Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, Mingshuai Chen
      Pages 195-212
    3. Takuya Matsuzaki, Hidenao Iwane, Munehiro Kobayashi, Yiyang Zhan, Ryoya Fukasaku, Jumma Kudo et al.
      Pages 213-227
    4. Vu Xuan Tung, To Van Khanh, Mizuhito Ogawa
      Pages 228-237
  7. First-Order Logic and Proof Theory

    1. Front Matter
      Pages 239-239
    2. David M. Cerna, Alexander Leitsch
      Pages 241-256
    3. Viorica Sofronie-Stokkermans
      Pages 273-289
  8. First-Order Theorem Proving

    1. Front Matter
      Pages 291-291
    2. Gabriel Ebner, Stefan Hetzl, Giselle Reis, Martin Riener, Simon Wolfsteiner, Sebastian Zivota
      Pages 293-301
    3. Jens Otten
      Pages 302-312
    4. Kryštof Hoder, Giles Reger, Martin Suda, Andrei Voronkov
      Pages 313-329
  9. Higher-Order Theorem Proving

    1. Front Matter
      Pages 347-347
    2. Michael Färber, Chad Brown
      Pages 349-361
    3. Max Wisniewski, Alexander Steen, Kim Kern, Christoph Benzmüller
      Pages 362-370
  10. Modal and Temporal Logics

    1. Front Matter
      Pages 371-371
    2. Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, Pietro Sala
      Pages 389-405
    3. Open image in new window: A Resolution-Based Prover for Multimodal K
      Cláudia Nalon, Ullrich Hustadt, Clare Dixon
      Pages 406-415
  11. Non-classical Logics

    1. Front Matter
      Pages 433-433
    2. Diana Costa, Manuel A. Martins
      Pages 435-451
    3. Jeremy E. Dawson, James Brotherston, Rajeev Goré
      Pages 452-468
    4. Simon Docherty, David Pym
      Pages 469-486
  12. Verification

    1. Front Matter
      Pages 497-497
    2. Konstantinos Athanasiou, Peizun Liu, Thomas Wahl
      Pages 516-531
    3. F. Frohn, M. Naaf, J. Hensel, M. Brockschmidt, J. Giesl
      Pages 550-567
    4. Lars Hupel, Viktor Kuncak
      Pages 568-577

About these proceedings


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.


description logics higher order logic modal logics temporal logics theorem proving automated reasoning constraint solving deduction differential dynamic logic equational logic and rewriting higher-order rewriting HOL integer arithmetic interactive theorem proving isabelle logic maude program verification proof theory satisfiability

Editors and affiliations

  • Nicola Olivetti
    • 1
  • Ashish Tiwari
    • 2
  1. 1.Aix-Marseille UniversityMarseilleFrance
  2. 2.SRI InternationalMenlo ParkUSA

Bibliographic information

  • DOI
  • Copyright Information Springer International Publishing Switzerland 2016
  • Publisher Name Springer, Cham
  • eBook Packages Computer Science Computer Science (R0)
  • Print ISBN 978-3-319-40228-4
  • Online ISBN 978-3-319-40229-1
  • Series Print ISSN 0302-9743
  • Series Online ISSN 1611-3349
  • Buy this book on publisher's site
Industry Sectors
IT & Software