LARA

This is an old revision of the document!


Finite Models Imply Decidability

Prover and counterexample finder running in parallel.