Using a generalisation critic to find bisimulations for coinductive proofs (Q5234712): Difference between revisions

@@ Property / cites work @@
+Q4264732
@@ Property / cites work: Q4264732 / rank @@
+Normal rank
@@ Property / cites work @@
+Implicit induction in conditional theories
@@ Property / cites work: Implicit induction in conditional theories / rank @@
+Normal rank
@@ Property / cites work @@
+Q3804239
@@ Property / cites work: Q3804239 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated deduction -- CADE-12. 12th international conference, Nancy, France, June 26 -- July 1, 1994. Proceedings
+Normal rank
@@ Property / cites work @@
+Using a generalisation critic to find bisimulations for coinductive proofs
+Normal rank
@@ Property / cites work @@
+Q4222760
@@ Property / cites work: Q4222760 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3204055
@@ Property / cites work: Q3204055 / rank @@
+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 @@
+Q3992568
@@ Property / cites work: Q3992568 / rank @@
+Normal rank
@@ Property / cites work @@
+Co-induction in relational semantics
@@ Property / cites work: Co-induction in relational semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Circuits as streams in Coq: Verification of a sequential multiplier
+Normal rank
@@ Property / cites work @@
+A fixedpoint approach to implementing (Co)inductive definitions
+Normal rank
@@ Property / cites work @@
+A co-induction principle for recursively defined domains
+Normal rank
@@ Property / cites work @@
+A lattice-theoretical fixpoint theorem and its applications
+Normal rank
@@ Property / cites work @@
+A divergence critic
@@ Property / cites work: A divergence critic / rank @@
+Normal rank
@@ Property / cites work @@
+Q3790597
@@ Property / cites work: Q3790597 / rank @@
+Normal rank