Conditional Simplification

 

Title: Conditional Simplification
Author: Mihails Milehins (user9716869 /at/ gmail /dot/ com)
Submission date: 2021-09-06
Abstract: 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.
BibTeX:
@article{Conditional_Simplification-AFP,
  author  = {Mihails Milehins},
  title   = {Conditional Simplification},
  journal = {Archive of Formal Proofs},
  month   = sep,
  year    = 2021,
  note    = {\url{https://isa-afp.org/entries/Conditional_Simplification.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Used by: CZH_Foundations
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.