# Automatic Generation of Formula Simplifiers based on Conditional Rewrite Rules

arXiv: https://arxiv.org/abs/1602.07285 · HTML: https://mlsanity.com/paper/1602.07285/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Feb 2016.

## Built on by (most cited first, 1 of 1)

- [ObSynth: An Interactive Synthesis System for Generating Object Models from Natural Language Specifications](https://mlsanity.com/paper/2210.11468/) (2022)

## Abstract (arXiv)

This paper addresses the problem of creating simplifiers for logic formulas based on conditional term rewriting. In particular, the paper focuses on a program synthesis application where formula simplifications have been shown to have a significant impact. We show that by combining machine learning techniques with constraint-based synthesis, it is possible to synthesize a formula simplifier fully automatically from a corpus of representative problems, making it possible to create formula simplifiers tailored to specific problem domains. We demonstrate the benefits of our approach for synthesis benchmarks from the SyGuS competition and automated grading.