Experimental Results for Vampire on the Equational Theories Project

TL;DR

This paper evaluates Vampire, an automated theorem prover, on the Equational Theories Project, demonstrating its effectiveness in proving valid implications and refuting invalid ones in first-order logic.

Contribution

It provides an empirical assessment of Vampire's capabilities on a specific set of equational logic implications, highlighting its strengths and limitations.

Findings

Vampire proved all valid implications in the study.

Vampire refuted most invalid implications.

The results support Vampire's utility in equational logic reasoning.

Abstract

Equational Theories Project is a collaborative effort, which explores the validity of certain first-order logic implications of certain kind. The project has been completed but triggered further research. This report investigates how much can be automatically proven and disproven by the automated theorem prover Vampire. An interesting conclusion is that Vampire can prove all the considered implications that hold and also is able to refute a vast majority of those that do not hold.