Three Tactic Theorem Proving

Don Syme · International Conference on Theorem Proving in Higher Order Logics · 1999

Summary

The key features of the proof description language of Declare, an experimental theorem prover for higher order logic, are described, which takes a somewhat radical approach to proof description: proofs are not described with tactics but by using just three expressive outlining constructs.

Published: 1999-09-01
Cited by: 42
References: 15
DOI: https://doi.org/10.1007/3-540-48256-3_14
Semantic Scholar: https://api.semanticscholar.org/CorpusID:18563798

References

A Tutorial Introduction to PVSJudy Crow, Sam Owre, John Rushby — 1998
Introduction to HOL: a theorem proving environment for higher order logicMike Gordon, Tom Melham — 1993
Declarative theorem proving for operational semanticsDonald Robert Syme — 1999
Isabelle: A Generic Theorem ProverLawrence C. Paulson, Tobias Nipkow — 1994
ACL2: an industrial strength version of NqthmMatt Kaufmann, J Strother Moore — 1996
A computational logic handbookR. Boyer, J. Moore — 1979
The University of CambridgeG. D. Liveing — 1897
Interaction for Declarative Theorem ProvingDon Syme — 1998
An Overview of the MIZAR ProjectP. Rudnicki — 1992
A Mizar Mode for HOLJ. Harrison — 1996

Cited by

The K combinator as a semantically transparent tagging mechanismKonrad Slind, Michael Norrish — 2002
Isabelle, Isar - a versatile environment for human readable formal proof documentsMarkus Wenzel — 2002
A comparison of the mathematical proof languages Mizar and IsarMarkus Wenzel, Freek Wiedijk, Lawrence C. Paulson — 2002
Proving as Programming with DrHOL: A Preliminary DesignScott Owens, Konrad Slind — 2003
Improving Legibility of Formal Proofs Based on the Close Reference Principle is NP-HardKarol Pąk — 2015
Algorytmy poprawy czytelności formalnych rozumowań zapisanych w systemie naturalnej dedukcjiKarol Pąk — 2013
Assertion level proof planning with compiled strategiesDominik Dietrich — 2011
A Comparison of Mizar and IsarMarkus Wenzel, Freek Wiedijk — 2003
Mizar in a NutshellAdam Grabowski, Artur Korniłowicz, Adam Naumowicz — 2010
The Racket virtual machine and randomized testingCasey Klein, Matthew Flatt, Robert Bruce Findler — 2012
Towards an Intelligent Tutor for Mathematical ProofsSerge Autexier, Dominik Dietrich, Marvin Schiller — 2012
Improving legibility of natural deduction proofs is not trivialKarol Pąk — 2014
Colouring Proofs: A Lightweight Approach to Adding Formal Structure to ProofsLaurent Théry — 2004
Recent developments in mega's proof search programming languageSerge Autexier, Dominik Dietrich — 2010
On the Macaulay inverse system and its importance for the theory of linear differential equations with constant coefficientsWolfgang Gröbner — 2010
ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First ExperimentsJosef Urban, Geoff Sutcliffe — 2008
Publication/Citation: A Proof-Theoretic Approach to Mathematical Knowledge ManagementDexter Kozen, Kamal Aboul-Hosn — 2007
An industrially effective environment for formal hardware verificationC.-J.H. Seger, Robert B. Jones, John O’Leary — 2005
Towards a Readable Formalisation of Category TheoryGreg O’Keefe — 2004
Formal Proof SketchesFreek Wiedijk, Fokkink, W. — 2003

Related papers

No related papers recorded.