The following pages link to HipSpec (Q19753):
Displaying 18 items.
- Proving properties of functional programs by equality saturation (Q300342) (← links)
- Theory exploration powered by deductive synthesis (Q832255) (← links)
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (Q1640636) (← links)
- Superposition with structural induction (Q1687553) (← links)
- Unprovability results for clause set cycles (Q2084942) (← links)
- Induction and Skolemization in saturation theorem proving (Q2084957) (← links)
- Removing algebraic data types from constrained Horn clauses using difference predicates (Q2096439) (← links)
- Induction with generalization in superposition reasoning (Q2219385) (← links)
- Combining induction and saturation-based theorem proving (Q2303240) (← links)
- Inductive theorem proving based on tree grammars (Q2344621) (← links)
- Equivalence checking of two functional programs using inductive theorem provers (Q2410575) (← links)
- TIP: Tons of Inductive Problems (Q3453129) (← links)
- Disproving Inductive Entailments in Separation Logic via Base Pair Approximation (Q3455777) (← links)
- TIP: Tools for Inductive Provers (Q3460056) (← links)
- Automating Inductive Proofs Using Theory Exploration (Q4928454) (← links)
- (Q5140266) (← links)
- Quick specifications for the busy programmer (Q5371995) (← links)
- Hipster: Integrating Theory Exploration in a Proof Assistant (Q5495917) (← links)