Introduction to ``Milestones in interactive theorem proving

DOI10.1007/s10817-018-9465-5zbMath1398.00118OpenAlexW2801537935WikidataQ57382527 ScholiaQ57382527MaRDI QIDQ1663212

No author found.

Publication date: 21 August 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://research.vu.nl/ws/files/118674118/Avigad2018_IntroductionToMilestonesInInteractiveTheoremProving.pdf

Mathematics Subject Classification ID

Related Items (1)

A proof system for graph (non)-isomorphism verification

Uses Software

• Nitpick
• Isabelle/HOL
• PIDE
• Isabelle/jEdit
• Sledgehammer
• CakeML
• Flyspeck
• Locales
• seL4
• Tame Graphs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Intelligent computer mathematics. 11th international conference, AISC 2012, 19th symposium, Calculemus 2012, 5th international workshop, DML 2012, 11th international conference, MKM 2012, systems and projects, held as part of CICM 2012, Bremen, Germany, July 8--13, 2012. Proceedings
• Linear quantifier elimination
• Term rewriting and beyond -- theorem proving in Isabelle
• Verified software: Theories, tools, experiments. Second international conference, VSTTE 2008, Toronto, Canada, October 6--9, 2008. Proceedings
• Unification in Boolean rings
• Winskel is (almost) right: Towards a mechanized semantics textbook
• Boolean unification - the story so far
• Equational reasoning in Isabelle
• A verified compiler from Isabelle/HOL to CakeML
• Concrete Semantics
• Unification in primal algebras, their powers and their varieties
• Flyspeck I: Tame Graphs
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Hoare logic for Java in Isabelle/HOL
• Term Rewriting and All That
• Modular higher-order E-unification
• Logic for Programming, Artificial Intelligence, and Reasoning
• Types for Proofs and Programs
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
• Sledgehammer: Judgement Day
• Higher-order unification, polymorphism, and subsorts

This page was built for publication: Introduction to ``Milestones in interactive theorem proving