Automating change of representation for proofs in discrete mathematics (extended version) (Q2364883): Difference between revisions

@@ Property / DOI @@
-.1007/s11786-016-0275-z
@@ Property / DOI: 10.1007/s11786-016-0275-z / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+Hets
@@ Property / describes a project that uses: Hets / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+IMPS
@@ Property / describes a project that uses: IMPS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nitpick
@@ Property / describes a project that uses: Nitpick / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Sledgehammer
@@ Property / describes a project that uses: Sledgehammer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Transfer
@@ Property / describes a project that uses: Transfer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Lifting
@@ Property / describes a project that uses: Lifting / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+Publication
@@ Property / MaRDI profile type: Publication / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s11786-016-0275-z
+Normal rank
@@ Property / OpenAlex ID @@
+W2417291013
@@ Property / OpenAlex ID: W2417291013 / rank @@
+Normal rank
@@ Property / cites work @@
+Interpretation of Locales in Isabelle: Theories and Proof Contexts
+Normal rank
@@ Property / cites work @@
+Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
+Normal rank
@@ Property / cites work @@
+Sledgehammer: Judgement Day
@@ Property / cites work: Sledgehammer: Judgement Day / rank @@
+Normal rank
@@ Property / cites work @@
+Q3065693
@@ Property / cites work: Q3065693 / rank @@
+Normal rank
@@ Property / cites work @@
+The New Quickcheck for Isabelle
@@ Property / cites work: The New Quickcheck for Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+Using tactics to reformulate formulae for resolution theorem proving
+Normal rank
@@ Property / cites work @@
+IMPS: An interactive mathematical proof system
@@ Property / cites work: IMPS: An interactive mathematical proof system / rank @@
+Normal rank
@@ Property / cites work @@
+Institutions: abstract model theory for specification and programming
+Normal rank
@@ Property / cites work @@
+Data Refinement in Isabelle/HOL
@@ Property / cites work: Data Refinement in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Constructive Type Classes in Isabelle
@@ Property / cites work: Constructive Type Classes in Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+HOL with Definitions: Semantics, Soundness, and a Verified Implementation
+Normal rank
@@ Property / cites work @@
+A Consistent Foundation for Isabelle/HOL
@@ Property / cites work: A Consistent Foundation for Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Translating higher-order clauses to first-order clauses
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q3075239
@@ Property / cites work: Q3075239 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2755077
@@ Property / cites work: Q2755077 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q59474485
@@ Property / Wikidata QID: Q59474485 / rank @@
+Normal rank
@@ Property / DOI @@
+.1007/S11786-016-0275-Z
@@ Property / DOI: 10.1007/S11786-016-0275-Z / rank @@
+Normal rank