A proof-centric approach to mathematical assistants
From MaRDI portal
Publication:865648
DOI10.1016/j.jal.2005.10.007zbMath1107.68096MaRDI 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
Uses Software
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