Talk Keyword Index

TALK KEYWORD INDEX

This page contains an index consisting of author-provided keywords.

Shortcuts: A D E F H I P S T U V

A
answer literals	Integrating Answer Literals with AVATAR for Program Synthesis
anti-unification	Heuristic Definition Introduction
automate reasoning	Sorting without Sorts in Vampire
automated reasoning	The Spawns of the Saturation Framework
automated theorem proving	Lazy and Eager Patterns in High-Performance Automated Theorem Proving
AVATAR	Integrating Answer Literals with AVATAR for Program Synthesis
D
Dedukti	Towards verifying Vampire proofs in λΠ-calculus Modulo Theories
definition introduction	Heuristic Definition Introduction
E
efficient algorithms	Lazy and Eager Patterns in High-Performance Automated Theorem Proving
F
first-order theorem proving	Spider: Learning in the Sea of Options Heuristic Definition Introduction Integrating Answer Literals with AVATAR for Program Synthesis
H
Higher-order	New Trends in Higher-Order
I
implementation of logics	Lazy and Eager Patterns in High-Performance Automated Theorem Proving
induction	Sorting without Sorts in Vampire
inductive reasoning	Syntax-driven induction
interactive theorem proving	Towards verifying Vampire proofs in λΠ-calculus Modulo Theories
P
profiling	Engineering Subsumption Resolution in Vampire
program synthesis	Integrating Answer Literals with AVATAR for Program Synthesis
proof interoperability	Towards verifying Vampire proofs in λΠ-calculus Modulo Theories
proof verification	Towards verifying Vampire proofs in λΠ-calculus Modulo Theories
S
saturation	Engineering Subsumption Resolution in Vampire The Spawns of the Saturation Framework
saturation-based theorem proving	Syntax-driven induction
sorting	Sorting without Sorts in Vampire
subsumption resolution	Engineering Subsumption Resolution in Vampire
Superposition	New Trends in Higher-Order
superposition calculus	Spider: Learning in the Sea of Options
T
theorem proving	Engineering Subsumption Resolution in Vampire The Spawns of the Saturation Framework
U
Unification	New Trends in Higher-Order
unit testing	Engineering Subsumption Resolution in Vampire
V
Vampire	Spider: Learning in the Sea of Options Syntax-driven induction
Vampire prover	Towards verifying Vampire proofs in λΠ-calculus Modulo Theories