Automating Change of Representation for Proofs in Discrete Mathematics

DOI10.1007/978-3-319-20615-8_15zbMath1409.68260arXiv1505.02449OpenAlexW228754674MaRDI QIDQ3453117

Daniel Raggi, Alison Pease, Gudmund Grov, Alan Bundy

Publication date: 20 November 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1505.02449

zbMATH Keywords

automated reasoningtransformationIsabelle proof assistantchange of representation

Mathematics Subject Classification ID

General topics of discrete mathematics in relation to computer science (68R01) Logic in artificial intelligence (68T27) Knowledge representation (68T30)

Related Items (1)

A new compact finite difference quasilinearization method for nonlinear evolution partial differential equations

Uses Software

• Isabelle
• Nitpick
• Isabelle/HOL
• Hets
• Sledgehammer
• IMPS
• Transfer
• Lifting

Cites Work

• Unnamed Item
• IMPS: An interactive mathematical proof system
• Isabelle/HOL. A proof assistant for higher-order logic
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Institutions: abstract model theory for specification and programming
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder

This page was built for publication: Automating Change of Representation for Proofs in Discrete Mathematics