Talk Keyword Index

TALK KEYWORD INDEX

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

Shortcuts: A B C F I O P S T V

A
automated theorem proving	Better Proof Output for Vampire
automated verification	Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny
B
Benchmark	Evaluating Automated Theorem Provers Using Adimen-SUMO
blocked clause	Blocked clauses in first-order logic
C
consequence finding	Theory-Specific Reasoning about Loops with Arrays using Vampire
F
Finite term algebra	Handling the Theory of Finite Term Algebras in a Saturation Theorem Prover
first order logic	Revisiting Global Subsumption Blocked clauses in first-order logic Better Proof Output for Vampire
First order theorem prover	Handling the Theory of Finite Term Algebras in a Saturation Theorem Prover
first-order logic	Reasoning about Next-State Relations with Vampire
first-order theorem proving	Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny
I
invariant generation	Theory-Specific Reasoning about Loops with Arrays using Vampire
O
Ontologies	Evaluating Automated Theorem Provers Using Adimen-SUMO
P
polymorphic arrays	Theory-Specific Reasoning about Loops with Arrays using Vampire
program analysis	Reasoning about Next-State Relations with Vampire Theory-Specific Reasoning about Loops with Arrays using Vampire
program verification	Theory-Specific Reasoning about Loops with Arrays using Vampire
proof output	Better Proof Output for Vampire
S
System evaluation	Evaluating Automated Theorem Provers Using Adimen-SUMO
T
theorem proving	Revisiting Global Subsumption
Theory reasoning	Handling the Theory of Finite Term Algebras in a Saturation Theorem Prover
type systems	Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny
V
vampire	Revisiting Global Subsumption Reasoning about Next-State Relations with Vampire Blocked clauses in first-order logic Better Proof Output for Vampire