Pages that link to "Item:Q1134541"
From MaRDI portal
The following pages link to Mechanizing structural induction. II: Strategies (Q1134541):
Displaying 19 items.
- Using induction and rewriting to verify and complete parameterized specifications (Q672051) (← links)
- Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs (Q673496) (← links)
- Proofs by induction in equational theories with constructors (Q789177) (← links)
- Mathematical induction in Otter-lambda (Q861715) (← links)
- Deaccumulation techniques for improving provability (Q882487) (← links)
- Mechanizing structural induction. I: Formal system (Q1134540) (← links)
- Mechanizing structural induction. II: Strategies (Q1134541) (← links)
- PASCAL in LCF: Semantics and examples of proof (Q1242670) (← links)
- Towards the automation of set theory and its logic (Q1253108) (← links)
- A strong restriction of the inductive completion procedure (Q1824381) (← links)
- Sound generalizations in mathematical induction (Q1882908) (← links)
- Middle-out reasoning for synthesis and induction (Q1915136) (← links)
- Specification and proof in membership equational logic (Q1978640) (← links)
- Equivalence checking of two functional programs using inductive theorem provers (Q2410575) (← links)
- Lean induction principles for tableaux (Q4610315) (← links)
- Termination of algorithms over non-freely generated data types (Q4647505) (← links)
- A divergence critic (Q5210759) (← links)
- Lazy generation of induction hypotheses (Q5210761) (← links)
- A general framework to build contextual cover set induction provers (Q5950934) (← links)
