Automating Event-B invariant proofs by rippling and proof patching (Q667526): Difference between revisions

@@ Property / describes a project that uses @@
+IsaCoSy
@@ Property / describes a project that uses: IsaCoSy / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ProofPower
@@ Property / describes a project that uses: ProofPower / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Z
@@ Property / describes a project that uses: Z / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s00165-018-00476-7
+Normal rank
@@ Property / OpenAlex ID @@
+W2908173533
@@ Property / OpenAlex ID: W2908173533 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q113906136
@@ Property / Wikidata QID: Q113906136 / rank @@
+Normal rank
@@ Property / cites work @@
+The B-Book
@@ Property / cites work: The B-Book / rank @@
+Normal rank
@@ Property / cites work @@
+Q3569584
@@ Property / cites work: Q3569584 / rank @@
+Normal rank
@@ Property / cites work @@
+Rippling: Meta-Level Guidance for Mathematical Reasoning
+Normal rank
@@ Property / cites work @@
+Q3838801
@@ Property / cites work: Q3838801 / rank @@
+Normal rank
@@ Property / cites work @@
+A Graphical Language for Proof Strategies
@@ Property / cites work: A Graphical Language for Proof Strategies / rank @@
+Normal rank
@@ Property / cites work @@
+Proof-Pattern Recognition and Lemma Discovery in ACL2
+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 @@
+Reasoned modelling critics: turning failed proofs into modelling guidance
+Normal rank
@@ Property / cites work @@
+Conjecture synthesis for inductive theories
@@ Property / cites work: Conjecture synthesis for inductive theories / rank @@
+Normal rank
@@ Property / cites work @@
+Q3997074
@@ Property / cites work: Q3997074 / rank @@
+Normal rank
@@ Property / cites work @@
+Hipster: Integrating Theory Exploration in a Proof Assistant
+Normal rank
@@ Property / cites work @@
+Q3992808
@@ Property / cites work: Q3992808 / 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 @@
+Q4301167
@@ Property / cites work: Q4301167 / rank @@
+Normal rank