Zobrazeno 1 - 10 of 19 pro vyhledávání: '"定理証明"'
1
CoqとIsabelle を用いたユークリッド原論の定理証明
Autor: Fumiya, IWAMA, Tadashi, TAKAHASHI
Publikováno v: 甲南大学教育学習支援センター紀要 = Memoirs of Learning Utility Center for Konan University Students. 5:1-16
ソフトウェアを用いて数学の定理の証明を行うことについては，多くのソフトウェアが開発されている。本研究では，定理証明ソフトウェアCoq とIsabelle を用いてユークリッド原論の定理
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=jairo_______::20313b7643fcc687281e86d38c82f22b
http://id.nii.ac.jp/1260/00003612/
Zobrazit plný text záznamu
5
UMLによるプロテクションプロファイルのモデル化とその形式的検証
Publikováno v: 電子情報通信学会論文誌. D, 情報・システム. (4):726-742
プロテクションプロファイルは，様々な情報システムにおけるセキュリティ仕様書の雛形であり， ISO/IEC15408という国際基準によりセキュリティが保証されている．しかしながら，扱う分
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=jairo_______::26cf7e04747a987895af48ae2647ab52
http://id.nii.ac.jp/1586/00013084/
Zobrazit plný text záznamu
6
On Improvements of a SAT-Solver PCMGTP on FPGA
Publikováno v: 九州大学大学院システム情報科学紀要. 10(1):21-26
In this paper, an improved design of a SAT-solver PCMGTP on FPGA is described. The previous implementation of PCMGTP achieved considerable speedup of SAT-solving compared to the software counterpart of MGTP. After intensive analyses and experiments,
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=jairo_______::f57cbd28ce8e29c99caf8090512e6541
http://hdl.handle.net/2324/1516056
Zobrazit plný text záznamu
7
定理証明系PCMGTPのFPGA上の実装について
Publikováno v: 九州大学大学院システム情報科学紀要. 9(1):13-18
In this paper, a design and implementation of theorem prover PCMGTP on an FPGA chip is described. PCMGTP is based on a model-generation method which is sound and complete to decide satisfiability of a set of clauses of propositional logic. Given a se
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=jairo_______::ea2422bbf85d8a00f405ff1a6dba2452
http://hdl.handle.net/2324/1515920
Zobrazit plný text záznamu
8
二分決定グラフによるモデル生成木の刈込み
Publikováno v: 九州大学大学院システム情報科学紀要. 8(1):49-54
Binary Decision Diagram(BDD) is a data structure that expresses Boolean expressions on computers. We can effectively manipulate Boolean expressions and determine their satisfiability with BDDs. We can enhance the proving power of MGTP (Model Generati
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=jairo_______::4bafee36d40a2e1b15b5601cc62f7149
http://hdl.handle.net/2324/1515817
Zobrazit plný text záznamu
9
一般化補題を利用したモデル生成法
Publikováno v: 九州大学大学院システム情報科学紀要. 8(1):55-59
We can prune unnecessary search spaces using lemmas. In order to enhance the pruning ability of lemmas, we introduce a method to generalize them. There may be many cases to which generalized lemma can be applied but non-generalized one can not. Then
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=jairo_______::a8b823a15ef0967e75eff1ab4936bfda
http://hdl.handle.net/2324/1515818
Zobrazit plný text záznamu
10
An Efficient Method to Generate Minimal Models by Introducing Splitting Lemmas
Publikováno v: 九州大学大学院システム情報科学紀要. 4(2):145-150
An efficient method for minimal model generation is presented. The extended MGTP, called MM-MGTP, was implemented using the method so that every model it generates is guaranteed to be minimal. The method employs splitting assumption which is equivale
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=jairo_______::7ee8abd65ad8e280b5fc7b6070151b8f
http://hdl.handle.net/2324/1513728
Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání

Omezení vyhledávání
Plný text Recenzováno Digitální knihovna AV ČR
Zdroje