Paper Title:
Performing Calculation in Interactive Theorem Proving
  Abstract

An LCF style tactic can be used to verify that the conclusion is a logical consequence of the premises, however, in mathematical practice, we often construct a conclusion in a proof step. This paper proposes a calculational style of tactic, and illustrates the characteristic and the realization issues of the tactics on the top of a theorem prover.

  Info
Periodical
Edited by
Han Zhao
Pages
2924-2927
DOI
10.4028/www.scientific.net/AMM.130-134.2924
Citation
B. Li, C. Y. Zhao, L. Li, "Performing Calculation in Interactive Theorem Proving", Applied Mechanics and Materials, Vols. 130-134, pp. 2924-2927, 2012
Online since
October 2011
Export
Price
$32.00
Share

In order to see related information, you need to Login.

In order to see related information, you need to Login.

Authors: Wei Gong, Jun Wei Jia
Chapter 4: Information Technologies in Manufacturing
Abstract:Model Checking is a method for verification. The model will be checked until the specification of it is proved or disproved. With the rising...
181
Authors: Yan Li, Zhi Run Xiao
Chapter 7: Production Management
Abstract:The problem of multi-skilled project scheduling (MSPSP) is a complex problem of task scheduling and resource assignment that comes up in the...
265
Authors: You Liang Fu, Da Hang Zhang
Chapter 9: Signal and Image, Video Processing, Data Mining and Acquisition, Computational Mathematics and Algorithms
Abstract:A class of shallow water waves equations are studied in this paper. Using Kato's existence theorem, we mainly study the initial and bounded...
753