Tinycals: Step by Step Tacticals

DOI10.1016/j.entcs.2006.09.026zbMath1278.68253OpenAlexW2113936998WikidataQ56901946 ScholiaQ56901946MaRDI QIDQ2867943

Stefano Zacchiroli, Claudio Sacerdoti Coen, Enrico Tassi

Publication date: 20 December 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2006.09.026

zbMATH Keywords

interactive theorem provingtacticalssmall step semantics

Mathematics Subject Classification ID

Related Items

Declarative representation of proof terms, Formal metatheory of programming languages in the Matita interactive theorem prover, User interaction with the Matita proof assistant, The proof monad, The Matita Interactive Theorem Prover, Natural Deduction Environment for Matita, Implementing type theory in higher order constraint logic programming, A Tactic Language for Hiproofs

Uses Software

• Coq
• Isar
• Proof General
• Matita
• CtCoq

Cites Work

• Edinburgh LCF. A mechanized logic of computation
• The Isabelle/Naproche natural language proof assistant
• Unnamed Item
• Unnamed Item
• Unnamed Item