Zobrazeno 1 - 10
of 95
pro vyhledávání: '"Theorem Proving System"'
Autor:
Mingkai Zhou
Publikováno v:
OALib. :1-8
Learning methods such as neural network and decision tree need a certain number of training samples to achieve a certain level of generalization accuracy. Analytic learning uses prior knowledge and deductive reasoning to expand the information provid
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8c9f44c6d9cc2b4ec7352d608d068b7b
https://doi.org/10.4236/oalib.preprints.1200295
https://doi.org/10.4236/oalib.preprints.1200295
Autor:
Chad E. Brown, Peter B. Andrews
Publikováno v:
Journal of Applied Logic. 4(4):367-395
The theorem proving system Tps provides support for constructing proofs using a mix of automation and user interaction, and for manipulating and inspecting proofs. Its library facilities allow the user to store and organize work. Mathematical theorem
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6bb4be5c8954822b39c44d15ac8a0c62
Publikováno v:
Journal of Applied Mathematics, Vol 2014 (2014)
J. Appl. Math.
J. Appl. Math.
The paper presents a formal proof of a machine closed theorem of TLA+in the theorem proving system Coq. A shallow embedding scheme is employed for the proof which is independent of concrete syntax. Fundamental concepts need to state that the machine
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3c0dd2da70394c74dd475d4151b52134
https://doi.org/10.1155/2014/892832
https://doi.org/10.1155/2014/892832
Publikováno v:
Iosif-Lazăr, A F & Wasowski, A 2016, ' Trustworthy Variant Derivation with Translation Validation for Safety Critical Product Lines ', The Journal of Logic and Algebraic Programming, vol. 85, no. 6, 85, pp. 1154–1176 . https://doi.org/10.1016/j.jlamp.2016.02.001
Software product line (SPL) engineering facilitates development of entire families of software products with systematic reuse. Model driven SPLs use models in the design and development process. In the safety critical domain, validation of models and
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::21dabf2145316025156b809cd725b192
https://pure.itu.dk/ws/files/82447551/2016_jlamp_afla_trustworthy_variant_derivation.pdf
https://pure.itu.dk/ws/files/82447551/2016_jlamp_afla_trustworthy_variant_derivation.pdf
Autor:
Camille Fayollas, Saulo Rodrigues e Silva, Célia Martinie, Paolo Masci, Michael D. Harrison, José Creissac Campos, Philippe Palanque
Publikováno v:
Proceedings of the 3rd Workshop on Formal Integrated Development Environment
3rd Workshop on Formal Integrated Development Environment (F-IDE 2016), co-located with FM 2016, 21st International Symposium on Formal Methods
3rd Workshop on Formal Integrated Development Environment (F-IDE 2016), co-located with FM 2016, 21st International Symposium on Formal Methods, Nov 2016, Limassol, Cyprus. pp. 1-19
Electronic Proceedings in Theoretical Computer Science, Vol 240, Iss Proc. F-IDE 2016, Pp 1-19 (2017)
3rd Workshop on Formal Integrated Development Environment (F-IDE 2016), co-located with FM 2016, 21st International Symposium on Formal Methods
3rd Workshop on Formal Integrated Development Environment (F-IDE 2016), co-located with FM 2016, 21st International Symposium on Formal Methods, Nov 2016, Limassol, Cyprus. pp. 1-19
Electronic Proceedings in Theoretical Computer Science, Vol 240, Iss Proc. F-IDE 2016, Pp 1-19 (2017)
Critical human-machine interfaces are present in many systems including avionics systems and medical devices. Use error is a concern in these systems both in terms of hardware panels and input devices, and the software that drives the interfaces. Gua
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::daee70774b49dbb39975acd5894cb28b
https://hal.archives-ouvertes.fr/hal-01757338/file/fayollas_18933.pdf
https://hal.archives-ouvertes.fr/hal-01757338/file/fayollas_18933.pdf
Publikováno v:
ASYNC
The increasing scale and complexity of integrated circuits leads to many departures from a pure, synchronous design methodology. Clock-domain crossings, multi-cycle paths, and circuits for test with long combinational logic delays introduce vulnerabi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::df55df08f05a7f39658d8e9c53b03d47
https://doi.org/10.1109/async.2016.12
https://doi.org/10.1109/async.2016.12
Publikováno v:
International Journal of Communications, Network and System Sciences. :165-177
Group key security protocols play an important role in today’s communication systems. Their verification, however, remains a great challenge because of the dynamic characteristics of group key construction and distribution protocols. Security prope
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ba94c0af0560a4cd29f4c3a74f7195b3
https://doi.org/10.4236/ijcns.2012.53021
https://doi.org/10.4236/ijcns.2012.53021
Autor:
Filip Maric
Publikováno v:
Journal of Automated Reasoning. 43:81-119
Most, if not all, state-of-the-art complete SAT solvers are complex variations of the DPLL procedure described in the early 1960's. Published descriptions of these modern algorithms and related data structures are given either as high-level state tra
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8f2493e8b7e523fcba8fb0c96189f3c9
https://doi.org/10.1007/s10817-009-9127-8
https://doi.org/10.1007/s10817-009-9127-8
Publikováno v:
Formal Methods in System Design. 30:83-116
We describe an approach for formally verifying the linkage between a symbolic state enumeration system and a theorem proving system. This involves the following three stages of proof. Firstly we prove theorems about the correctness of the translation
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::359774072dcb99f37a6832bf3fd8f4c9
https://doi.org/10.1007/s10703-006-0017-y
https://doi.org/10.1007/s10703-006-0017-y
Autor:
Jacek Tkacz
Publikováno v:
IFAC Proceedings Volumes. 39:53-56
The paper presents a practical application of Gentzen theorem proving system by means of an experimental computer tool, for the purpose of logic expressions normalization into the form similar to the Horn clauses. The initial expressions are describe
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5c4ae846f41542c429cbd341ea581b66
https://doi.org/10.3182/20060926-3-pl-4904.00010
https://doi.org/10.3182/20060926-3-pl-4904.00010