PAAR 2016
Practical Aspects of Automated Reasoning

Table of Contents

• Preface
  
  

• Efficient Instantiation Techniques in SMT (Work In Progress) 1 - 10
  Haniel Barbosa
  
• Alternative Treatments of Common Binary Relations in First-order Automated Reasoning 11 - 23
  Koen Claessen , Ann Lillieström
  
• No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions 24 - 31
  Michael Färber , Cezary Kaliszyk
  
• Deduction as a Service 32 - 40
  Mohamed Hassona , Stephan Schulz
  
• TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism 41 - 55
  Cezary Kaliszyk , Geoff Sutcliffe , Florian Rabe
  
• Prover-independent Axiom Selection for Automated Theorem Proving in Ontohub 56 - 68
  Eugen Kuksa , Till Mossakowski
  
• On Checking Kripke Models for Modal Logic K 69 - 81
  Jean Marie Lagniez , Daniel Le Berre , Tiago de Lima , Valentin Montmirail
  
• Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers 82 - 94
  Tomer Libal , Alexander Steen
  
• Ordered Resolution with Straight Dismatching Constraints 95 - 109
  Andreas Teucke , Christoph Weidenbach
  
• A Saturation-based Algebraic Reasoner for ELQ 110 - 124
  Jelena Vlasenko , Maryam Daryalal , Volker Haarslev , Brigitte Jaumard
  
• The PIE Environment for First-Order-Based Proving, Interpolating and Eliminating 125 - 138
  Christoph Wernhard