1
|
基于Isabelle定理证明器算法程序的形式化验证 |
游珍
薛锦云
|
《计算机工程与科学》
CSCD
北大核心
|
2009 |
9
|
|
2
|
柯西中值定理的证明及其应用探索 |
杨雄
|
《辽宁师专学报(自然科学版)》
|
2024 |
0 |
|
3
|
基于Isabelle/HOL的文件系统形式化设计与验证 |
王文斌
钱振江
靳勇
孙高飞
邢晓双
苏超
孙天琦
|
《计算机工程》
CAS
CSCD
北大核心
|
2024 |
0 |
|
4
|
定理证明辅助工具Isabelle剖析与应用 |
郭慧梅
缪淮扣
陈怡海
|
《计算机应用与软件》
CSCD
北大核心
|
2007 |
0 |
|
5
|
约束求解与定理证明专题前言 |
蔡少伟
陈振邦
王戟
詹博华
赵永望
|
《软件学报》
EI
CSCD
北大核心
|
2023 |
0 |
|
6
|
多项式插值余项定理的一个自然证明 |
陶马成
陈松林
|
《大学数学》
|
2023 |
0 |
|
7
|
综述中学勾股定理的证明方法 |
邵恽益
|
《课堂内外(初中教研)》
|
2023 |
0 |
|
8
|
用搭积木的方法证明费马大定理没有正整数解 |
张谦
|
《爱人》
|
2023 |
0 |
|
9
|
美国和英国早期教科书中的圆幂定理 |
刘梦哲
汪晓勤
|
《中国数学教育(初中版)》
|
2024 |
0 |
|
10
|
基于Coq的RVWMO加载值公理形式化描述与推论证明 |
梁少杰
徐学政
杨德亨
黄安文
|
《智能安全》
|
2024 |
0 |
|
11
|
展方法、品文化,让经典熠熠生辉——以《勾股定理》第一课时教学为例 |
田英杰
|
《数学教学》
|
2024 |
0 |
|
12
|
算法的形式化推导与基于Isabelle的自动化验证 |
齐蕾蕾
杨庆红
游颖
|
《江西师范大学学报(自然科学版)》
CAS
北大核心
|
2018 |
2
|
|
13
|
运用定理证明器ACL2验证机器人操作系统ROS节点间通信 |
高雅
李晓娟
关永
王瑞
张杰
魏洪兴
|
《小型微型计算机系统》
CSCD
北大核心
|
2014 |
12
|
|
14
|
运用定理证明的形式化方法验证SpaceWire编码电路 |
李黎明
关永
吴敏华
张杰
施智平
|
《小型微型计算机系统》
CSCD
北大核心
|
2012 |
10
|
|
15
|
几何定理可读证明的自动生成 |
张景中
杨路
高小山
周咸青
|
《计算机学报》
EI
CSCD
北大核心
|
1995 |
22
|
|
16
|
一种新的基于扩展规则的定理证明算法 |
孙吉贵
李莹
朱兴军
吕帅
|
《计算机研究与发展》
EI
CSCD
北大核心
|
2009 |
17
|
|
17
|
机械化定理证明研究综述 |
江南
李清安
汪吕蒙
张晓瞳
何炎祥
|
《软件学报》
EI
CSCD
北大核心
|
2020 |
6
|
|
18
|
多项式等式型几何定理的可读证明 |
江建国
张景中
王晓京
|
《计算机学报》
EI
CSCD
北大核心
|
2008 |
6
|
|
19
|
文件比较算法fcomp在Isabelle/HOL中的验证 |
宋丽华
王海涛
季晓君
张兴元
|
《软件学报》
EI
CSCD
北大核心
|
2017 |
1
|
|
20
|
一阶谓词演算定理机器证明的余式方法 |
吴尽昭
刘卓军
|
《计算机学报》
EI
CSCD
北大核心
|
1996 |
7
|
|