Introduction

Welcome to the Quip documentation. Quip ("Quick Proofs") is an experimental proof format for first-order and higher-order automatic theorem provers, designed to be easy to produce, and reasonably easy to check.

There are two sides to this documentation:

• the point of view of theorem provers, SMT solvers, etc. that might produce Quip proofs;
• the point of view of proof checkers that aim at validating such proofs.

NOTE: the proof format is experimental and its design will most likely fluctuate a lot for a while, as checkers and proof-producing provers are developed.