Tactics for hierarchical proof

DOI10.1007/s11786-010-0025-6zbMath1205.68359OpenAlexW2030178956MaRDI QIDQ626933

Ewen Denney, Christoph Lüth, David Aspinall

Publication date: 19 February 2011

Published in: Mathematics in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11786-010-0025-6

zbMATH Keywords

hierarchical proofhiprooftactical theorem proving

Mathematics Subject Classification ID

Related Items (2)

Interleaving Strategies ⋮ Towards Formal Proof Script Refactoring

Uses Software

• ArcAngel
• Isar
• Proof General
• HOL
• Matita
• OMDoc
• LOUI

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• ArcAngel: a tactic language for refinement
• Innovations in computational type theory using Nuprl
• Computer supported mathematics with \(\Omega\)MEGA
• Implementing tactics and tacticals in a higher-order logic programming language
• Isabelle/HOL. A proof assistant for higher-order logic
• Edinburgh LCF. A mechanized logic of computation
• A tactic calculus. --- Abridged version
• User interaction with the Matita proof assistant
• A Pragmatic Approach to Reuse in Tactical Theorem Proving
• PVS#: Streamlined Tacticals for PVS
• PlatΩ: A Mediator between Text-Editors and Proof Assistance Systems
• A Brief Overview of HOL4
• Towards Self-verification of HOL Light
• Dependent types ensure partial correctness of theorem provers
• A Proof-Theoretic Approach to Tactics

This page was built for publication: Tactics for hierarchical proof