Iscalc: An Interactive Symbolic Computation Framework (System Description)

被引：0

作者：

Zhan, Bohua ^{[1
,2
]}

Fan, Yuheng ^{[3
]}

Xiong, Weiqiang ^{[2
]}

Xu, Runqing ^{[1
]}

机构：

[1] Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing, Peoples R China

[2] Univ Chinese Acad Sci, Beijing, Peoples R China

[3] Natl Comp Syst Engn Res Inst China, Beijing, Peoples R China

来源：

AUTOMATED DEDUCTION, CADE 29 | 2023年 / 14132卷

基金：

中国国家自然科学基金;

关键词：

Symbolic computation; User interface; Computer algebra; PROVER;

D O I：

10.1007/978-3-031-38499-8_33

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

The need to verify symbolic computation arises in diverse application areas. In this paper, based on earlier work on verifying computation of definite integrals in HolPy, we present a tool Iscalc for performing a variety of symbolic computations interactively, taking a middle ground in terms of easy of use and rigor between computer algebra systems and interactive theorem provers. The tool supports user-level definitions and dependency among computations, allowing construction and reuse of custom theories. Side conditions are checked on a best-effort basis. The tool is applied to highly non-trivial computations from the textbook Inside Interesting Integrals.

引用

页码：577 / 589

页数：13

共 19 条

[1] MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions [J].

Akbarpour, Behzad ;

Paulson, Lawrence Charles .

JOURNAL OF AUTOMATED REASONING, 2010, 44 (03) :175-205

[2]

Astr om K. J., 2008, Feedback Systems: An Introduction for Scientists and Engineers

[3] A Heuristic Prover for Real Inequalities [J].

Avigad, Jeremy ;

Lewis, Robert Y. ;

Roux, Cody .

JOURNAL OF AUTOMATED REASONING, 2016, 56 (03) :367-386

[4] Analytics - An experiment in combining theorem proving and symbolic computation [J].

Bauer, A ;

Clarke, E ;

Zhao, XD .

JOURNAL OF AUTOMATED REASONING, 1998, 21 (03) :295-325

[5]

Bohua Zhan, 2019, Formal Methods and Software Engineering. 21st International Conference on Formal Engineering Methods, ICFEM 2019. Proceedings. Lecture Notes in Computer Science (LNCS 11852), P86, DOI 10.1007/978-3-030-32409-4_6

[6] Formalization of real analysis: a survey of proof assistants and libraries [J].

Boldo, Sylvie ;

Lelay, Catherine ;

Melquiond, Guillaume .

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2016, 26 (07) :1196-1233

[7] The Lean 4 Theorem Prover and Programming Language [J].

de Moura, Leonardo ;

Ullrich, Sebastian .

AUTOMATED DEDUCTION, CADE 28, 2021, 12699 :625-635

[8] A Drag-and-Drop Proof Tactic [J].

Donato, Pablo ;

Strub, Pierre-Yves ;

Werner, Benjamin .

PROCEEDINGS OF THE 11TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP '22), 2022, :197-209

[9] Verified Real Asymptotics in Isabelle/HOL [J].

Eberl, Manuel .

PROCEEDINGS OF THE 2019 ACM INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION (ISSAC '19), 2019, :147-154

[10] Automated and readable simplification of trigonometric expressions [J].

Fu, Hongguang ;

Zhong, Xiuqin ;

Zeng, Zhenbing .

MATHEMATICAL AND COMPUTER MODELLING, 2006, 44 (11-12) :1169-1177

← 1 2 →