A tactic language for Ergo

Andrew Martin; Ray Nickson; Mark Utting

Back

Conference paper

Peer reviewed

A tactic language for Ergo

Andrew Martin, Ray Nickson and Mark Utting

Formal Methods Pacific '97: Proceedings of the FMP '97, Springer Series in Discrete Mathematics and Theoretical Computer Science, p.186 207

Formal Methods Pacific '97: joint conference of the 6th Australasian Refinement Workshop and the 3rd New Zealand Formal Program Development Colloquium, 1997 (Wellington, New Zealand, 09-Jul-1997–11-Jul-1997)

Springer Singapore

1997

Abstract

Computer Software

Information Systems

computer programming

computer software

development

congresses

A new version of the Ergo theorem prover is under development. It uses a single tactic language, based on Angel, for tactic programming, user interface, and proof representation. This paper describes the language as it is used in each of these cases, and explains the details of its implementation in Qu-Prolog. An example from classical propositional calculus is included.

Details

Title: A tactic language for Ergo
Authors: Andrew Martin (Author)
Ray Nickson (Author)
Mark Utting (Author)
Contributors: Lindsay Groves (Editor)
Steve Reeves (Editor)
Publication details: Formal Methods Pacific '97: Proceedings of the FMP '97, Springer Series in Discrete Mathematics and Theoretical Computer Science, p.186 207
Conference details: Formal Methods Pacific '97: joint conference of the 6th Australasian Refinement Workshop and the 3rd New Zealand Formal Program Development Colloquium, 1997 (Wellington, New Zealand, 09-Jul-1997–11-Jul-1997)
Publisher: Springer Singapore
Date published: 1997
ISBN: 981308331X
Organisation Unit: School of Science and Engineering - Legacy; University of the Sunshine Coast, Queensland
Language: English
Record Identifier: 99449280902621
Output Type: Conference paper

Metrics

721 Record Views