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

@@ Property / DOI @@
-.1007/s00165-018-00476-7
@@ Property / DOI: 10.1007/s00165-018-00476-7 / 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
@@ Property / DOI @@
+.1007/S00165-018-00476-7
@@ Property / DOI: 10.1007/S00165-018-00476-7 / rank @@
+Normal rank