Volume •Abstracts •Preface •Authors •Keywords •BibTex Entries

Vampire 2017. Proceedings of the 4th Vampire Workshop

Editors: Laura Kovács and Andrei Voronkov

EPiC Series in Computing•Volume 53

7 articles•74 pages•Published: June 29, 2018

Papers

Theorem recycling for Theorem Proving

Nikolaj Bjorner and Lev Nachmanson

Pages 1-8

Light-Weight Integration of SAT Solving into First-Order Reasoners – First Experiments

Pages 9-19

An Inference Rule for the Acyclicity Property of Term Algebras

Simon Robillard

Pages 20-32

Local proofs and AVATAR

Giles Reger and Martin Suda

Pages 33-41

Using Vampire with Support for Algebraic Datatypes in Type Soundness Proofs

Sylvia Grewe, André Pacak and Mira Mezini

Pages 42-51

Incremental Solving with Vampire

Giles Reger and Martin Suda

Pages 52-63

Revisiting Question Answering in Vampire

Pages 64-74

Keyphrases

acyclicity, automated theorem proving², Avatar, inference rule, Interpolants, local proofs, Question Answering, SMT solving, soundness proofs of type systems, superposition, term algebra, theorem proving², Vampire³