小型微型计算机系统
小型微型計算機繫統
소형미형계산궤계통
MINI-MICRO SYSTEMS
2011年
6期
1175-1180
,共6页
杨思敏%李兆鹏%庄重%张臻婷
楊思敏%李兆鵬%莊重%張臻婷
양사민%리조붕%장중%장진정
证明生成%自动定理证明%整数定理证明%出具证明编译器
證明生成%自動定理證明%整數定理證明%齣具證明編譯器
증명생성%자동정리증명%정수정리증명%출구증명편역기
近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译器至关重要.本文基于Simplex算法在出具证明编译器的框架内设计并实现了一个支持线性整数命题求解的自动定理证明器,并且提出一套证明项构造方法,将其应用于自动定理证明器中可生成Coq可检查的证明.
近年來,齣具證明編譯器作為構建高可信軟件的重要途徑,逐漸成為編譯器理論和形式化驗證的研究熱點.在其理論框架中,編譯器需要藉助自動定理證明技術,自動地證明驗證條件併生成機器可檢查的證明項,因此好的自動定理證明器對齣具證明編譯器至關重要.本文基于Simplex算法在齣具證明編譯器的框架內設計併實現瞭一箇支持線性整數命題求解的自動定理證明器,併且提齣一套證明項構造方法,將其應用于自動定理證明器中可生成Coq可檢查的證明.
근년래,출구증명편역기작위구건고가신연건적중요도경,축점성위편역기이론화형식화험증적연구열점.재기이론광가중,편역기수요차조자동정리증명기술,자동지증명험증조건병생성궤기가검사적증명항,인차호적자동정리증명기대출구증명편역기지관중요.본문기우Simplex산법재출구증명편역기적광가내설계병실현료일개지지선성정수명제구해적자동정리증명기,병차제출일투증명항구조방법,장기응용우자동정리증명기중가생성Coq가검사적증명.
