Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

CADE

1990

Springer

1990

Springer

imps is an Interactive Mathematical Proof System intended as a general purpose tool for formulating and applying mathematics in a familiar fashion. The logic of imps is based on a version of simple type theory with partial functions and subtypes. Mathematical specification and inference are performed relative to axiomatic theories, which can be related to one another via inclusion and theory interpretation. imps provides relatively large primitive inference steps to facilitate human control of the deductive process and human comprehension of the resulting proofs. An initial theory library containing almost a thousand repeatable proofs covers significant portions of logic, algebra and analysis, and provides some support for modeling applications in computer science. Key Words: interactive theorem proving, automated analysis, computing with theorems, theory interpretation, higher-order logic, partial functions Supported by the MITRE-Sponsored Research program. Published in Journal of A...

Related Content

Added |
10 Aug 2010 |

Updated |
10 Aug 2010 |

Type |
Conference |

Year |
1990 |

Where |
CADE |

Authors |
William M. Farmer, Joshua D. Guttman, F. Javier Thayer |

Comments (0)