Making Theory Reasoning Simpler

EasyChair Preprint 5000

Abstract

Reasoning with quantifiers and theories is at the core of many applications in program analysis and verification. Whilst the problem is undecidable in general and hard in practice, we have been making large pragmatic steps forward. Our previous work proposed an instantiation rule for theory reasoning that produced pragmatically useful instances. Whilst this led to an increase in performance it had its limitations as the rule produces ground instances which (i) can be overly specific, thus not useful in proof search, and (ii) contribute to the already problematic search space explosion as many new instances are introduced. This paper begins by introducing a form of Gaussian variable elimination that specifically addresses these two concerns as it produces general solutions and it is a simplification rule e.g. it replaces an existing clause by a ‘simpler’ one. Encouraged by initial success with this new rule, we performed an experiment to identify further common cases where the complex structure of theory terms blocked existing methods. This resulted in four further simplification rules for theory reasoning. The resulting extensions are implemented in the Vampire theorem prover and evaluated on SMT-LIB, showing that the new extensions result in a considerable increase in the number of problems solved.

Keyphrases: SMT, automated reasoning, first-order logic, gaussian variable elimination rule, proof search, saturation based proof search, theorem prover, theory reasoning

@booklet{EasyChair:5000,
  author    = {Giles Reger and Johannes Schoisswohl and Andrei Voronkov},
  title     = {Making Theory Reasoning Simpler},
  howpublished = {EasyChair Preprint 5000},
  year      = {EasyChair, 2021}}