Declarative representation of proof terms

DOI10.1007/s10817-009-9136-7zbMath1185.68633OpenAlexW2004639559MaRDI QIDQ2655330

Claudio Sacerdoti Coen

Publication date: 25 January 2010

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-009-9136-7

zbMATH Keywords

translationgenerationdeclarative languageproof terms

Mathematics Subject Classification ID

Related Items (1)

The Matita Interactive Theorem Prover

Uses Software

• Coq
• Isar
• Mizar
• Matita
• PhoX

Cites Work

• Unnamed Item
• A comparison of Mizar and Isar
• User interaction with the Matita proof assistant
• Procedural representation of CIC proof terms
• Tinycals: Step by Step Tacticals
• The duality of computation
• A Declarative Language for the Coq Proof Assistant
• An Interactive Driver for Goal-directed Proof Strategies
• A Formal Correspondence Between OMDoc with Alternative Proofs and the ${\overline{\lambda}\mu\tilde{\mu}}$ -Calculus
• Mathematical Knowledge Management

This page was built for publication: Declarative representation of proof terms