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

Vampire17: Volume Information

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

1-8

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

9-19

An Inference Rule for the Acyclicity Property of Term Algebras

Simon Robillard

20-32

Local proofs and AVATAR

Giles Reger and Martin Suda

33-41

Using Vampire with Support for Algebraic Datatypes in Type Soundness Proofs

Sylvia Grewe, André Pacak and Mira Mezini

42-51

Incremental Solving with Vampire

Giles Reger and Martin Suda

52-63

Revisiting Question Answering in Vampire

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