Tactics for hierarchical proof
type: Item
instance of: scholarly article
title: Tactics for hierarchical proof
zbMATH Open document ID: 1205.68359
author: D. Aspinall
author: Ewen Denney
author: Christoph Lüth
published in: Mathematics in Computer Science
publication date: 2011-02-19T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5853498
zbMATH Keywords: hierarchical proof
zbMATH Keywords: hiproof
zbMATH Keywords: tactical theorem proving
describes a project that uses: Proof General
describes a project that uses: ArcAngel
describes a project that uses: Isar
describes a project that uses: Matita
describes a project that uses: OMDoc
describes a project that uses: HOL
describes a project that uses: LOUI
MaRDI profile type: Publication
full work available at URL: s11786-010-0025-6
OpenAlex ID: W2030178956
cites work: A Proof-Theoretic Approach to Tactics
cites work: Innovations in computational type theory using Nuprl
cites work: Dependent types ensure partial correctness of theorem provers
cites work: User interaction with the Matita proof assistant
cites work: Q2729065
cites work: Q2767010
cites work: Hiproofs: a hierarchical notion of proof tree
cites work: Implementing tactics and tacticals in a higher-order logic programming language
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Towards Self-verification of HOL Light
cites work: PVS\#: streamlined tacticals for PVS
cites work: A tactic calculus. --- Abridged version
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: ArcAngel: a tactic language for refinement
cites work: A pragmatic approach to reuse in tactical theorem proving
cites work: Computer supported mathematics with \(\Omega\)MEGA
cites work: A Brief Overview of HOL4
cites work: \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems
DOI: 10.1007/S11786-010-0025-6
description: scientific article; zbMATH DE number 5853498