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

@@ Property / describes a project that uses @@
+CLAM
@@ Property / describes a project that uses: CLAM / 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 @@
+Isabelle/ZF
@@ Property / describes a project that uses: Isabelle/ZF / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+Publication
@@ Property / MaRDI profile type: Publication / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W1541732450
@@ Property / OpenAlex ID: W1541732450 / rank @@
+Normal rank
@@ 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
@@ Property / cites work @@
+The OYSTER-CLAM system
@@ Property / cites work: The OYSTER-CLAM system / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:5234712