Tinycals: Step by Step Tacticals

Claudio Sacerdoti Coen; Enrico Tassi; Stefano Zacchiroli

doi:10.1016/j.entcs.2006.09.026

Tinycals: Step by Step Tacticals

Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli

University of Bologna

Research output: Contribution to journal › Article › peer-review

Abstract

Most of the state-of-the-art proof assistants are based on procedural proof languages, scripts, and rely on LCF tacticals as the primary tool for tactics composition. In this paper we discuss how these ingredients do not interact well with user interfaces based on the same interaction paradigm of Proof General (the de facto standard in this field), identifying in the coarse-grainedness of tactical evaluation the key problem. We propose Tinycals as an alternative to a subset of LCF tacticals, showing that the user does not experience the same problem if tacticals are evaluated in a more fine-grained manner. We present the formal operational semantics of tinycals as well as their implementation in the Matita proof assistant.

Original language	English
Pages (from-to)	125-142
Number of pages	18
Journal	Electronic Notes in Theoretical Computer Science
Volume	174
Issue number	2
DOIs	https://doi.org/10.1016/j.entcs.2006.09.026
Publication status	Published - 15 May 2007
Externally published	Yes

Keywords

Interactive Theorem Proving
Small Step Semantics
Tacticals

Access to Document

10.1016/j.entcs.2006.09.026

Cite this

@article{db25f962dc4447ad8c053b99182f64a4,

title = "Tinycals: Step by Step Tacticals",

abstract = "Most of the state-of-the-art proof assistants are based on procedural proof languages, scripts, and rely on LCF tacticals as the primary tool for tactics composition. In this paper we discuss how these ingredients do not interact well with user interfaces based on the same interaction paradigm of Proof General (the de facto standard in this field), identifying in the coarse-grainedness of tactical evaluation the key problem. We propose Tinycals as an alternative to a subset of LCF tacticals, showing that the user does not experience the same problem if tacticals are evaluated in a more fine-grained manner. We present the formal operational semantics of tinycals as well as their implementation in the Matita proof assistant.",

keywords = "Interactive Theorem Proving, Small Step Semantics, Tacticals",

author = "Coen, \{Claudio Sacerdoti\} and Enrico Tassi and Stefano Zacchiroli",

year = "2007",

month = may,

day = "15",

doi = "10.1016/j.entcs.2006.09.026",

language = "English",

volume = "174",

pages = "125--142",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

number = "2",

}

TY - JOUR

T1 - Tinycals

T2 - Step by Step Tacticals

AU - Coen, Claudio Sacerdoti

AU - Tassi, Enrico

AU - Zacchiroli, Stefano

PY - 2007/5/15

Y1 - 2007/5/15

N2 - Most of the state-of-the-art proof assistants are based on procedural proof languages, scripts, and rely on LCF tacticals as the primary tool for tactics composition. In this paper we discuss how these ingredients do not interact well with user interfaces based on the same interaction paradigm of Proof General (the de facto standard in this field), identifying in the coarse-grainedness of tactical evaluation the key problem. We propose Tinycals as an alternative to a subset of LCF tacticals, showing that the user does not experience the same problem if tacticals are evaluated in a more fine-grained manner. We present the formal operational semantics of tinycals as well as their implementation in the Matita proof assistant.

AB - Most of the state-of-the-art proof assistants are based on procedural proof languages, scripts, and rely on LCF tacticals as the primary tool for tactics composition. In this paper we discuss how these ingredients do not interact well with user interfaces based on the same interaction paradigm of Proof General (the de facto standard in this field), identifying in the coarse-grainedness of tactical evaluation the key problem. We propose Tinycals as an alternative to a subset of LCF tacticals, showing that the user does not experience the same problem if tacticals are evaluated in a more fine-grained manner. We present the formal operational semantics of tinycals as well as their implementation in the Matita proof assistant.

KW - Interactive Theorem Proving

KW - Small Step Semantics

KW - Tacticals

U2 - 10.1016/j.entcs.2006.09.026

DO - 10.1016/j.entcs.2006.09.026

M3 - Article

AN - SCOPUS:34247881880

SN - 1571-0661

VL - 174

SP - 125

EP - 142

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 2

ER -

Tinycals: Step by Step Tacticals

Abstract

Keywords

Access to Document

Fingerprint

Cite this