Middle-out reasoning for synthesis and induction (Q1915136): Difference between revisions

@@ Property / author @@
-David A. Basin
@@ Property / author: David A. Basin / rank @@
-Normal rank
@@ Property / author @@
+David A. Basin
@@ Property / author: David A. Basin / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+NQTHM
@@ Property / describes a project that uses: NQTHM / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Oyster
@@ Property / describes a project that uses: Oyster / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+InKa
@@ Property / describes a project that uses: InKa / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CLAM
@@ Property / describes a project that uses: CLAM / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Mollusc
@@ Property / describes a project that uses: Mollusc / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanizing structural induction. II: Strategies
@@ Property / cites work: Mechanizing structural induction. II: Strategies / rank @@
+Normal rank
@@ Property / cites work @@
+Q4023948
@@ Property / cites work: Q4023948 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4040283
@@ Property / cites work: Q4040283 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3804239
@@ Property / cites work: Q3804239 / rank @@
+Normal rank
@@ Property / cites work @@
+Rippling: A heuristic for guiding inductive proofs
+Normal rank
@@ Property / cites work @@
+Q3490990
@@ Property / cites work: Q3490990 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4138099
@@ Property / cites work: Q4138099 / rank @@
+Normal rank
@@ Property / cites work @@
+Logic program synthesis
@@ Property / cites work: Logic program synthesis / rank @@
+Normal rank
@@ Property / cites work @@
+Q3743300
@@ Property / cites work: Q3743300 / rank @@
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+A unification algorithm for typed \(\bar\lambda\)-calculus
+Normal rank
@@ Property / cites work @@
+Synthesis of induction orderings for existence proofs
+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 @@
+Middle-out reasoning for synthesis and induction
@@ Property / cites work: Middle-out reasoning for synthesis and induction / rank @@
+Normal rank
@@ Property / cites work @@
+Q3992908
@@ Property / cites work: Q3992908 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3328540
@@ Property / cites work: Q3328540 / rank @@
+Normal rank
@@ Property / cites work @@
+A logic programming language with lambda-abstraction, function variables, and simple unification
+Normal rank
@@ Property / cites work @@
+Lazy generation of induction hypotheses
@@ Property / cites work: Lazy generation of induction hypotheses / rank @@
+Normal rank
@@ Property / cites work @@
+Mollusc a general proof-development shell for sequent-based logics
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:1915136