GitHub - cvc5/isabelle-integration-evaluation: Tests to evaluate the reconstruction of cvc5 proofs in the proof assistant Isabelle

cvc5 / isabelle-integration-evaluation Public

Notifications You must be signed in to change notification settings
Fork 0
Star 0

Tests to evaluate the reconstruction of cvc5 proofs in the proof assistant Isabelle

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 51 Commits
Binaries		Binaries
CarcaraElaboration/scripts		CarcaraElaboration/scripts
RewriteReconstruction		RewriteReconstruction
cvc5Reconstruction		cvc5Reconstruction
README		README

Repository files navigation

# isabelle-integration-evaluation
Tests to evaluate the reconstruction of cvc5 proofs in the proof assistant Isabelle

Tests available:
1. Test the impact of reconstructing rewrites with the use of custom lemmas that correspond to rewrite rules instead of merely simplifying.
   -> See RewriteReconstruction/README for more information