Conditional Simplification

Mihails Milehins 📧

September 6, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


The article provides a collection of experimental general-purpose proof methods for the object logic Isabelle/HOL of the formal proof assistant Isabelle. The methods in the collection offer functionality that is similar to certain aspects of the functionality provided by the standard proof methods of Isabelle that combine classical reasoning and rewriting, such as the method auto, but use a different approach for rewriting. More specifically, these methods allow for the side conditions of the rewrite rules to be solved via intro-resolution.


BSD License


January 7, 2022
added a switch for backtracking (revision 241da1cdeabf)


Session Conditional_Simplification