Theorem proving based on proof scores for rewrite theory specifications of OTSs

被引：6

作者：

Ogata, Kazuhiro ^{[1
]}

Futatsugi, Kokichi ^{[1
]}

机构：

[1] School of Information Science, JAIST, Japan

来源：

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | 2014年 / 8373卷

基金：

日本学术振兴会;

关键词：

Theorem proving - Model checking;

D O I：

10.1007/978-3-642-54624-2_31

中图分类号：

学科分类号：

摘要：

引用

页码：630 / 656

共 50 条

[1] REWRITE METHOD FOR THEOREM-PROVING IN 1ST ORDER THEORY WITH EQUALITY
HSIANG, J
JOURNAL OF SYMBOLIC COMPUTATION, 1987, 3 (1-2) : 133 - 151
[2] Inductive Theorem Proving for Design Specifications
J Symb Comput, 1 (41):
[3] Inductive theorem proving for design specifications
Padawitz, P
JOURNAL OF SYMBOLIC COMPUTATION, 1996, 21 (01) : 41 - 99
[4] UNIT PROOF AND INPUT PROOF IN THEOREM PROVING
CHANG, CL
JOURNAL OF THE ACM, 1970, 17 (04) : 698 - &
[5] Inductive theorem proving in hierarchical conditional specifications
Avenhaus, J
Madlener, K
MODELS, ALGEBRAS, AND PROOFS, 1999, 203 : 337 - 371
[6] Proving and Disproving Assertion Rewrite Rules with Automated Theorem Provers
Morin-Allory, Katell
Boule, Marc
Borrione, Dominique
Zilic, Zeljko
HLDVT: 2008 IEEE INTERNATIONAL HIGH LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS, 2008, : 56 - +
[7] ON THE USE OF CONDITIONAL REWRITE RULES IN INDUCTIVE THEOREM-PROVING
FRIBOURG, L
LECTURE NOTES IN COMPUTER SCIENCE, 1988, 308 : 56 - 61
[8] Proof simplification and automated theorem proving
Kinyon, Michael
PHILOSOPHICAL TRANSACTIONS OF THE ROYAL SOCIETY A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES, 2019, 377 (2140):
[9] Verifying specifications with proof scores in CafeOBJ
Futatsugi, Kokichi
ASE 2006: 21ST IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2006, : 3 - 10
[10] REWRITE METHODS FOR CLAUSAL AND NON-CLAUSAL THEOREM-PROVING
HSIANG, J
DERSHOWITZ, N
LECTURE NOTES IN COMPUTER SCIENCE, 1983, 154 : 331 - 346

← 1 2 3 4 5 →