Virtual Substitution

Largely based on

• course website of CMU CS15-217
• paper Thirty years of virtual substitution: foundations, techniques, applications

Quantifier Elinimation (QE)

1. Fourier-Motzkin Elimination

1.1. Introduction

1.2. Application to Logic

2. Virtual Substitution