Performing Calculation in Interactive Theorem Proving

Bing Li; Chen Yang Zhao; Lian Li

doi:10.4028/www.scientific.net/AMM.130-134.2924

Paper Titles

Research on Cipher Coprocessor Instruction Level Parallelism Compiler
p.2907

A New Image Affine-Invariant Region Detector and Descriptor
p.2911

Dimension-Descending Algorithm for Spherical Delaunay Triangulation
p.2915

Ergonomics Evaluation of Mobile Maintenance Shelter with Fuzzy AHP Method
p.2920

Performing Calculation in Interactive Theorem Proving
p.2924

Image Digital Watermarking Algorithm Based on Arnold Scrambling and Wavelet Transform
p.2928

Adaptive Image Denoising Based on Sparse Decomposition
p.2932

A New Phase Noise and Channel Estimate Method in CO-OFDM System
p.2936

Interference Suppression Detection Algorithms in STBC-MIMO Systems
p.2940

HomeApplied Mechanics and MaterialsApplied Mechanics and Materials Vols. 130-134Performing Calculation in Interactive Theorem...

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.

You might also be interested in these eBooks

Mechanical and Electronics Engineering III

View Preview

Info:

Periodical:

Applied Mechanics and Materials (Volumes 130-134)

Pages:

2924-2927

DOI:

https://doi.org/10.4028/www.scientific.net/AMM.130-134.2924

Citation:

Cite this paper

Online since:

October 2011

Authors:

Bing Li, Chen Yang Zhao, Lian Li

Keywords:

Computational Model, Interactive Theorem Proving, Isabelle/HOL, Symbolic Calculation

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

References

[1] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, colume 828 of Lecture Nodes in Computer Science. Spring Verlag, (1994).

Google Scholar

[2] Buchberger, B. The Theorema Project: A Progress Report. In Kerber,M. and Kohlhase, M. (eds. ), Symbolic Computation and Automated Reasoning, 2000, A.K. Peters, Natick, p.98–113.

Google Scholar

[3] S. Buswell et al. The OpenMath Standard, version 2. 0, (2002).

Google Scholar

[4] V. Sorge. Non-trivial symbolic computations in proof planning. In FroCoS '00: Proceedings of the Third International Workshop on Frontiers of Combining Systems, London, UK, 2000. Springer-Verlag, p.121–135.

DOI: 10.1007/10720084_9

Google Scholar

[5] Kaliszyk, C. & Wiedijk, F. Certified computer algebra on top of an interactive theorem prover. In J.G. Carbonell & J. Siekmann (eds), Towards Mechanized Mathematical Assistants, Lecture Notes in Computer Science, Vol. 4573, Heidelberg: Springer-Verlag, 2007, pp.94-105.

DOI: 10.1007/978-3-540-73086-6_8

Google Scholar

[6] Aracne. Tim Sheard. Putting Curry-Howard to work. In Proceedings of ACM Workshop on Haskell, Tallinn, Tallinn, Estonia, September 2005. ACM, p.74–85.

DOI: 10.1145/1088348.1088356

Google Scholar

[7] P. Letouzey. Extraction in coq: An overview. In CiE'08, volume 5028 of LNCS. Springer, 2008, p.359–369.

Google Scholar

[8] Davis, R. Sigal and EJ Weyuker, Computability, Complexity, and Languages: Fundamentals of Theoretical Computer Science (second ed. ), Academic Press, San Diego, CA, (1994).

DOI: 10.2307/2275691

Google Scholar