The use of embeddings to provide a clean separation of term and annotation for higher order rippling (Q540694): Difference between revisions

@@ Property / cites work @@
+A calculus for and termination of rippling
@@ Property / cites work: A calculus for and termination of rippling / rank @@
+Normal rank
@@ Property / cites work @@
+Rippling: Meta-Level Guidance for Mathematical Reasoning
+Normal rank
@@ Property / cites work @@
+Rippling: A heuristic for guiding inductive proofs
+Normal rank
@@ Property / cites work @@
+Q4790660
@@ Property / cites work: Q4790660 / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Managing structural information by higher-order colored unification
+Normal rank
@@ Property / cites work @@
+Productive use of failure in inductive proof
@@ Property / cites work: Productive use of failure in inductive proof / rank @@
+Normal rank
@@ Property / cites work @@
+Q4036585
@@ Property / cites work: Q4036585 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2767046
@@ Property / cites work: Q2767046 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle. A generic theorem prover
@@ Property / cites work: Isabelle. A generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Q4264708
@@ Property / cites work: Q4264708 / rank @@
+Normal rank