Automating change of representation for proofs in discrete mathematics (extended version)
From MaRDI portal
Publication:2364883
DOI10.1007/S11786-016-0275-ZzbMATH Open1409.68261OpenAlexW2417291013WikidataQ59474485 ScholiaQ59474485MaRDI QIDQ2364883FDOQ2364883
Recommendations
Cites work
- A consistent foundation for Isabelle/HOL
- A course in combinatorics.
- A new look at generalized rewriting in type theory
- A walk through combinatorics. An introduction to enumeration and graph theory
- Constructive Type Classes in Isabelle
- Data refinement in Isabelle/HOL
- HOL with definitions: semantics, soundness, and a verified implementation
- IMPS: An interactive mathematical proof system
- Institutions: abstract model theory for specification and programming
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Isabelle/HOL. A proof assistant for higher-order logic
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- Sledgehammer: judgement day
- The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
- Translating higher-order clauses to first-order clauses
- Using tactics to reformulate formulae for resolution theorem proving
Cited in
(4)- Automating Change of Representation for Proofs in Discrete Mathematics
- scientific article; zbMATH DE number 2085174 (Why is no real title available?)
- Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
- Changing data representation within the \textsf{Coq} system
Describes a project that uses
Uses Software
This page was built for publication: Automating change of representation for proofs in discrete mathematics (extended version)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2364883)
