Performing Calculation in Interactive Theorem Proving

Abstract:

Article Preview

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 et al., "Performing Calculation in Interactive Theorem Proving", Applied Mechanics and Materials, Vols. 130-134, pp. 2924-2927, 2012

Online since:

October 2011

Export:

Price:

$35.00

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

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