A proof-centric approach to mathematical assistants

DOI10.1016/j.jal.2005.10.007zbMath1107.68096OpenAlexW2099924673MaRDI QIDQ865648

Lucas Dixon, Jacques D. Fleuriot

Publication date: 20 February 2007

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://www.pure.ed.ac.uk/ws/files/22995251/1_s2.0_S1570868305000728_main.pdf

zbMATH Keywords

theorem provingproof assistantIsabelleproof planningIsaPlannerIsar

Mathematics Subject Classification ID

Related Items

Crystal: Integrating structured queries into a tactic language ⋮ Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit

Uses Software

• Coq
• Isabelle
• TPS
• ML
• IsaPlanner
• Isar
• Mizar
• IsaWin
• TAS
• Proof General
• TeXmacs
• HOL
• Nuprl
• Lambda-Clam

Cites Work

• A theory of type polymorphism in programming
• Isabelle. A generic theorem prover
• Productive use of failure in inductive proof
• TPS: A theorem-proving system for classical type theory
• Formalizing Hilbert’s Grundlagen in Isabelle/Isar
• The Zipper
• Automated Reasoning
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• The Principal Type-Scheme of an Object in Combinatory Logic
• Types for Proofs and Programs
• Types for Proofs and Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item